problems setting up a project depending on mathlib4

Stream: new members

[Kalle Kytölä]

I'd like to start learning about mathlib4 (I'm very far from being able to help with the port, but maybe I could eventually even learn enough for that). However, I have trouble setting up mathlib4 (no doubt because of my lack of computer skills). I'd appreciate a lot if someone can tell me what I'm doing wrong. I'm on a Ubuntu 16.04 (a bit old admittedly).

I'm trying to follow instructions from <https://github.com/leanprover-community/mathlib4> section "Using mathlib4 as a dependency".

Reading the warning about recent toolchains required, I started as follows:

$ elan self update
info: checking for self-updates

$ elan default leanprover/lean4:nightly-2023-02-04
info: using existing install for 'leanprover/lean4:nightly-2023-02-04'
info: default toolchain set to 'leanprover/lean4:nightly-2023-02-04'

  leanprover/lean4:nightly-2023-02-04 unchanged - (error reading lean version)

The error is not reassuring, but I was not quite sure about it, so I tried to go on.

$ lake new MyProject math
/home/kalle/.elan/toolchains/leanprover--lean4---nightly-2023-02-04/bin/lake: /lib/x86_64-linux-gnu/libm.so.6: version `GLIBC_2.27' not found (required by /home/kalle/.elan/toolchains/leanprover--lean4---nightly-2023-02-04/lib/libLLVM-15.so)

At this point I assume that I have failed to set up Mathlib4 this way. The best would be to know how to fix the elan error above, but I tried something else :grimacing:.

[Kalle Kytölä]

I decided to still try with the stable toolchain, because at least it didn't give elan errors.

$ elan default leanprover/lean4:stable
info: using existing install for 'leanprover/lean4:stable'
info: default toolchain set to 'leanprover/lean4:stable'

  leanprover/lean4:stable unchanged - Lean (version 4.0.0, commit 7dbfaf9b7519, Release)

Looks better. But of course explicitly against the warning that mathlib4 requires a more recent toolchain... Nevertheless, I boldly ran

lake new MyProject math

and got no errors and found a folder MyProject

$ ls MyProject/
lakefile.lean  MyProject.lean

I have seen others at this point also find a file lean-toolchain in this folder, so I don't know if I should be concerned.

Pretending to be unconcerned, I went on to the folder and ran:

$ lake exe cache get
info: cloning https://github.com/leanprover-community/mathlib4.git to ./lean_packages/mathlib
error: ./lean_packages/mathlib/lakefile.lean:7:2: error: unknown attribute [default_target]
error: ./lean_packages/mathlib/lakefile.lean:14:2: error: unknown attribute [default_target]
error: ./lean_packages/mathlib/lakefile.lean: package configuration has errors

So this failed. Same failure with:

$ lake build
info: mathlib: no manifest entry; deleting ./lean_packages/mathlib and cloning again
info: cloning https://github.com/leanprover-community/mathlib4.git to ./lean_packages/mathlib
error: ./lean_packages/mathlib/lakefile.lean:7:2: error: unknown attribute [default_target]
error: ./lean_packages/mathlib/lakefile.lean:14:2: error: unknown attribute [default_target]
error: ./lean_packages/mathlib/lakefile.lean: package configuration has errors

I assume the package configuration errors are a mismatch of the mathlib4 required toolchain and the stable toolchain that I have.

[Kalle Kytölä]

So I assume the issue is the elan failure at trying to install a more recent toolchain. Does this look like a correct diagnosis to people who understand computers? Does anyone have hints on how to fix the elan failure to install a more recent toolchain? Thanks in advance for any advice!

[Reid Barton]

Yes I think your old OS is preventing you from using a recent lean/lake, which is preventing you from using a recent mathlib4.

[Kalle Kytölä]

Ouch... But thanks!

I can use Lean4 and Lean3+mathlib3 on my OS, so it is a pity that mathlib4 doesn't work.

Does someone know the reason mathlib4 requires newer OS, and whether it will stay that way? Or will it eventually even be possible to use mathlib4 on Ubuntu 16.04?

[Reid Barton]

The reason is contained in your first error message, mathlib requires a new lean/lake, which requires a new LLVM, which requires a new libm, etc

[Reid Barton]

Whether it might change, I can't say.

[Reid Barton]

Considering 16.04 is no longer getting free updates, I would guess it's not a priority

[Kalle Kytölä]

...and if this is really about the whole (recent) lean-toolchain, is it likely that at some point soon Lean4 itself might no longer work on Ubuntu 16.04?

[Reid Barton]

Well, the version that works will continue to work

[Kalle Kytölä]

Sure! But "stable" might soon mean a more recent tool chain, right?

(Sorry, I have a very poor understanding of software, so I may just be totally confused.)

[Reid Barton]

Yes, I would assume so. The current "stable" version is from August

[Kalle Kytölä]

Thanks a lot for the explanations!

I will perhaps consider getting a more recent OS, but that looks like a nontrivial project to me, so for now it looks like I will just have to give up on mathlib4. :sad:

[Ruben Van de Velde]

My first step towards upgrading my os has typically been to buy a new computer, but that may not be practical :sweat_smile:

I'd still strongly recommend getting something newer than 16.04, though

[Patrick Massot]

Kalle Kytölä said:

I'm very far from being able to help with the port, but maybe I could eventually even learn enough for that.

This isn't true at all. Your Lean 3 work already makes you over-qualified for the port. We have people helping with the port that had never written a single line of Lean code (in any version) before starting their work. All you need is time.

[Mauricio Collares]

Kalle Kytölä said:

Thanks a lot for the explanations!

I will perhaps consider getting a more recent OS, but that looks like a nontrivial project to me, so for now it looks like I will just have to give up on mathlib4. :sad:

I wonder if installing elan via Nix is enough to make Lean 4 work on your computer. I would only recommend this if you have root access (nix-user-chroot exists but it's less polished), but you wouldn't need to upgrade your Ubuntu.

[Mauricio Collares]

Perhaps there is a better way to work around the glibc version issue, but I tested on an Ubuntu 16.04 VM and installing elan via Nix seems to work. If you'd like to try, you install Nix by downloading https://nixos.org/nix/install and running chmod +x install; ./install --no-daemon. Then you restart your terminal, remove your current version of elan and run nix-env -iA nixpkgs.elan.

[Kevin Buzzard]

Upgrading Ubuntu is pretty easy and you don't even need to back up your stuff, at least if you're happy to gamble

[Kalle Kytölä]

I did indeed start upgrading my OS, and it seemed easy enough (also figured 2023 is as good a time as any to upgrade an OS from 2016). I guess a person with normal computer skills would just succeed.

But I'm afraid I'm not one. I now do have a newer Ubuntu --- just unfortunately without working keyboard input, which makes it hard to use terminal to fix anything (or to do anything else).

I'm not particularly worried --- it's not my first time messing up computers and I did make backups (for the most part). But I think I'll just opt for a fresh OS install from scratch instead of fighting to fix a borked upgrade of an ancient OS in some recovery mode (in addition to keyboard, at least some third party GPU drivers did not live happily everafter). But that will have to wait until the next weekend...

I think OS upgrade is a reasonable (but not entirely trivial) option.

I was too hasty so I never got around to trying the nix solution. That seems like an interesting alternative --- thanks!