Outdated quickstart instructions?

Stream: new members

[Li Xuanji]

I followed the instructions exactly as written for creating a Lean project that depends on mathlib and it looks like the mkdir MyProject is unnecessary (some command already created that folder, presumably by converting my snake_case argument to SentenceCase and creating a folder with it)

I'm happy to create a PR to fix this if that's the intended behaviour of lake

As a separate question, is there a way to make it create a lakefile.toml instead of a lakefile.lean? I generally prefer the former

[Yaël Dillies]

Very interesting! Thank you for informing us. @Mac Malone, do you think we can get lake ... new math to create a lakefile.toml by default?

[Kevin Buzzard]

I can reproduce; "and then mkdir MyProject" needs to go. Independently of this, do we have a better incantation yet for this lake command which doesn't have the 2024 date in it? e.g. "type elan something something to ensure that you're not on some super-old lean by default"

[Kevin Buzzard]

lake new my_project math is giving me a lean-toolchain of leanprover/lean4:v4.19.0-rc3but IIRC if you installed Lean 2 years ago and then didn't use it then you used to get some catastrophically old thing? Is this still the case?

[Marc Huisinga]

Kevin Buzzard said:

lake new my_project math is giving me a lean-toolchain of leanprover/lean4:v4.19.0-rc3but IIRC if you installed Lean 2 years ago and then didn't use it then you used to get some catastrophically old thing? Is this still the case?

If your default toolchain is leanprover/lean4:stable and you're using Elan 4.0.0, then no.

[Marc Huisinga]

I plan to warn users in the VS Code extension if they have an Elan version older than 4.0.0 in a couple of months when hopefully all the package repositories shipping Elan have caught up.

[Kevin Buzzard]

So I'm wondering whether on the community website, instead of saying "install this old version of Lean, trust us, we know what we're doing even though it looks confusing", we should say "type elan self update and then elan default toolchain something and then lake new my_project math"?

[Yaël Dillies]

Just FYI we're still shipping elan 3.blah in the docker images. I need to rebuild them, but haven't yet managed to get the setup working on my laptop

[Marc Huisinga]

Kevin Buzzard said:

So I'm wondering whether on the community website, instead of saying "install this old version of Lean, trust us, we know what we're doing even though it looks confusing", we should say "type elan self update and then elan default toolchain something and then lake new my_project math"?

Sounds reasonable to me.

[Mac Malone]

Yaël Dillies said:

Very interesting! Thank you for informing us. Mac Malone, do you think we can get lake ... new math to create a lakefile.toml by default?

What do you mean? Any Lake after lean4#5504 (v4.13.0-rc1) should have produced a lakefile.toml by default.

[Kevin Buzzard]

lake new my_project math is giving me a lakefile.lean

[Kevin Buzzard]

As is lake +leanprover/lean4:nightly-2024-04-24 new my_project math (the current instructions on the community website)

[Li Xuanji]

Yeah, looks like bumping that date to something more recent creates a lakefile.toml for me. The command I used to test is lake +leanprover/lean4:nightly-2025-03-01 new tp3 math.

