Linux setups

Stream: lean4

[antonio]

I have just installed Lean 4 in my Arch Linux with:

yay -Syu elan-lean
elan default leanprover/lean4:nightly

but I can't find lake? Any suggestion?

[Marc Huisinga]

Does updating elan via elan self update help?

[Adam Topaz]

Would that install a new version of elan in $HOME/.local/bin/ (or somewhere else in the home folder)?

[antonio]

 >>> elan self update

error: self-update is disabled for this build of elan
error: you should probably use your system package manager to update elan

[Adam Topaz]

@antonio this message was posted in the wrong thread. You can change the title of the thread to your message to move it.

[Marc Huisinga]

I think the version in AUR should be sufficiently up-to-date to include lake anyways. elan -V yields the version if you want to check.

[Adam Topaz]

I'm on arch, and I installed elan with the official script, not via aur. It might be worthwhile trying that.

[antonio]

Sorry @Adam Topaz
btw I have a $HOME/.elan/toolchains/leanprover--lean4---nightly

[antonio]

and there is a lake in bin

[antonio]

but it is not linked to the path

[Marc Huisinga]

Usually the official script does that by default, but the AUR version probably doesn't. Should be fine if you add it yourself

[antonio]

elan --help says

elan manages your installations of the Lean theorem prover.
It places lean and leanpkg binaries in your PATH that automatically select

Not lake. It may be my elan is too old .

[antonio]

~ >>> elan --version
elan 1.3.1 (26ce65531 2021-11-11)

[Mauricio Collares]

I think line 23 of the PKGBUILD just needs to be updated.

[Marc Huisinga]

antonio said:

~ >>> elan --version
elan 1.3.1 (26ce65531 2021-11-11)

That's the recent version, I think if you add elan's bin folder to your PATH it'll work

[antonio]

export PATH="$HOME/.elan/toolchains/leanprover--lean4---nightly/bin:$PATH"

[Marc Huisinga]

There should be a $HOME/.elan/bin too where the binaries that elan manages reside (this way lean or lake will refer to the version managed by elan, not the concrete nightly version you just installed)

[antonio]

@Marc Huisinga but $HOME/.elan/bin is empty

[Marc Huisinga]

Hm. It shouldn't be :sweat_smile:
One easy solution to all this is to remove the AUR version you've installed and use https://github.com/leanprover/elan#manual-installation instead, which should hopefully work.

[antonio]

BTW

lake new hello
cd hello

works and opening Hello.lean in Emacs (with lean-mode) shows the code highlighted

[Marc Huisinga]

Yup, after adding .elan/toolchains/leanprover--lean4---nightly/bin to your path the commands will work, but it's one specific version that you downloaded via elan. The purpose of elan is to manage lean versions for you. E.g. if a project says that it works with a specific version, elan will automatically download and install that version for you and use that binary locally for that project. Ideally, for everything to fully work, it should use the .elan/bin directory (it contains links to the "real" binary for the specific version of the project in the toolchain directory), which doesn't seem to contain anything for some reason for you. But the manual install version should do this correctly.

[antonio]

Got your point! Do you perhaps use Emacs elan-mode?

[Mauricio Collares]

To fix this using the AUR version, it suffices to mimic the PKGBUILD. That is, add a symlink to /usr/bin/elan named "lake" somewhere in your path. Elan will take care of the rest.

[Marc Huisinga]

antonio said:

Got your point! Do you perhaps use Emacs elan-mode?

I used Emacs lean4-mode before the lean4 VSCode extension existed :grinning:

[antonio]

@Mauricio Collares
thanks, it works like a charm

[antonio]

@Mauricio Collares is there a separate procedure for installing Mathlib?

[Mauricio Collares]

antonio said:

Mauricio Collares is there a separate procedure for installing Mathlib?

Every other poster in this thread is more qualified to answer this than I am, but I'll try to answer anyway :) You should install https://aur.archlinux.org/packages/python-mathlibtools/ and then use leanproject to fetch mathlib along with its precompiled oleans, saving many hours of CPU time. See https://leanprover-community.github.io/leanproject.html for details.

(The connection to elan is the following: Mathlib contains a leanpkg.toml file which is automatically read by elan to provide the correct toolchain, which is useful because the oleans are tied to the version they were generated with.)

[Mauricio Collares]

You can also clone mathlib manually and use leanproject to just fetch the oleans, if you prefer.

[Mac]

