How to Efficiently Use Mathlib in Multiple Projects?

Stream: mathlib4

[Pietro Monticone]

Hi, I have multiple locally cloned GitHub repositories hosting distinct Lean projects having Mathlib as a dependency.

How can I efficiently use the same compiled version of Mathlib for all projects without re-building it and decompressing it in the .lake folder occupying about 5GB for each one?

[Luigi Massacci]

Maybe you can tag @Mac Malone (if I'm not mistaken), since this is arguably a lake feature

[Kim Morrison]

Unfortunately this is barely supported. You can use relative paths when specifying dependencies (but this is not really a shareable solution if your project is in a repo others use), but people seem to have regular problems when doing so.

[Eric Wieser]

Note that relative paths will only work if your projects are on exactly the same version of mathlib

[Eric Wieser]

On the subject of relative paths, #8767 was an attempt to add better support for them with lake exe cache pack and lake exe cache unpack, but it ran into some issues I haven't tried to diagnose

[Tony Starter]

Is there any progress on this topic?

[Kim Morrison]

@Tony Starter, if you're working on a non-shared project, you can use relative paths in your lakefile to point to a fixed copy of Mathlib somewhere on your drive.

If you're working on a shared project, I don't think anyone has even proposed a mechanism by which this might work. What happens when the project needs to update a dependency? How does your local setup know it needs to "detach" from the shared copy of Mathlib to move to a different version? This is why we have separate copies in the first place.

[Eric Wieser]

(are both non-s intentional Kim? It sounded like you were intending to make a comparison)

[Kim Morrison]

Eric Wieser said:

(are both non-s intentional Kim? It sounded like you were intending to make a comparison)

editted, thanks

[Eric Wieser]

If you're working on a shared collection of projects, you can create a "workspace" repo that checks all the projects out as git submodules into a single folder structure, and have each project refer to the others via relative paths.

[Eric Wieser]

I think @Mac Malone has custom repositories in-the-works/implemented-but-not-announced, which would avoid you having to even modify the lakefiles?

[Kyle Miller]

I could imagine something elan-like to cache oleans for specific versions of mathlib, and maybe using git worktree per project to save duplicating the 300MB of git history

[Sebastian Ullrich]

A low-level post-hoc solution, but it should be possible to hardlink these duplicate .olean files with tools such as https://github.com/pauldreik/rdfind

[Michael Rothgang]

@Jon Eugster wrote some docs on how to re-use the same mathlib version: https://github.com/leanprover-community/leanprover-community.github.io/pull/510

[Michael Rothgang]

(Proof-reading and approving that PR is welcome, I presume.)