Zulip Chat Archive

Stream: new members

Topic: install for nixos

Luca Maio (Sep 19 2023 at 12:47):

Hey, maybe I am also just being really dumb but installing lean4 and especially mathlib with it has been giving me some trouble, so I thought maybe someone else who also uses NixOS could tell me the best way to do that on NixOS (I am not an expert on NixOS yet). I tried to follow the instructions from the "Nix Setup" page inthe documentation, but the resulting installation kept giving me errors and at least the vs-code extension did not work with it. Thank you in advance!

Mauricio Collares (Sep 19 2023 at 13:03):

Just install elan (yes, elan, not lean) from Nixpkgs and let it handle everything else. For example, to tinker with mathlib, just git clone https://github.com/leanprover-community/mathlib4 and run lake exe cache get inside the mathlib directory. This will automatically fetch the correct version of Lean.

Luca Maio (Sep 19 2023 at 13:07):

Okay, I have installed the elan package, I ran elan install leanprover/lean4:stable but if I then try things like lake init or what you suggested I only get $ command failed 'lake' with os error 2

Luca Maio (Sep 19 2023 at 13:08):

elan toolchain list also shows that lean4 is supposedly installed.

Mauricio Collares (Sep 19 2023 at 13:11):

Not sure what is going on. Can you try removing ~/.elan and running lake init again? Also, what does elan --version say?

Mauricio Collares (Sep 19 2023 at 13:12):

3.0.0 would be ideal, but maybe you're running nixos 23.05 instead of unstable

Luca Maio (Sep 19 2023 at 13:12):

elan --version says 3.0.0

Mauricio Collares (Sep 19 2023 at 13:13):

If removing the elan folder does not work, try running elan default stable as well

Luca Maio (Sep 19 2023 at 13:16):

Okay, after elan default stable (also deleted .elan before, which did not help), now the error is toolchain 'stable' does not have the binary '<path>/bin/lake'

Luca Maio (Sep 19 2023 at 13:17):

Also, I think that this now installed lean 3 right?

Luca Maio (Sep 19 2023 at 13:17):

At least it said latest update on stable, lean version v3.51.1

Luca Maio (Sep 19 2023 at 13:18):

Or is this just an internal version of lean4?

Mauricio Collares (Sep 19 2023 at 13:18):

Weird, I thought stable defaulted to Lean 4 on elan 3.0.0

Luca Maio (Sep 19 2023 at 13:19):

Changed stable to leanprover/lean4:stable and now lake seems to work!

Luca Maio (Sep 19 2023 at 13:19):

Thank you!

Mauricio Collares (Sep 19 2023 at 13:23):

That's great! But I think https://github.com/leanprover/elan/pull/98 (available in elan 3.0.0) should have made leanprover/lean4 the default origin, so there's something strange happening still.

Mauricio Collares (Sep 19 2023 at 13:24):

But you don't need to be the one to debug it, of course.

Luca Maio (Sep 19 2023 at 13:24):

Ah, okay, now (probably after deleting the .elan folder) the version shows 1.4.5

Luca Maio (Sep 19 2023 at 13:26):

So apparently my elan got downgraded in the process, which is weird in and of itself, but that is probably somewhere on my end ...

Luca Maio (Sep 19 2023 at 13:26):

Cause I swear it said 3.0.0 earlier!

Mauricio Collares (Sep 19 2023 at 13:27):

Ok, I see! You had two installed Elans: NixOS 23.05's version of elan, and a user installation of elan (I assume you ran the curl | sh install script) on ~/.elan. The latter didn't come from Nixpkgs and it does not work on NixOS, because the Nixpkgs version of elan patches the downloaded toolchains to work on NixOS. Without patching, you'll get errors like the os error 2 you mentioned above.

Luca Maio (Sep 19 2023 at 13:28):

Aaaaaaah, okay thank you very much vor the explaination!

Luca Maio (Sep 19 2023 at 13:29):

Is there a possible problem with "only" having elan 1.4.5?

Ruben Van de Velde (Sep 19 2023 at 13:29):

Well, it defaults to lean 3, for one :)

Mauricio Collares (Sep 19 2023 at 13:32):

Other than defaulting to Lean 4, there was one other convenient feature added: REPO:lean-toolchain now refers to "the version of Lean REPO currently uses". You're fine with 1.4.5. I'm sure if there's a breaking change to elan people will backport it to NixOS stable.

Mauricio Collares (Sep 19 2023 at 13:40):

By the way, if you plan to create a project that uses mathlib, use lake new my_project_name math to create it. The extra "math" argument adds the required lines to the lakefile and ensures the used toolchain matches mathlib's.

Luca Maio (Sep 19 2023 at 13:57):

Mauricio Collares said:

By the way, if you plan to create a project that uses mathlib, use lake new my_project_name math to create it. The extra "math" argument adds the required lines to the lakefile and ensures the used toolchain matches mathlib's.

Ah that's very good advice, thank you!

Luca Maio (Sep 19 2023 at 13:58):

Mauricio Collares said:

Other than defaulting to Lean 4, there was one other convenient feature added: REPO:lean-toolchain now refers to "the version of Lean REPO currently uses". You're fine with 1.4.5. I'm sure if there's a breaking change to elan people will backport it to NixOS stable.

Okay, thanks for the Info!

Last updated: Dec 20 2023 at 11:08 UTC