Allow trailing comma in tuples, lists, and tactics #2643

lenianiva · 2023-10-09T19:21:29Z

Put an X in this bracket to confirm you have read the
External Contribution Guidelines.
Please put the link to your RFC or bug issue here.
PRs missing this link will be marked as missing RFC.

If that issue does not already have approval from a developer,
please be sure to open this PR in "Draft" mode.
Please make sure the PR has excellent documentation and tests.
If we label it missing documentation or missing tests then it needs fixing!
You can manage the awaiting-review, awaiting-author, and WIP labels
yourself, by writing a comment containing one of these labels on its own line.

lenianiva · 2023-10-09T19:30:09Z

I'm modifying the array syntax and for some reason this doesn't work

-- src/Init/Data/Array/Basic.lean
syntax "#[" withoutPosition(sepBy(term, ", ", allowTrailingSep)) "]" : term

which gives

Init/Data/Array/Basic.lean:507:46: error: unknown parser declaration/category/alias 'allowTrailingSep'

This is puzzling since the 3rd argument is explicitly marked as optional:

-- src/Lean/Parser/Syntax.lean
@[builtin_syntax_parser] def sepBy           := leading_parser
  "sepBy(" >> withoutPosition (many1 syntaxParser >> ", " >> strLit >>
    optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep")) >> ")"

digama0 · 2023-10-09T20:14:56Z

Because there isn't any disambiguator between the two optional fields, it just prefers the first parse in which allowTrailingSep is treated as a syntax element referring to a (nonexistent) parser. So you have to give the third argument explicitly if you want to pass the fourth one, that is, sepBy(term, ",", ", ", allowTrailingSep). Or better yet, just use term,*,? since this isn't setting anything different from the default (see Init/Notation.lean#L238).

lenianiva · 2023-10-09T20:17:47Z

Because there isn't any disambiguator between the two optional fields, it just prefers the first parse in which allowTrailingSep is treated as a syntax element referring to a (nonexistent) parser. So you have to give the third argument explicitly if you want to pass the fourth one, that is, sepBy(term, ",", ", ", allowTrailingSep). Or better yet, just use term,*,? since this isn't setting anything different from the default (see Init/Notation.lean#L238).

I tried sepBy(term, ",", ", ", allowTrailingSep) and it doesn't work either. I'll use term,*,? like what we have in lists.

digama0 · 2023-10-09T20:37:40Z

It should... one is literally just a macro for the other. What error do you get, and when?

lenianiva · 2023-10-09T21:22:25Z

It should... one is literally just a macro for the other. What error do you get, and when?

This is what I get when I write either of

-- Array/Basic.lean
syntax "#[" withoutPosition(term,*,?) "]" : term
syntax "#[" withoutPosition(sepBy(term, ",", ", ", allowTrailingSep)) "]" : term

The same schematic allowed me to implement trailing comma for lists though

Lean/Widget/TaggedText.lean:24:43: error: elaboration function for '«term#[_,]»' has not been implemented
  [Error pretty printing syntax: unknown constant 'term#[_,]'. Falling back to raw printer.]
  («term#[_,]»
   "#["
   [(Term.app `[email protected]._hyg.4 [`[email protected]._hyg.640])
    ","
    (Term.app `[email protected]._hyg.635 [`[email protected]._hyg.641])]
   "]")
make[7]: *** [../build/debug/stage1/lib/lean/Lean/Widget/TaggedText.olean] Error 1

digama0 · 2023-10-09T21:50:51Z

That's a bootstrapping issue, you will get the same error making any change to a builtin parser. See https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/Bootstrapping.20issue.3F for a recent similar discussion, and see if setting parseQuotWithCurrentStage in stage0/src/stdlib_flags.h works for you.

lenianiva · 2023-10-09T21:52:47Z