@Mauricio Collares, @antonio may be talking about mathlib for Lean 4, not Lean 3, especially since he just got finished installing Lean 4.

[Marc Huisinga]

Mac said:

Mauricio Collares, antonio may be talking about mathlib for Lean 4, not Lean 3, especially since he just got finished installing Lean 4.

Or it's the other way around and they really want Lean 3 together with the real mathlib :)

[Marc Huisinga]

In any case, for Lean 3 and mathlib the leanprover-community site is a great place to start. Mathlib for Lean 4 is still very much a work in progress.

[Mauricio Collares]

@Mac Ah, yes, good point! @antonio I should've mentioned that the full-blown mathlib only exists for Lean 3 at this point. It is being ported to Lean 4, but IMO you should only use mathlib4 if you're really interested in helping with porting, or want to have a very early sneak peek. If you want to do mathematics, you should stick with Lean 3 for a little longer :)

[Mauricio Collares]

Elan handles the transition seamlessly. "lean" will run Lean 3 if that's the version specified in leanpkg.toml, so you should be good to go if your plan is to use the main mathlib.

[antonio]

@Mauricio Collares, so no more lake but leanpkg with lean3?

[Arthur Paulino]

@antonio It depends on what you want to do. Do you want to play inside mathlib code or do you want to use mathlib to build something else (using mathlib as a dependency)?

[antonio]

@Arthur Paulino well, I would like to do things with set theory, and I am interested to create something similar to this project https://github.com/asouther4/lean-social-choice

[Mauricio Collares]

Then you'd probably use leanproject (which uses leanpkg internally) and Lean 3, so you can use mathlib theorems. Lake only supports Lean 4. https://leanprover-community.github.io/toolchain.html is a good explanation of how it all fits together.

[Mauricio Collares]

But please read the warning at the top of this last page! To reiterate it, if you just want to know how to do package management, https://leanprover-community.github.io/leanproject.html is the page you should be reading, not the Toolchain one. The Toolchain page is more of a deeper dive, but I figured it would help clarify the lake/leanpkg/leanproject choice.

[antonio]

yay -Sy leanproject

worked

[antonio]

elan default leanprover/lean3:nightly

does not work, and I can't find instruction for Lean3

[Mauricio Collares]

A valid lean3 version is leanprover-community/lean:3.35.1, for example.

[antonio]

perfect, thanks

[Anders Christiansen Sørby]

Lake can also be loaded with nix flakes nix run github:leanprover/lake or installed in your profile with nix profile install github:leanprover/lake. Flakes is still experimental though.

[Sebastian Ullrich]

No, this is not a reasonable alternative, so please don't advertise it. The only lean and lake executables that correctly interpret projects' lean-toolchain files currently are elan's.

[antonio]

As I understand, I can't use Lean4, because I cannot do actual mathematics without Mathlib library. At this point, where can I find the Lean3 docs? The official site only mentions Lean4.
leanprover.github.io/documentation/

[Huỳnh Trần Khanh]

@antonio don't forget that the community site exists! https://leanprover-community.github.io

[Kevin Buzzard]

https://leanprover-community.github.io is the place for all your Lean 3 related stuff

[Kevin Buzzard]

The community runs Lean 3 right now; Microsoft are working on Lean 4. The community maintains a fork of Lean 3 and they also maintain mathlib.

[antonio]

Clear, thanks, strange that Microsoft does not give explicit directions on this

[Sebastian Ullrich]

The official site you linked to does link to the community page

[Arthur Paulino]

Installing on a new Linux via the "Install Lean using Elan" button triggers this error:
Captura-de-tela-de-2022-06-21-12-51-59.png
That is, it's not finding curl (it's a brand new Linux installation). The terminal disappears super fast and I had to be a bit ninja to get this screenshot. Maybe installing curl before is safer

[Henrik Böving]

Installing curl on a Linux machine would require root privs though and you'd have to guess the system package manager (well you can figure out the distro from /etc/os-release and then run the according manager but still) that doesn't seem like a good (and sometimes even impossible, consider e.g. uni PCs) idea to do unasked.

[Arthur Paulino]

Right now, the user can't even see that curl wasn't found

[Arthur Paulino]

(the terminal disappears very very fast. I was lucky to get the timing right for that screenshot and be able to see the error)

[Sebastian Ullrich]

Similar issue, but prior to clicking "Install Elan": https://github.com/leanprover/vscode-lean4/issues/181