Mathlib4 globally

Stream: general

[Vinicius de Lima]

How can i install mathlib4 globally, so that any lean file can source it? I've read some topics about it, but remained unclear on how to do it in more recent versions.

[Mario Carneiro]

It's (still) not an officially supported configuration, but you can use symlinks to make it work

[Kevin Buzzard]

This question doesn't quite make sense to me. What do you mean by "any Lean file"? A lean file cannot really work unless it's in a Lean project (together with configuration files which say which version of Lean to use with the file) and the if the project has mathlib as a dependency then the config files will say exactly which commit of mathlib (and mathlib has many commits per day) should be being used in the project. So the file has to be in a project and the project has to know which version of mathlib to use. You could override this by manually ensuring that each project always uses the same version of mathlib (which will force you to use the same version of lean which will stop you from updating the project as lean evolves) and then doing some trickery with symlinks in .lake/packages/mathlib I guess?

[Mario Carneiro]

(I autocorrected the request to Kevin Buzzard 's last sentence. Agreed that you still need to have a project to put your files in, but symlinks let you have multiple projects that share a mathlib and that you can only upgrade in lock step)

[Vinicius de Lima]

When i made this question i was thinking about the C++ standard library, that you can import from wherever you want, or if you have the absolute path to the file you could still import it.

But, thanks for clarifying. So, just to summarize, for importing the same installation of mathlib in every project, i should creake a lakefile.toml requiring mathlib and symlink my original installation .lake/packages/mathlib?

Appreciate the help! :D

[Mario Carneiro]

There is no such thing as a global installation of mathlib. But you can make multiple projects, notice that the contents of .lake/packages/mathlib is suspiciously similar between them, and symlink one to the other or both to a location of your choosing.

[Mario Carneiro]

This will occasionally cause problems where lake in one project will stomp on the internal files expected by lake in the other project. It mostly works but there is no warranty

[Patrick Massot]

You can also use a local path to require mathlib instead of a git url.

[Mario Carneiro]

Is there an open issue for this? I feel like you might have opened one before @Patrick Massot

[Eric Wieser]

There's ongoing work on having a local "source registry" (offline reservoir), as I understand it

[Patrick Massot]

I don’t remember opening such an issue. The thing that was crucial for me was not to be able to use the same Mathlib for several project (since this seems very rarely useful). What is crucial for teaching is to be able to have Mathlib in a shared folder that students can’t write to.

[Patrick Massot]

And this works modulo the fact that you currently need to specify all transitive dependencies in your lakefile, which is a bit painful.

[Eric Wieser]

If you use a reservoir specifier instead of a git url, you can specify the path in addition

[Eric Wieser]

Patrick Massot said:

And this works modulo the fact that you currently need to specify all transitive dependencies in your lakefile, which is a bit painful.

If you control the local mathlib copy anyway, you can modify its lakefile instead, rather than putting everything in the student lakefile.

[Patrick Massot]

My requirements in the lakefile currently look like

[[require]]
name = "mathlib"
path = "/opt/lean/lib/mathlib"
rev = "v4.15.0-patch1"
[[require]]
name = "aesop"
path = "/opt/lean/lib/aesop"
[[require]]
name = "batteries"
path = "/opt/lean/lib/batteries"
[[require]]
name = "Cli"
path = "/opt/lean/lib/Cli"
[[require]]
name = "importGraph"
path = "/opt/lean/lib/importGraph/"
[[require]]
name = "LeanSearchClient"
path = "/opt/lean/lib/LeanSearchClient/"
[[require]]
name = "plausible"
path = "/opt/lean/lib/plausible"
[[require]]
name = "proofwidgets"
path = "/opt/lean/lib/proofwidgets/"
[[require]]
name = "Qq"
path = "/opt/lean/lib/Qq"
[[require]]
name = "verbose"
path = "/doc_enseignants/massot/verbose"

[Mario Carneiro]

I think it would be very useful to have a global install which is a soup of versioned files like what cache does

[Patrick Massot]

It’s true I could also modify the Mathlib lakefile.

[Patrick Massot]

But students never see the lakefile content anyway.

[Mario Carneiro]

I can see the possibility of having a global dump of stuff making storage issues worse though if it isn't aggressively GC'd

[Eric Wieser]

Patrick Massot said:

But students never see the lakefile content anyway.

I guess this depends on the students and the course. If you have a small number of students who might want to publish their class project at the end, then having a lakefile that's minimally different from upstream is probably a good thing. But if you're teaching basics then indeed it would be pointless.

[Patrick Massot]

There are no projects. It’s all about doing exercises that are ready made.

[Patrick Massot]

And it’s using Verbose Lean, which is not exactly “minimally different from upstream”.

[Patrick Massot]

I’m talking about https://github.com/PatrickMassot/proofs_with_lean/

[Eric Wieser]

For reference, the combined version I was referring to above I think would be something like

[[require]]
name = "mathlib"
scope = "leanprover-community"
version = "git#v4.15.0"
path = "/opt/lean/lib/mathlib"

though perhaps @Mac Malone can confirm

[Mac Malone]

@Eric Wieser Ah, that will just always use the path. Lake does not currently support mutiple sources.

[Eric Wieser]

But you can backspace the path at least to get the normal behavior, so it's only a one-line diff?

[Eric Wieser]

Is there a roadmap / tracking issue for the "source replacement" feature? I'd like to be able to check the status without having to ping you :)

[Mac Malone]

True. Also, using rev works just as well:

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.15.0"
path = "/opt/lean/lib/mathlib"

[Mac Malone]

Eric Wieser said:

Is there a roadmap / tracking issue for the "source replacement" feature? I'd like to be able to check the status without having to ping you :)

The basic system is already implemented as --packages (lean4#6411). Did you mean something more?

[Mac Malone]

When I have more time to dedicate to that area, I do hope to implement a user-wide version of the same thing (and eventually standardize the Reservoir index format as an even better replacment). Lake will be getting a user-local cache this quarter, so adding package-overrides.json as well to the user-wide Lake configuration should hopefully be easy to squeeze in.

[Eric Wieser]

I guess adding .lake/package-overrides.json to a course repo would be sufficient then, and no changes to lakefiles would be needed?

[Eric Wieser]

(I had indeed forgotten the PR you linked above, despite the fact that I commented on it)

[Shreyas Srinivas]

Mario Carneiro said:

I can see the possibility of having a global dump of stuff making storage issues worse though if it isn't aggressively GC'd

Like an opam switch?

[Mario Carneiro]

opam switches are very manual, I'm not a fan

[Mario Carneiro]

you have to actively manage your installation and this is a recipe for disaster with users who are learning the ropes

[Shreyas Srinivas]

Right. Another question : Couldn’t mathlib be installed with the toolchain somehow?

[Shreyas Srinivas]

And then just linked to projects by lake?

[Mac Malone]

Mario Carneiro said:

I think it would be very useful to have a global install which is a soup of versioned files like what cache does

You may be happy to learn that is what I am working on this quarter. :-)

[Shreyas Srinivas]

Mario Carneiro said:

opam switches are very manual, I'm not a fan

True, but opam can list all installed switches which can be deleted at will. Further if a project is still using a switch that was “deleted “, then opam re creates that switch as I recall

[Shreyas Srinivas]

Not too dissimilar to what elan does with toolchains (as far as installing and deleting them goes). Of course opam switches go further by also installing packages centrally with the switch

[Mario Carneiro]

yes, this is basically like elan toolchains. I think people will have to be actively cleaning them up much more often, esp. mathlib contributors since there is a new mathlib every day

[Shreyas Srinivas]

How does Nix do garbage collection?

[Shreyas Srinivas]

Couldn’t we tack that on?

[Mario Carneiro]

I think you could do something with reference counting

[Shreyas Srinivas]

Okay, but we could also have more aggressive deletion policies

[Shreyas Srinivas]

And when necessary lake would just get a deleted toolchain re installed (maybe marking it as “don’t remove” until it wants to use that toolchain and removing the marking if the project’s toolchain is updated)

[Shreyas Srinivas]

Mark and sweep garbage collection

[Shreyas Srinivas]

Slightly better, when a project is created or built with lake, some metadata is added to or deleted from the toolchain folder about the directory of the project that is using that toolchain. The GC just checks this list of folders and if none of them exist anymore, then it deletes the toolchain.

[Mario Carneiro]

I think that's also just reference counting

[Jz Pan]

Do you mean this link? https://leanprover-community.github.io/mathlib-manual/html-multi/Guides/Shared-Mathlib-Installation/#Mathlib-Manual--Guides--Shared-Mathlib-Installation

[Shreyas Srinivas]

Jz Pan said:

Do you mean this link? https://leanprover-community.github.io/mathlib-manual/html-multi/Guides/Shared-Mathlib-Installation/#Mathlib-Manual--Guides--Shared-Mathlib-Installation

This is a workaround. I'd like it to be the default way lake + elan manage mathilib dependencies (currently only lake is involved).