That's a bootstrapping issue, you will get the same error making any change to a builtin parser. See https://leanprover.zulipchat.com/#narrow/stream/341532-lean4-dev/topic/Bootstrapping.20issue.3F for a recent similar discussion, and see if setting parseQuotWithCurrentStage in stage0/src/stdlib_flags.h works for you.

Would the unit tests pass if I just change the file in stage0 without committing it into the repo?

digama0 · 2023-10-09T21:55:45Z

You should make the stage0 change (and commit it), then run make update-stage0 which will clobber the change in addition to copying stage1 to stage0 (and commit this too as chore: update stage0), then compile again and ensure the tests pass in the second run. See https://github.com/leanprover/lean4/blob/master/doc/dev/bootstrap.md for more information.

leanprover-community-mathlib4-bot · 2023-10-09T22:27:36Z

✅ Mathlib branch lean-pr-testing-2643 has successfully built against this PR. (2023-10-09 22:27:32) View Log
✅ Mathlib branch lean-pr-testing-2643 has successfully built against this PR. (2023-10-10 00:38:49) View Log
✅ Mathlib branch lean-pr-testing-2643 has successfully built against this PR. (2023-10-18 23:44:44) View Log
✅ Mathlib branch lean-pr-testing-2643 has successfully built against this PR. (2023-10-19 01:12:03) View Log
✅ Mathlib branch lean-pr-testing-2643 has successfully built against this PR. (2023-10-19 03:07:52) View Log
✅ Mathlib branch lean-pr-testing-2643 has successfully built against this PR. (2023-10-20 04:51:08) View Log
✅ Mathlib branch lean-pr-testing-2643 has successfully built against this PR. (2023-10-20 06:59:31) View Log
💥 Mathlib branch lean-pr-testing-2643 build failed against this PR. (2023-10-24 08:39:44) View Log

lenianiva · 2023-10-10T05:20:49Z

You should make the stage0 change (and commit it), then run make update-stage0 which will clobber the change in addition to copying stage1 to stage0 (and commit this too as chore: update stage0), then compile again and ensure the tests pass in the second run. See https://github.com/leanprover/lean4/blob/master/doc/dev/bootstrap.md for more information.

I think I'm doing this correctly but it is not working:

Make the necessary stage 0 changes to Array/Basic.lean
Commit
make update-stage0

which gives

Lean/SubExpr.lean:198:21: error: elaboration function for '«term#[_,]»' has not been implemented
  [Error pretty printing syntax: unknown constant 'term#[_,]'. Falling back to raw printer.]
  («term#[_,]»
   "#["
   [(Term.app `toJson[email protected]._hyg.1526 [`a[email protected]._hyg.1870])
    ","
    (Term.app `toJson[email protected]._hyg.1526 [`a[email protected]._hyg.1871])]
   "]")
Lean/SubExpr.lean:198:21: error: elaboration function for '«term#[_,]»' has not been implemented
  [Error pretty printing syntax: unknown constant 'term#[_,]'. Falling back to raw printer.]
  («term#[_,]»
   "#["
   [(Term.app `toJson[email protected]._hyg.1526 [`a[email protected]._hyg.1872])
    ","
    (Term.app `toJson[email protected]._hyg.1526 [`a[email protected]._hyg.1873])]
   "]")
[    ] Building ../build/debug/stage1/lib/temp/Lean/Elab/Config.c

This fails even if I just write withoutPosition(term,*), which should have identical behaviour as before, instead of withoutPosition(term,*,?)

digama0 · 2023-10-10T05:49:34Z

This fails even if I just write withoutPosition(term,*), which should have identical behaviour as before, instead of withoutPosition(term,*,?)

I believe the reason for the change is that the default name for the term,* variant is term#[_] instead of term#[_,] (this name is constructed by looking at the syntax used to specify the parser).

lenianiva · 2023-10-10T06:35:20Z

This fails even if I just write withoutPosition(term,*), which should have identical behaviour as before, instead of withoutPosition(term,*,?)

