Kabelo Moiloa

Stream: new members

[Kabelo Moiloa]

Hey everyone! I'm a pure maths undergraduate in my final year (so called "Honours," in South Africa) with a long term interest in type-theoretic foundations for maths from the SICP book and the HoTT Book.

[Kabelo Moiloa]

I'm having trouble using mathlib4 as a dependency on any new projects. I use nix to get lean4 from the nixpkgs-unstable channel. I'm able to run nix-shell -p lean and within this shell to run lake new foo && cd foo && lake build. The binary foo is produced successfully and the command .lake/build/bin/foo runs and gives me the output "Hello World" as desired.

[Ruben Van de Velde]

It will likely be easier if you install elan as suggested on our website: https://leanprover-community.github.io/get_started.html
and then follow the instructions on the wiki: https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency

[Kabelo Moiloa]

@Ruben Van de Velde, I doubt it but I shall try. I use Guix System, which doesn't comply with the FHS standard.

[Kevin Buzzard]

Just to warn you -- if you are using an unsupported set-up then you might find it much harder to get help here; it's hard enough trying to support people who are using the supported (elan) set-up! Another thing you should probably be warned about -- if you're not using elan then you will probably have to compile mathlib4 yourself because the cache will not be valid for your set-up, and this takes hours.

[Kabelo Moiloa]

Got it, thanks @Ruben Van de Velde and @Kevin Buzzard. So now, I'm following the standard elan setup but I now can't run any lake commands at all. I get the following error:

error: command failed: 'lake'
info: caused by: No such file or directory (os error 2).
```. Lean itself works though, I can create a file `test.lean` and run `#eval 2+2` and get e.g. `4` in the infoview.

[Kevin Buzzard]

Is this a path issue?

[Kevin Buzzard]

Lake is in ~/.elan/bin for me on Ubuntu. Is it a case of "log out and log in again so that your .profile, which was updated by elan, actually gets run"?

[Kabelo Moiloa]

Kevin Buzzard said:

Lake is in ~/.elan/bin for me on Ubuntu. Is it a case of "log out and log in again so that your .profile, which was updated by elan, actually gets run"?

Nope it is a relatively obscure (i.e. definitely obscure for mathematicians, but not at all for sysadmins) issue that affects NixOS and the quite similar Guix System. Thanks for the help everyone, but I think the best way for me to proceed is to build everything from source. Probably will try to do this over the weekend or similar.

[Julian Berman]

There definitely are existing users who are on nixOS -- what is type -a lean?

[Julian Berman]

And in whatever directory that returns, there's no lake in it?

[Kabelo Moiloa]

Julian Berman said:

There definitely are existing users who are on nixOS -- what is type -a lean?

Alright, I think I'm making progress. I'm using nix-shell -p elan to get elan -- the curl | sh method doesn't work because the usual build of elan assumes that your distro is FHS compliant (so that e.g. binaries can be found in /usr/bin, etc.). I can build the Mathematics in Lean repo simply by cloning it and running cd mathematics_in_lean followed by lake build. Everything builds successfully.

However, when I open emacs with lean4-mode installed, I then get something like this when I open MIL/C02_Basics/S01_Calculating.lean I get the following error:

/nix/store/syfqdchrnlrfq44svbjmfld1zfhzmqcc-lean4-4.2.0/bin/lake print-paths Init MIL.Common Mathlib.Data.Real.Basic
error: ./lakefile.lean:5:2: error: 'leanOptions' is not a field of structure 'Lake.PackageConfig'
error: ./lakefile.lean: package configuration has errors

[Kevin Buzzard]

That looks like a lean version mismatch somewhere. Is your lean-toolchain file compatible with the version of lean which the version of mathlib used by MIL is using?

[Kabelo Moiloa]

Kevin Buzzard said:

That looks like a lean version mismatch somewhere. Is your lean-toolchain file compatible with the version of lean which the version of mathlib used by MIL is using?

The lean-toolchain file that is at the root of MIL and the one in .lake/packages/mathlib (EDIT: removed the erroneous .lean file extension for the mathlib directory) have the same contents.

[Kabelo Moiloa]

Hooorah! I have a working environment, @Kevin Buzzard your last tip was particularly helpful. Effectively, I had to clear a variable in my editor to get the lean plugin to use the correct version of lean. Thanks all much appreciated.

[Quinn]

my take is to not use nix-shell -p lean, but use nix-shell -p elan

[lorã]

my take is to not use nix-shell -p lean, but use nix-shell -p elan

@Quinn

Ty!! ur comment saved my life <3