community "Creating a lean project" instructions

Stream: general

[Kevin Buzzard]

The instructions for creating a lean project on the community website here always struck me as weird, because they tell you to install something from April 2024 and have this line about how you shouldn't worry about it all. I recently created a new Lean project following the instructions on lean-lang.org and I never had to use the command line at all, or ever mention April 2024. Should the community pages just be directing users to lean-lang for installing projects nowadays? I know that some people would prefer command line instructions, but conversely I know many that wouldn't (including essentially all Windows users, who might only have a very dismal command line installed by default) and many find their way to the community via the community pages rather than the lean-lang ones. IIRC the community pages were written when there was no GUI-only way to create a new project but things have since moved on.

[Kevin Buzzard]

My proposal:
1) the community pages should have as first option for creating a new project a GUI-only version and a link to lean-lang.
2) We should also keep the command-line-only installation instructions for the hardcore, but the reference to April 2024 (which will only get weirder and weirder as time goes on) should be replaced with something like:

a) check your elan is up to date with elan self update
b) check your default lean is sensible e.g. with elan default leanprover/lean4:stable
c) create a new project with lake new my_project math

Would a PR to the community website implementing this be welcome?

[Mario Carneiro]

steps a and b can be skipped for those that have just installed lean for the first time

[Mario Carneiro]

ideally we would only have step c, but this has not always been the case

[Mario Carneiro]

if you were to get the latest now and then run step c in a year without a/b first it will work

[Patrick Massot]

Yes, it would be really nice to clean up this mess. But whenever we try to do that we hit a new lake weirdness.

[Kevin Buzzard]

In fact, I see that now https://leanprover-community.github.io/get_started.html starts with a pointer to the official lean instructions. My proposal is that we should highlight this more clearly, and also start https://leanprover-community.github.io/install/project.html with a similar pointer.

[Mario Carneiro]

I think the point is that the community instructions currently have more weirdness than current lake stable

[Mario Carneiro]

The april 2024 reference was supposed to be updated whenever anything affecting lake new changed

[Mario Carneiro]

I don't think we can be trusted to track this

[Kevin Buzzard]

It seems to me that the big problem with lake is/was that it is (presumably) written in Lean and that lean has been moving so fast in the last couple of years that anyone with an old version of lean is kind of doomed to have problems. This is the source of many lake problems (e.g, Yael and me both complaining to Mac yesterday that lake is still creating projects with lakefile.lean instead of lakefile.toml and this is just because our default toolchains were old). But we might optimistically hope that such problems are in the past now (certainly there are far far fewer complaints about lake on this forum than a year ago, indeed there is very little lake chat nowadays) and so maybe it's time to make a "once and for all" change to the community website which now pushes users to the lean-lang website rather than telling them to use a command line, which I am convinced that most of our mathematician users probably don't want to do. There is now a pain-free way to make a new lean project involving just point and click and this way is clearly explained on the official website. That was most definitely not always the case, and the community website helped an entire generation of new users, but things have moved on now.

[Mario Carneiro]

I think we should keep hosting setup instructions, because we want to be able to adapt to lake weirdness

[Mario Carneiro]

but that only works if we keep our setup instructions up to date

[Patrick Massot]

I completely agree that we need to do something here.

[Patrick Massot]

Feel free to open a PR to the community website!

[Mario Carneiro]

right now you can use either CLI or non CLI options

[Mario Carneiro]

and I think we should document both

[Mario Carneiro]

The setup instructions have this:

• Go inside the my_project folder and type lake update.
  • Windows users seeing a curl: (35) schannel: next InitializeSecurityContext failed error should read this note.

It is notes like that which make me think that it is worthwhile to maintain community instructions. The lean-lang quickstart has no such notes, and I think they would be very unlikely to add one because they don't want lean to look bad

[Marc Huisinga]

Mario Carneiro said:

and I think they would be very unlikely to add one because they don't want lean to look bad

This is documented in the setup guide in the "Troubleshooting" entry.

[Mario Carneiro]

it's not on the website

[Marc Huisinga]

... But the website directs users to the setup guide?

[Mario Carneiro]

it seems the quickstart is not self contained at all, it's deferring to the in-vscode guide

[Mario Carneiro]

what if I want to read it on a webpage and/or I'm not using vscode?

[Mario Carneiro]

it's certainly nice to have a vscode setup guide but I want a website setup guide too

[Mario Carneiro]

they can even have the same text

[Marc Huisinga]

Improvements to our website in this regard are coming soon-ish :-)

[Marc Huisinga]

In any case, the claim you made that we don't document this in the quickstart guide (which is intended as an easy setup for most users) and that we would be very unlikely to add it is demonstrably false. If you want to provide an "easy path" towards getting a Lean project set up on the community website, then this shouldn't have to be a concern for you.

[Kevin Buzzard]

@Marc Huisinga what is the "setup guide"? I see two different links

https://docs.lean-lang.org/lean4/doc/quickstart.html
https://lean-lang.org/documentation/setup/

I'm making a PR to the community website. What exactly should I be pointing people to?

[Marc Huisinga]

The setup guide is the platform-specific guide in VS Code that step 3 of the quickstart guide points to.

[Kevin Buzzard]

Is the second link I post above now deprecated? I've just also found
https://docs.lean-lang.org/lean4/doc/setup.html which looks very similar to the second link but it doesn't have broken links.

[Marc Huisinga]

I'd say that the latter is preferred to the former, I think it was just copied over carelessly. I'll ping the responsible people about it.

[Kevin Buzzard]

I created a thread in #lean4 when I was being confused about this half an hour ago

[Mario Carneiro]

is it possible to link to the vscode setup guide? Like some kind of vscode:// link that actually opens the page?

[Marc Huisinga]

Mario Carneiro said:

is it possible to link to the vscode setup guide? Like some kind of vscode:// link that actually opens the page?

vscode-lean4#596

[Kevin Buzzard]

Does this work: vscode://leanprover.lean4/setup-guide

[Kevin Buzzard]

PR to the community guide which now more aggressively points users to the lean-lang instructions:
https://github.com/leanprover-community/leanprover-community.github.io/pull/621

[Marc Huisinga]

Kevin Buzzard said:

Does this work: vscode://leanprover.lean4/setup-guide

Zulip's linkifier doesn't appear to like the URI, but you can also just paste it into your browser address bar to test it

[Mario Carneiro]

[vscode://leanprover.lean4/setup-guide](vscode://leanprover.lean4/setup-guide)

[Sebastian Ullrich]

I just noticed that https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency may also want to be "upgraded" to refer to the Setup Guid/extension menu first, before the cmdline instructions