I believe the reason for the change is that the default name for the term,* variant is term#[_] instead of term#[_,] (this name is constructed by looking at the syntax used to specify the parser).

How come the same change for list was fine?

digama0 · 2023-10-10T07:12:08Z

Most likely because the derive handler in question (running stage0 code which is no longer correct) happens to be constructing arrays and not lists.

lenianiva · 2023-10-10T20:31:05Z

Most likely because the derive handler in question (running stage0 code which is no longer correct) happens to be constructing arrays and not lists.

so should I just leave the stage 0 code alone and add a separate syntax for arrays with a trailing comma?

lenianiva · 2023-10-13T17:43:22Z

Most likely because the derive handler in question (running stage0 code which is no longer correct) happens to be constructing arrays and not lists.

I dug into this a bit more and all of the errors occur in Lean/Elab/Deriving/FromToJson.lean, but I could not pinpoint exactly where does compilation fail.

src/Init/Notation.lean

tests/compiler/array.lean

tests/lean/rewrite.lean

lenianiva · 2023-10-23T18:25:14Z

@semorrison Could you take a look to see if this is ready to merge?

Kha

LGTM, but just to double-check: are we happy with (1,) meaning the same as (1)? It has a special meaning (1-tuple) in Python but I don't think that has to affect the design of a statically typed language like Lean.

tests/lean/StxQuot.lean.expected.out

kim-em · 2023-10-25T02:04:20Z

LGTM, but just to double-check: are we happy with (1,) meaning the same as (1)? It has a special meaning (1-tuple) in Python but I don't think that has to affect the design of a statically typed language like Lean.

Hmm this is a good point. I think tuples should not allow trailing commas.

digama0 · 2023-10-25T03:16:50Z

I lean toward allowing this, with (1,) meaning the same as (1), because it is useful for macro-style code to be able to just have consistent behavior in the base case, and tuples are iterated cases of Prod constructor with the base case just being the underlying type.

Kha · 2023-11-17T12:31:47Z

Thanks!

…2643)

lenianiva changed the title ~~Allow trailing comma in tuples, lists, arrays, and tactics~~ feat: Allow trailing comma in tuples, lists, arrays, and tactics Oct 9, 2023

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 9, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 9, 2023

Update lean-toolchain for testing leanprover/lean4#2643

82de2c6

leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 9, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 9, 2023

Trigger CI for leanprover/lean4#2643

0885e35

lenianiva added 3 commits October 18, 2023 13:44

feat: Allow trailing comma in tuples

771e8ad

feat: Allow trailing commas in lists

9e9790d

fix: Single test failure due to trailing comma

5f8d488

lenianiva force-pushed the parser/trailing-comma branch from 67fbcfb to 5f8d488 Compare October 18, 2023 21:02

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 18, 2023

Trigger CI for leanprover/lean4#2643

ef4c34d

feat: Allow trailing commas in simp and rewrite

fab8b65

lenianiva changed the title ~~feat: Allow trailing comma in tuples, lists, arrays, and tactics~~ feat: Allow trailing comma in tuples, lists, and tactics Oct 18, 2023

lenianiva marked this pull request as ready for review October 18, 2023 22:33

lenianiva mentioned this pull request Oct 18, 2023

RFC: Allow trailing comma after the last element of a list #2635

Closed

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 18, 2023

Trigger CI for leanprover/lean4#2643

f157df3

digama0 reviewed Oct 18, 2023

View reviewed changes

src/Init/Notation.lean Outdated Show resolved Hide resolved

feat: Move list syntax to Init/Data/List/Basic

77f54e9

kim-em reviewed Oct 19, 2023

View reviewed changes

tests/compiler/array.lean Outdated Show resolved Hide resolved

kim-em reviewed Oct 19, 2023

View reviewed changes

tests/lean/rewrite.lean Outdated Show resolved Hide resolved

kim-em added the missing tests This PR requires the addition of tests before it can be merged. label Oct 19, 2023

