Mathlib installation on Linux

Stream: maths

[Julien Puydt]

I find the page here (and the variant for Debian derivative) as bit deceptive: it's mostly about installing elan, mathlibtools and vscode+lean extension. It doesn't really install what it's about!

I installed lean in my homedir with "elan default stable"... mostly unusable: no mathlib.

I then created a directory and started a leanproject in there, and it did download mathlib. In the directory, not my homedir, so if I try to make various experiments, that means massive duplication (700M!). As a comparison, I have coq installed from packaging and I have dozen of separate 4k-files.

Is there a way to install mathlib along the lean toolchain so it's of more general use? Did I miss a better documentation?

[Riccardo Brasca]

There is no real "mathlib installation", what we usually do is leanproject new your_project. Then, leanproject creates a folder your_project with mathlib inside.

[Anatole Dedecker]

Mathlib gets a new version several times a day, so having a global mathlib is essentially useless because most projects depend on a slightly different version. Personally I have a "draft" project in which I make all of my testing, which use a common mathlib. But apart from that, each project having its own mathlib directory is essentially the only possible way right now

[Riccardo Brasca]

The reason is that mathlib change super quickly, so the usual way of installing a software is not really adapted to it.

[Patrick Massot]

If you follow two links from that webpage you'll find https://leanprover-community.github.io/leanproject.html#global-mathlib-install explaining how to get a global mathlib install, but it is indeed a very bad idea (and this explain why the corresponding documentation is somewhat hidden).

[Miguel Marco]

I found that, for the kind of usage that does not need to care about mathlib updates, the tryleanapproach works very well.