(I'm not sure what exactly that + argument is used for, the documentation returned by lake help new says "lean-version", but that's a bit terse and the version doesn't seem to be persisted anywhere in the created project...)

So probably the fastest fix is to update the quickstart guide to ask users to pass a newer version there.

[Marc Huisinga]

Li Xuanji said:

(I'm not sure what exactly that + argument is used for, the documentation returned by lake help new says "lean-version", but that's a bit terse and the version doesn't seem to be persisted anywhere in the created project...)

Since Lake depends on Lean and is shipped together with it, Lake itself differs based on the Lean version you're using. +<toolchain> instructs Elan to invoke the Lake of <toolchain>. Here, this is helpful since the implementation of lake new itself has changed over time with different Lean versions, so we usually want to ensure that new projects are created using a recent version of Lake.

[Marc Huisinga]

Kevin Buzzard said:

lake new my_project math is giving me a lakefile.lean

mhuisi@fedora:~/Lean$ lake new MyProject math
info: downloading mathlib `lean-toolchain` file
mhuisi@fedora:~/Lean$ cd MyProject/
mhuisi@fedora:~/Lean/MyProject$ ls
lakefile.toml  lean-toolchain  MyProject  MyProject.lean  README.md

What's your default toolchain?

[Kevin Buzzard]

I have no idea. As an end user am I supposed to understand this question and if so, should be we explaining this in the instructions?

[Kevin Buzzard]

Every lean project I've started in the last year or so has been "use a GitHub template which is already set up with blueprint" not "use lake"

[Ruben Van de Velde]

I think "default toolchain" is "whatever elan gives outside a project"

[Ruben Van de Velde]

And the +blah is saying "don't use that"

[Kevin Buzzard]

So this strikes me as a very weird setup. Is there any good value for "default toolchain" which won't become a super-bad value for a user who tries lean once, forgets about it, and comes back to it in two years when the ecosystem has moved on so much that using the old toolchain is a disaster?

[Kevin Buzzard]

Is there a way that we can tell users to set the default toolchain to always be on the latest stable? Or, with math appended to lake, to be on mathlib's current toolchain? The current instructions on the community website always struck me as very odd and more than one question has been asked about them before.

[Kevin Buzzard]

tl;dr: why can't I have my "default toolchain" being "any recent one, please" or "mathlib's one"? Those are the only two I ever want.

[Marc Huisinga]

Kevin Buzzard said:

I have no idea. As an end user am I supposed to understand this question and if so, should be we explaining this in the instructions?

You can check it via elan show.

Kevin Buzzard said:

So this strikes me as a very weird setup. Is there any good value for "default toolchain" which won't become a super-bad value for a user who tries lean once, forgets about it, and comes back to it in two years when the ecosystem has moved on so much that using the old toolchain is a disaster?

As mentioned above, leanprover/lean4:stable is now such a toolchain, and it is what Elan uses by default. But you might have changed it in the past, which is why I'm asking the question.

[Sebastian Ullrich]

Use of the cmdline hasn't been necessary for a long time to start a new math project. This is all explained in the official quickstart (or rather, the Setup Guide it points to). The community page seems to be doing a huge disservice to newcomers here. Why not replace at least the cmdline instructions with a link to the official guide?

[Li Xuanji]

Hmm, I am more comfortable using the command line than vscode and would prefer to at least have the steps for creating a new project without using vscode documented somewhere

Of course, for actually editing the lean code vscode is indispensable for the infoview, what I mean is that I would want to spend as little time in vscode as possible other than that.

[Marc Huisinga]

Li Xuanji said:

Hmm, I am more comfortable using the command line than vscode and would prefer to at least have the steps for creating a new project without using vscode documented somewhere

Of course, for actually editing the lean code vscode is indispensable for the infoview, what I mean is that I would want to spend as little time in vscode as possible other than that.

It should definitely still be documented somewhere on the community page, but perhaps not all new users should be guided towards this way of setting up projects when the VS Code way is as easy as "click this button and select a project location"

image.png

[Kevin Buzzard]

https://github.com/leanprover-community/leanprover-community.github.io/pull/620 for the original question in this thread BTW.

[Kevin Buzzard]

I'll start a new one for this other issue.

[Marc Huisinga]

@Kevin Buzzard
Could you also run elan default leanprover/lean4:stable and check whether lake new my_project math now creates a project with a lakefile.toml?
I just want to make sure that you have a reasonable setup, too.

[Mario Carneiro]

can lake new foo mathlib be made to work? The "math" abbreviation is not used as an abbreviation for mathlib anywhere else

[Kevin Buzzard]

I'm starting a new thread in #general. Hopefully the question which started this thread is answered and this is not an appropriate channel for this conversation. @Marc Huisinga I'll get to your question in a second.

[Kevin Buzzard]

Marc, apparently my default is leanprover/lean4:v4.5.0-rc1, which is presumably the last time I ever messed with elan on the command line. I can confirm that I get the toml after switching default to stable.

[Mario Carneiro]

Is there a non CLI way to update the CLI?

[Marc Huisinga]

Mario Carneiro said:

Is there a non CLI way to update the CLI?

You can update Elan via 'Version Management > Setup: Update Elan'.

[Mario Carneiro]

that updates elan, not the default toolchain though

[Kevin Buzzard]

PS I realised I lied above: a while ago I did once create a new test math project following the instructions on lean-lang (a website which I barely ever look at) because I was whingeing about there being no GUI way to create projects (having read the community site) and then Sebastian pointed out that I was now out of date. I agree that we should switch to telling new users to follow the official instructions and I mentioned this in my post in #general

[Marc Huisinga]

Mario Carneiro said:

that updates elan, not the default toolchain though

Release channels like leanprover/lean4:stable are updated automatically as of Elan 4.0.0 (see here) and you can set the default toolchain via 'Version Management > Setup: Select Default Lean Version'.

[Mario Carneiro]

the "show setup information" option pops a modal dialog which makes it a bit hard to use; it also cuts off at the end

**Operating system**: Linux (release: 6.8.0-57-generic)
**CPU architecture**: x64
**CPU model**: 12 x 12th Gen Intel(R) Core(TM) i7-1255U
**Available RAM**: 33.28 GB

**VS Code version**: Reasonably up-to-date (version: 1.98.2)
**Lean 4 extension version**: 0.0.202
**Curl installed**: true
**Git installed**: true
**Elan**: Reasonably up-to-date (version: 4.0.0)
**Lean**: Reasonably up-to-date (version: 4.20.0-pre)
**Project**: Valid Lean project (path: /home/mario/Documents/lean/lean4)
**Active Lean version**: lean4 (set by `elan override` in `file:///home/mario/Documents/lean/lean4`)
**Installed Lean versions**: lean4, lean4-stage0, leanprover/lean4-pr-releases:pr-release-3159, leanprover/lean4-pr-releases:pr-release-7059, leanprover/lean4:v4.1.0-rc1, leanprover/lean4:v4.10.0-rc1, leanprover/lean4:v4.10.0-rc2, leanprover/lean4:v4.11.0-rc2, leanprover/lean4:v4.13.0, leanprover/lean4:v4.14.0-rc1, leanprover/lean4:v4.14.0-rc3, leanprover/lean4:v4.15.0, leanprover/lean4:v4.16.0, leanprover/lean4:v4.16.0-rc2, leanprover/lean4:v4.17.0, leanprover/lean4:v4.17.0-rc1, leanprover/lean4:v4.18.0-rc1, leanprover/lean4:v4.19.0-rc2, leanprover/lean4:v4.19.0-rc3, leanprover/lean4:v4.6.0-rc1 ...

[Marc Huisinga]

This is getting extremely off-topic, but 'Installed Lean versions' is truncated because for some silly reason VS Code doesn't provide scrolling functionality for modal dialogs.

This dialog is primarily intended for debugging user setups on Zulip, so that you can quickly figure out the state of a user's system, usually in a project. The full list of toolchains they have installed isn't as important.

[Marc Huisinga]

(We also have a link for it now at #vsc-setup)

[Mario Carneiro]

well I was mostly worried that there were more headings after that one

[Mario Carneiro]

it's also in fake markdown

[Marc Huisinga]

Mario Carneiro said:

well I was mostly worried that there were more headings after that one

It only truncates that entry.

Mario Carneiro said:

it's also in fake markdown

Yes, so that you can directly copy and paste it into Zulip and it'll be nicely formatted:

Operating system: Linux (release: 6.13.7-200.fc41.x86_64)
CPU architecture: x64
CPU model: 16 x AMD Ryzen 7 7800X3D 8-Core Processor
Available RAM: 32.81 GB

VS Code version: Reasonably up-to-date (version: 1.98.2)
Lean 4 extension version: 0.0.202
Curl installed: true
Git installed: true
Elan: Reasonably up-to-date (version: 4.0.0)
Lean: Reasonably up-to-date (version: 4.8.0)
Project: No open project
Active Lean version: leanprover/lean4:stable (default Lean version)
Installed Lean versions: lean4, lean4-stage0, leanprover/lean4-nightly:nightly-2024-12-12, leanprover/lean4-nightly:nightly-2025-01-27, leanprover/lean4-nightly:nightly-2025-02-05, leanprover/lean4-nightly:nightly-2025-02-12, leanprover/lean4-nightly:nightly-2025-03-19, leanprover/lean4-pr-releases:pr-release-6959, leanprover/lean4-pr-releases:pr-release-7366, leanprover/lean4:v4.11.0, leanprover/lean4:v4.12.0, leanprover/lean4:v4.13.0, leanprover/lean4:v4.13.0-rc3, leanprover/lean4:v4.14.0, leanprover/lean4:v4.15.0, leanprover/lean4:v4.15.0-rc1, leanprover/lean4:v4.16.0, leanprover/lean4:v4.16.0-rc2, leanprover/lean4:v4.17.0, leanprover/lean4:v4.17.0-rc1 ...