Problems with nix

Stream: general

[caralice]

Not sure if this is the right place to ask. I wanted to try Lean and decided to start with mathematics_in_lean. So I was following installation instructions and after running lake exe cach get got this:

info: mathlib: cloning https://github.com/leanprover-community/mathlib4 to './.lake/packages/mathlib'
info: std: cloning https://github.com/leanprover/std4 to './.lake/packages/std'
info: Qq: cloning https://github.com/leanprover-community/quote4 to './.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to './.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to './.lake/packages/proofwidgets'
error: ./.lake/packages/proofwidgets/lakefile.lean:6:2: error: 'buildArchive' is not a field of structure 'Lake.PackageConfig'
error: ./.lake/packages/proofwidgets/lakefile.lean: package configuration has errors

I was unable to find anything regarding that buildArchive issue. What should I do?

[Kevin Buzzard]

So

git clone https://github.com/leanprover-community/mathematics_in_lean.git
cd mathematics_in_lean/
lake exe cache get

works fine for me. Is this what you did? If so, what is the output of elan show? If you only just installed Lean then you might want to reboot or something, delete your previous attempt to install #mil completely, and then try again.

[Kevin Buzzard]

FWIW my elan show output is

$ elan show
installed toolchains
--------------------

leanprover/lean4:nightly-2023-08-19
leanprover/lean4:nightly-2024-02-01
leanprover/lean4:stable
leanprover/lean4:v4.3.0
leanprover/lean4:v4.3.0-rc2
leanprover/lean4:v4.4.0
leanprover/lean4:v4.5.0
leanprover/lean4:v4.5.0-rc1 (default)
leanprover/lean4:v4.6.0-rc1

active toolchain
----------------

leanprover/lean4:v4.5.0-rc1 (default)
Lean (version 4.5.0-rc1, commit b614ff1d12bc, Release)

[caralice]

I installed Lean with nix (nixpkgs.lean4) so I do not have elan. Is elan a hard requirement?

[Kevin Buzzard]

I'm sorry, that question is beyond my pay grade -- I have no idea what nix is. Your error seems to indicate some mismatch with lean versions and elan is precisely the tool which sorts this sort of thing out.

[caralice]

# mathematics_in_lean on  master [!+] via ❄  impure (nix-shell-env)
; lake --version
Lake version 5.0.0-v4.5.0 (Lean version 4.5.0)

# mathematics_in_lean on  master [!+] via ❄  impure (nix-shell-env)
; lean --version
Lean (version 4.5.0, commit v4.5.0, Release)

[Shreyas Srinivas]

caralice said:

I installed Lean with nix (nixpkgs.lean4) so I do not have elan. Is elan a hard requirement?

Nix packages seem to be maintained by a handful of nix enthusiasts. Elan is the textbook tool for handling toolchain installations. I recall @Joachim Breitner knows a lot about nix.

[Shreyas Srinivas]

that being said, your problem is not caused by not having elan.

[Shreyas Srinivas]

Try deleting ./lake-manifest.json and running lake exe cache get! again.

[Shreyas Srinivas]

MIL is currently on toolchain 4.6.0-rc1

[caralice]

Shreyas Srinivas said:

caralice said:

I installed Lean with nix (nixpkgs.lean4) so I do not have elan. Is elan a hard requirement?

Nix packages seem to be maintained by a handful of nix enthusiasts. Elan is the textbook tool for handling toolchain installations. I recall Joachim Breitner knows a lot about nix.

Well AFAICS elan is not unlike rustup which does a good job managing toolchains by itself but its functionality is better covered by a package manager. While managing Rust versions on, say, Arch Linux without rustup is expected to be hard, Nix has an overlay that removes the need in rustup.
Anyway, I'd expect everything to work fine on a single version.

[Shreyas Srinivas]

So if you are inside the MIL folder and getting toolchain 4.5.0, I think that's where the trouble is

[Shreyas Srinivas]

Regardless of the systemwide toolchain, the toolchain inside a project is fixed by the lean-toolchain file

[caralice]

Shreyas Srinivas said:

MIL is currently on toolchain 4.6.0-rc1

Alright, I'll try using that.

[Shreyas Srinivas]

Is nix overriding the default toolchain that lake uses in a project folder by presenting only v4.5.0? Can it even do that? I would be extremely surprised if nix could do such things and lake wasn't demanding the toolchain of the project folder or alternatively just giving up.

[Shreyas Srinivas]

I am surprised by this output. Did you by any chance clone mathematics_in_lean into a folder that already has a lean-toolchain file?

caralice said:

# mathematics_in_lean on  master [!+] via ❄  impure (nix-shell-env)
; lake --version
Lake version 5.0.0-v4.5.0 (Lean version 4.5.0)

# mathematics_in_lean on  master [!+] via ❄  impure (nix-shell-env)
; lean --version
Lean (version 4.5.0, commit v4.5.0, Release)

[Kim Morrison]

(I think it would be good if we were more emphatic in suggesting that new Lean users do not use Nix. :-)

[Shreyas Srinivas]

Scott Morrison said:

(I think it would be good if we were more emphatic in suggesting that new Lean users do not use Nix. :-)

alternatively we could create a stream for nix users and enthusiasts and direct nix questions there. I understand why people get excited about nix and in some sense we are re-inventing the wheel with lake and elan. Creating a separate stream allows nix enthusiasts to help each other while also making it very clear that nix is currently a niche with no official support.

[Chris Henson]

I would note that, while probably not what most nix users would prefer, you can use elan within a nix shell pretty painlessly (elan is on nixpkgs already).

While Lean + Nix is definitely a niche, I'd guess there are a few of us out here! I would definitely support @Shreyas Srinivas's idea of a nix stream. I'm not a nix expert either, but would be interested in seeing if there's enough interest to develop more support.

[Patrick Massot]

I renamed the thread since it has nothing to do with mathematics in Lean and this will be easier to find.

[Joachim Breitner]

Scott Morrison said:

(I think it would be good if we were more emphatic in suggesting that new Lean users do not use Nix. :-)

Well, by all means, do use nix (I certainly do), but do it to obtain elan (which is included in nixpkgs and works in a nix shell), and take it from there. That's what I do.

As soon as there are actual applications written in lean that need to be packaged for end users we need a better story. Until then, this is the best advice I can give to people wanting to use lean.

[Sebastian Ullrich]

Yes, it is no different than any other distribution in that respect

[Shreyas Srinivas]

How does one get a new stream created for nix users?