kim-em self-requested a review October 19, 2023 01:27

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 19, 2023

Trigger CI for leanprover/lean4#2643

96ca09b

refactor: Consolidate trailing comma tests

fea24cb

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 20, 2023

Trigger CI for leanprover/lean4#2643

3d65184

test: Test the trailing comma in simp

7c7e9c2

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 20, 2023

Trigger CI for leanprover/lean4#2643

246cc82

Kha reviewed Oct 24, 2023

View reviewed changes

tests/lean/StxQuot.lean.expected.out Outdated Show resolved Hide resolved

test: Test invalid syntax

f45d620

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 24, 2023

Trigger CI for leanprover/lean4#2643

feb4f7f

leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Oct 24, 2023

kim-em added awaiting-review Waiting for someone to review the PR changelog and removed missing tests This PR requires the addition of tests before it can be merged. breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Oct 26, 2023

Kha approved these changes Nov 17, 2023

View reviewed changes

Kha changed the title ~~feat: Allow trailing comma in tuples, lists, and tactics~~ Allow trailing comma in tuples, lists, and tactics Nov 17, 2023

Kha merged commit ab36ed4 into leanprover:master Nov 17, 2023
18 checks passed

arthur-adjedj pushed a commit to arthur-adjedj/lean4 that referenced this pull request Nov 20, 2023

feat: allow trailing comma in tuples, lists, and tactics (leanprover#…

4489ede

…2643)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Allow trailing comma in tuples, lists, and tactics #2643

Allow trailing comma in tuples, lists, and tactics #2643

lenianiva commented Oct 9, 2023

lenianiva commented Oct 9, 2023 •

edited

Loading

digama0 commented Oct 9, 2023

lenianiva commented Oct 9, 2023

digama0 commented Oct 9, 2023

lenianiva commented Oct 9, 2023

digama0 commented Oct 9, 2023

lenianiva commented Oct 9, 2023 •

edited

Loading

digama0 commented Oct 9, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Oct 9, 2023 •

edited

Loading

lenianiva commented Oct 10, 2023

digama0 commented Oct 10, 2023

lenianiva commented Oct 10, 2023

digama0 commented Oct 10, 2023 •

edited

Loading

lenianiva commented Oct 10, 2023

lenianiva commented Oct 13, 2023

lenianiva commented Oct 23, 2023

Kha left a comment

kim-em commented Oct 25, 2023

digama0 commented Oct 25, 2023

Kha commented Nov 17, 2023

Allow trailing comma in tuples, lists, and tactics #2643

Allow trailing comma in tuples, lists, and tactics #2643

Conversation

lenianiva commented Oct 9, 2023

lenianiva commented Oct 9, 2023 • edited Loading

digama0 commented Oct 9, 2023

lenianiva commented Oct 9, 2023

digama0 commented Oct 9, 2023

lenianiva commented Oct 9, 2023

digama0 commented Oct 9, 2023

lenianiva commented Oct 9, 2023 • edited Loading

digama0 commented Oct 9, 2023 • edited Loading

leanprover-community-mathlib4-bot commented Oct 9, 2023 • edited Loading

lenianiva commented Oct 10, 2023

digama0 commented Oct 10, 2023

lenianiva commented Oct 10, 2023

digama0 commented Oct 10, 2023 • edited Loading

lenianiva commented Oct 10, 2023

lenianiva commented Oct 13, 2023

lenianiva commented Oct 23, 2023

Kha left a comment

Choose a reason for hiding this comment

kim-em commented Oct 25, 2023

digama0 commented Oct 25, 2023

Kha commented Nov 17, 2023

lenianiva commented Oct 9, 2023 •

edited

Loading

lenianiva commented Oct 9, 2023 •

edited

Loading

digama0 commented Oct 9, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Oct 9, 2023 •

edited

Loading

digama0 commented Oct 10, 2023 •

edited

Loading