Trouble installing lean4

Stream: lean4

[Ali Ramsey]

Hi, sorry if this isn't the right place to ask, but I'm having a lot of trouble installing lean4. I've following the instructions on https://leanprover-community.github.io/install/windows.html, and I've downloaded the lean4 extension on VSCode, but this is what I see when I try to test it
Screenshot-714.png

I also tried cloning https://github.com/PatrickMassot/GlimpseOfLean to go straight to solving the exercises, but I just get the errors below:

Screenshot-712.png

When I installed Lean 3 just over a year ago I didn't have any problems with it, and was able to jump right into solving exercises, so I'm not sure what I've done wrong this time!

[Alex J. Best]

This is a strange looking error. Everything looks ok with the lean version and directory. but the error message is saying something odd about git

[Alex J. Best]

What happens if you run lake build in the GlimpseOfLean directory on the command line? (or terminal window in vscode)

[Ali Ramsey]

It took about 3hrs to build everything, but that seems to have fixed it -- thank you! Out of interest, is there something I missed in the installation?

[James Gallicchio]

Probably not. The language server was likely in some weird state and building everything kicked it out of that weird state :p
if there's ever an issue with the language server, restarting it is usually a good call (Control+Shift+P, then search for "Lean4 restart")

[James Gallicchio]

also @Patrick Massot maybe the GlimpseOfLean readme should mention lake exe cache?

[Patrick Massot]

I don see why it would refer specifically to this step since it refers to the whole installation instructions set.

[Scott Morrison]

Because people skip it and forget it? I think until we have it integrated into lake build the more reminders the better.

[Utensil Song]

Although I had known about lake exe cache from zulip, when I'm in a new environment (Github Codespaces in my case) and looking for just a full instruction set containing a few commands to execute for adding mathlib as a dependency without hours of build time, the experience was frustrating (I tried the following in order from the top of my head):

1. Mathlib README: https://github.com/leanprover-community/mathlib4#installation redirects to https://leanprover-community.github.io/get_started.html where is a manual installation that mentions nothing about lake exe cache for all OSes
2. Lean 4 manual: https://leanprover.github.io/lean4/doc/quickstart.html which lets VSCode Lean 4 extension to do the installing but if I wish to execute lake commands, by default I'll have to realize that it's not in the PATH yet, and starting a new terminal in VS Code would not add it to the PATH, I have to do manual export, source or using bash -l etc. Of course, it also mentions nothing about lake exe cache because the manual is for pure Lean 4 not Mathlib4-based Lean 4 projects.
3. Then following some tutorial or game projects that use mathlib4 already might be good enough? unfortunately, I picked https://github.com/djvelleman/HTPILeanPackage which is a great book for reading, but its lakefile here is specifying the lib source different from, e.g. https://github.com/bridgekat/filter-game, which would end up compile Mathlib every time even after I executed lake exe cachesuccessfully (I haven't figure out why yet)
4. Go back to Mathlib4 doc I found a separate https://github.com/leanprover-community/mathlib4#downloading-cached-build-files below that mentions lake exe cache but didn't help me resolve issues encountered in step 3
5. Reread Mathlib4 doc: I found another separate link below at https://github.com/leanprover-community/mathlib4#using-mathlib4-as-a-dependency pointing to Mathlib4 wiki, which eventually became a lifesaver to guide me to create a new project depending on Mathlib4, I managed to get the new project working with effective Mathlib4 cache, then I got to realize what went wrong in step 3 and got the original code base working
6. I also encounter issues related to Lean toolchain versions to realize that I need to use the toolchain as the one Mathlib4 is using, again I was copy-pasting Lean toolchain versions from some tutorial or game projects, so it's either incompatible with lake or mathlib4
7. There's also another annoying issue during the process, I need to open a Lean file in VS Code to activate the Lean 4 extension to install Lean toolchain, but then it would start the Lean server which is something like lake serve, but of course at the moment I haven't execute lake exe cache get yet, so it's recompiling Mathlib4 from scratch, so I have to stop lean server, but again, I have to remove the lake build lock to do my own lake build to verify whether it picks up Mathlib4 cache and keep trying. This is also known as the server for the editor and lake on the command line fight each other.

During the experience, the wiki link in step 4 is most helpful, but it's not easy to notice it because I was redirect away from Mathlib4 readme in step 1 .

I hope my experience could be useful as a case study to improve the doc about how to install Lean 4 to use Mathlib4. I might be a little silly and sloppy when I read the docs, but it's easy to make these mistakes as I was directed around by readmes, manuals, books and tutorial/game projects. The instructions are scattered, pointing to different places and it's up to the user to piece things together.

(A little background: I was familiar with Lean 3/Mathlib3 setup and pure Lean 4 setup around a year ago, but until recently I haven't got the chance to familiarize myself with Mathlib4 steup )

[Scott Morrison]

1. The instructions at https://leanprover-community.github.io/get_started.html haven't actually opened any projects yet, so lake exe cache get is irrelevant. When you click the "Lean projects" link it then tells you about lake exe cache get.

I suspect the problem here is that people don't realize they need to click "Lean projects". Perhaps someone could add a big banner at the bottom of that page: "Next step: set up a Lean project"?

[Utensil Song]

After reading your message and check the getting started page again, this is the first time I realize this sentence is right below all the links for all the OSes:

After this installation procedure, it is crucial to read how to start or get a Lean project. <- link here

But I was directed away from this page for the specific OS, like I was direct away from Mathlib4 README. The reading stream is broken, and for someone haven't got the big picture of all steps, it could be an obstacle.

(EDIT: I just noticed that for each OS, it mentions Lean projects at the bottom, now I truly have no excuse :joy: )

[Scott Morrison]

We are working on making lake exe cache get unnecessary (i.e. it will be an opt-out automatic action when you lake build), since we're realising instructions are hard. :-)