Problems installing lean

Stream: lean4

[Dominic Steinitz]

I am hoping to use lean to show the equivalence between a connection on a principal bundle and the Yang-Mills field (the pullback via a section on to the base manifold) but I can't even install lean. I've followed the instructions here https://leanprover-community.github.io/install/project.html but get

[nix-shell:~/Dropbox/Tidy/DifferentialGeometry/mathematics_in_lean]$ lake exe cache get
lake exe cache get
error: ././.lake/packages/mathlib/lakefile.lean:10:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:11:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:12:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:13:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean:14:7: error: unexpected token; expected identifier
error: ././.lake/packages/mathlib/lakefile.lean: package configuration has errors

[Julian Berman]

(Welcome.) Which were the instructions you followed for installing Lean itself? That page is for "step 2". Were they https://leanprover-community.github.io/install/linux.html, or did you follow something nixOS specific? Also can you show us what lake --version says in that directory?

[Yann Herklotz]

I believe this happens if the version of Lean in your local repo does not match the one in Mathlib. Try making sure that your local lean-toolchain file in the root of your repository matches that of https://github.com/leanprover-community/mathlib4/blob/master/lean-toolchain (for your version of Mathlib that you have in lakefile.lean). There is some more documentation here: https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency.

[Julian Berman]

Dominic has cloned the #mil repo it would seem, so I think you're right that it means the version doesn't match, but the fix is very unlikely to be changing the lean-toolchain file unless the plan really is to work on MIL (which it sounds like it isn't, it's just a test project?). The fix will likely be that Dominic should be following the instructions saying to install elan :)

[Yann Herklotz]

Ah OK I wasn't familiar with #mil, and I see now that it's a nix shell! So yes installing elan first and then it should pick up the right version from the #mil repo (or one can create a new repo).

[Dominic Steinitz]

[nix-shell:~/Dropbox/Tidy/DifferentialGeometry/mathematics_in_lean]$ lake --version
lake --version
Lake version 5.0.0-v4.9.0 (Lean version 4.9.0)

[Dominic Steinitz]

Should I not have run nix-shell -p lean4? I just wanted to try lean before committing to a more permanent installation.

[Yann Herklotz]

Mathlib and #mil seem to require Lean 4.12.0-rc1. Lean changes quite a lot with each version, and using something like elan will automatically use the right version for the project. It should be easy to uninstall as well, I believe it is just installed under ~/.elan, so removing that directory will remove lean.

[Patrick Massot]

I am afraid the general answer is that nixOS isn’t supported. You can search for many previous discussions about this, and they are always very painful.

[Patrick Massot]

More generally, refusing to use elan is not supported. There are simply not enough resources to support such requirements.

[Dominic Steinitz]

:-( homebrew did not seem to work either

[Sebastian Ullrich]

Using elan from NixOS is absolutely supported, but using lean4 from it directly is not recommended for these reasons

[Patrick Massot]

It’s the same issue. There is a one line installation procedure explained at https://leanprover-community.github.io/install/macos.html. You are free to insist on using homebrew, but you are on your own. This isn’t a moral judgement at all, we have a lot to do and not enough time to support non-recommended setups.

[Dominic Steinitz]

Here we will discuss the fast way, assuming a lot of trust from you.

I will hold back for now but thanks very much for the help and support :-)

[Patrick Massot]

Note you don’t have to trust us, you can also inspect https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_macos.sh before running it.

[Patrick Massot]

and recursively inspect https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh

[Dominic Steinitz]

I don't trust myself is the problem. I will go and look at the script.

[Mauricio Collares]

Sebastian Ullrich said:

Using elan from NixOS is absolutely supported, but using lean4 from it directly is not recommended for these reasons

i.e. just run nix-shell -p elan and lake exe cache get should work fine in the resulting shell

[Mauricio Collares]

(although I don't use nix on Darwin, so I can't be sure)

[Dominic Steinitz]

Thank you all - in the end I installed using the one line installation procedure and it now appears to be working via emacs.