Why Are Trailing Commas Not Allowed in Array Literals?

Stream: lean4

[Asei Inoue]

As shown in the code below, trailing commas are allowed in List literals but not in Array literals.

-- OK!
def list := [1, 2, 3,]

-- unexpected token ']';
def array := #[1, 2, 3,]

Is there any rational reason for this, or was it just an mistake/bug? If it was an bug, would a fix be welcome?

[Kim Morrison]

It does seem reasonable to fix this (also for Vector?), and I think should be safely straightforward, so a fix would be welcome.

[Asei Inoue]

@Kim Morrison I have submitted a PR. https://github.com/leanprover/lean4/pull/7055

[Kim Morrison]

@Asei Inoue, there's still quite a bit you need to do on that PR, let me know if you don't understand what's being asked (CI, Mathlib CI, add tests).

[François G. Dorais]

Since Vector is in core now, would it be feasible to unify the vector and array notations? That is, have #[...] give a Vector, which is coerced to Array when necessary?

[Kim Morrison]

Seems confusing rather than helpful? Could you explain the motivation more?

[Asei Inoue]

@Kim Morrison

I want to setup development environment in wsl2. I've read the manual: https://lean-lang.org/lean4/doc/dev/index.html#development-workflow

but I get the following error.

asei@gtune:~/lean4$ elan toolchain link lean4 build/release/stage1
error: not a directory: 'build/release/stage1/bin'

How to solve this?

[Kim Morrison]

Have you actually built Lean yet, per the instructions at https://lean-lang.org/lean4/doc/make/wsl.html? The elan toolchain step only comes later, once you want to use VSCode with your newly built Lean.

[François G. Dorais]

@Kim Morrison Just one notation for two types that are a hair from each other. For example, if I move from Polygon := Array (Array R) to Polygon := Array (Vector R 3) then I have to annoyingly add vs to all my standard polygon definitions. This is easily automated in this artificial example but no change would be even better regardless.

[Kim Morrison]

I think I'd prefer not for now, but I'm happy to hear other opinions.

[James Gallicchio]

I wouldn't mind a different notation for vectors, but any notation would be useful. I'm a little tired of writing \<#[a,b,c], by simp\> :joy:

[Markus Himmel]

Are you aware of the #v[a, b, c] notation?

[James Gallicchio]

oh!!!! I was not!

[James Gallicchio]

sorry, ignore the noise

[Asei Inoue]

@Kim Morrison

Have you actually built Lean yet, per the instructions at https://lean-lang.org/lean4/doc/make/wsl.html? The elan toolchain step only comes later, once you want to use VSCode with your newly built Lean.

I have read everything written at https://lean-lang.org/lean4/doc/make/wsl.html and tried it all, but it doesn’t work. I wish there was a Devcontainer available.

[Asei Inoue]

I realized my misunderstanding. I apologize for that.

[Asei Inoue]

I thought the CI error would be fixed with this commit, but I was too optimistic. Why isn’t it resolved…?

[Asei Inoue]

help me please, anyone

[Kyle Miller]

Changing the syntax name is breaking a deriving handler, because it's compiled for the old syntax name and it's in stage0 and being used to compile stage1.

Easiest would be to preserve the current syntax name I think.

[Kyle Miller]

I'm not sure how you could change the syntax name, except to (1) track down where #[...] syntax is used and replace it with its expansion, (2) recompile stage0, (3) rename the syntax, (4) revert changes in 1.

[Chris Wong]

I know Rust has stage0 compilation flags for this purpose. Does Lean have a similar system?

[Kim Morrison]

(Yes, but sometimes there are complicated edges cases, and from Kyle's message this appears to be one!)

[Eric Wieser]

Where would things like Kyle's suggestion fit in with @Joachim Breitner's bootstrapping ancestry tool?

[Joachim Breitner]

Eric Wieser said:

Where would things like Kyle's suggestion fit in with Joachim Breitner's bootstrapping ancestry tool?

If these steps happen in separate commits on the PR (which may not all have to pass the test suite) then https://lean-stage0.nomeata.de/ may be able to retrace it

[Asei Inoue]

why CI staill fails? I cannot edit PR labels...

https://github.com/leanprover/lean4/pull/7055

[Joachim Breitner]

It seems we need to update https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md. You can set changelog-language by writing that into a comment.

[Asei Inoue]

done!