lake new missing lean-toolchain

Stream: lean4

[Patrick Massot]

I would like to test this change, but I'm not good enough at wrestling lake. I tried lake +leanprover/lean4-pr-releases:pr-release-2393 new endproof math by imitation. But this creates a folder with no lean-toolchain file, no manifest, no lake-packages. I tried creating a lean-toolchain file, ran lake update but then the mathlib lean-toolchain is incompatible. Is there a way to have this working? Or should I test this without mathlib?

[Sebastian Ullrich]

Yes, testing without mathlib might be the simplest option. I didn't check whether we had already accumulated breaking changes compared to mathlib master's toolchain.

[Patrick Massot]

Removing math from the lake invocation doesn fix the missing lean-toolchain bug. Running lake +leanprover/lean4-pr-releases:pr-release-2393 new endproof produces a endproof folder without a lean-toolchain file.

[Scott Morrison]

I see the same thing. @Mac Malone?

[Mac Malone]

@Scott Morrison Does the PR release set the Lean.toolchain?

[Mac Malone]

There would also then to be a mathlib cache for said toolchain.

[Scott Morrison]

No, it doesn't. I will work on fixing that. I had assumed in this case that the explicit toolchain in the lake +xyz invocation would do something!

[Scott Morrison]

Can lake new print a big helpful warning message if it decides not to create a lean-toolchain, rather than silently giving you an unusable project?

[Scott Morrison]

Setting Lean.toolchain in PR releases does not look like a good idea. e.g. in src/Init/Meta.lean you can see that the toolchain is either going to be empty or to start with leanprover/lean4. Changing this would require gross plumbing that modifies the PR build process.

Can't lake +xyz just automatically use xyz as the toolchain? It seems like the natural behaviour.

[Sebastian Ullrich]

Unfortunately that +xyz is handled by elan, Lake has no idea about it

[Scott Morrison]

There's an issue tracking this now, lean4#2518.

[Scott Morrison]

There Mac suggested that elan could set an environment variable so the +toolchain information could be picked up.