Download mathlib4 once and link multiple projects against it

Stream: mathlib4

[Daniel Donnelly]

I am needing to know how this works with respect to git. Do I have users fork mathlib4 (creating like a workspace) and then add in their independent mathlib4 projects as git submodules? Not sure what Lean4 / mathlib4 expects or has to have. Thanks! :sunglasses::cactus::lady_beetle:

Edit:

What I'm building is a managed IDE for Lean4. So even though the user can manually still construct the Lean4 project structure using individual commands if they desire, we offer automatic quickstart project wizards. So I need comprehensive solutions to this problem (most likely all three options shown below).

The user might want to see the source code in which case they can use Option 2. If they don't need to, they can just use Option 1. If they have several related projects they put it all under a single github repo and under a single Workspace folder, then create subfolders for the individual sub-projects.

I'm just wanting to verify that this is all correct, since it would be nice to have real expert advice on this.

Edit 2:

The problem is I don't fully understand all ways of Sharing mathlib4 amongst many of the users' mathlib4-based Lean4 projects. I'm hoping to support the standard practices in my IDE. I certainly can't have them download all 700MB of mathlib cache each time they create a project; it takes way too long at least for my internet connection.

[Daniel Donnelly]

There are a few approaches for sharing mathlib4 across projects:

Option 1: Mathlib Cache (Recommended)
Mathlib provides pre-built .olean files. The cache is stored globally, so multiple projects share it:
# In each project, after adding mathlib dependency:
lake exe cache get

The cache lives in ~/.elan/ and is shared automatically. You still declare mathlib as a dependency in each project, but
the compiled artifacts are reused.

Option 2: Local Mathlib Clone with lake override

Clone mathlib once and point projects to it:

# Clone mathlib once
git clone https://github.com/leanprover-community/mathlib4 ~/mathlib4
cd ~/mathlib4
lake exe cache get
lake build

Then in each project's lakefile.lean, use a local override:

# From your project directory:
lake override set mathlib ~/mathlib4

Or set it in lake-manifest.json / environment variable.

Option 3: Workspace/Monorepo

Structure your projects under one workspace with mathlib as a shared dependency:

my-workspace/
lakefile.lean # defines mathlib dependency once
projects/
project-a/
project-b/

The root lakefile.lean:
import Lake
open Lake DSL

package workspace

require mathlib from git
"https://github.com/leanprover-community/mathlib4"

lean_lib ProjectA { srcDir := "projects/project-a" }
lean_lib ProjectB { srcDir := "projects/project-b" }

---

Recommendation: Option 1 (cache) is usually sufficient since the 700MB is mostly compiled .olean files that get cached
globally. Option 2 (local override) gives you explicit control and guarantees all projects use the exact same version.
Option 3 works well if your projects are closely related.

-Claude Opus

That's what the AI told me. Is this all correct and what option is standard?

[Daniel Donnelly]

I'm guessing: use option 1 if they don't need to edit source files of mathlib4. Option 2 if they do need to potentially edit them and Option 3 if they have several closely related projects.

[Snir Broshi]

FWIW I think using an LLM then asking humans to interpret it for you is a very roundabout way of asking a question. Can you instead formulate your question fully? (I don't understand the question from your first message)

[Michael Rothgang]

There probably is a documented answer to your question - but please tell us your question so we can be sure it would actually answer it!

[Daniel Donnelly]

@Snir Broshi @Michael Rothgang done. See further description. Basically I need comprehensive support for various ways of creating Lean4 projects, all done programmatically by the IDE itself. I'm creating a standalone IDE for Lean4 (doesn't require vscode). LSP, infoview, and all. I think we're also gonna parse Lean4 for beautification, and code generation when it comes to the Quiver-based diagram chasing tool.

[Daniel Donnelly]

Digression:
nParsing so that we can roundtrip changes from Lean4 to Diagram and from Diagram to Lean4. But perhaps this can be done using Widgets. Only issue is I don't want to have to wrap all existing non-widgets based proofs in widget-ready objects. So parsing is probably necessary. Otherwise, we're left using regex's only, which is not very general / robust.

[Michael Rothgang]

I'm still not sure what your question is. You have explained additional context, but nor your question itself. (I hear the question "is this LLM output correct" --- but what is the question you want the LLM to answer?)

[Snir Broshi]

Your edited question still refers to the LLM output (e.g. "Option 2"), so I still don't understand the question.
The first paragraph of your edit mentions "this problem" but you haven't stated the problem yet.

[Daniel Donnelly]

Okay, I've added Edit 2

[Daniel Donnelly]

Yeah, my internet conn either goes to space first (Starlink) or I use a small amount of data on my T-mobile plan. So it's not very quick to download Mathlib4 / cache.

[Snir Broshi]

Well you have to download Mathlib's cache to use it, but if you only need one version of Mathlib ever then you only have to download once. Wouldn't each project use a different version?

[Daniel Donnelly]

@Snir Broshi I'd think each project would use the stable release and that would stay the same for a while, then they can either update Mathlib4 in place or start a new workspace with another clone (and wait time) of mathlib4.

[Snir Broshi]

Updating Mathlib in-place requires downloading the cache again. The in-place part only lets you delete the old cache, but won't save time.

[Daniel Donnelly]

@Snir Broshi So I should support both options ig.

[Daniel Donnelly]

@Snir Broshi that's good to know, I will bookmark this conversation for later.

[Snir Broshi]

I'm confused. To summarize: You have to download the cache once per Mathlib version.
To share that downloaded version between all projects that use that same version, use symbolic links.

[Daniel Donnelly]

@Snir Broshi is that a Windows-specific filesystem symbolic link or something to do with Lean?

[Snir Broshi]

#lean4 > Does getting lean4 / mathlib usually take this long? @ 💬

[Daniel Donnelly]

I think I have enough to go on for now. Thanks @Snir Broshi @Michael Rothgang for the guidance.

[Michael Rothgang]

Have you seen https://leanprover-community.github.io/mathlib-manual/html-multi/Guides/Shared-Mathlib-Installation/#Mathlib-Manual--Guides--Shared-Mathlib-Installation already? That's a much better explanation for Option 2.

[Daniel Donnelly]

Thanks @Michael Rothgang very helpful! :nerd: Bookmarked :place_holder: and I will read it thorougly for understanding.

[Daniel Britten]

@Daniel Donnelly I haven't tried this myself yet, but https://github.com/lenianiva/lean4-nix might possibly help. If lean4-nix works as I think it would then it should only download each version of mathlib once (into /nix/store/... if you use Nix to build your projects using lean4-nix. See https://nixos.org/ if you're not familiar with Nix.
If you do give this a try, I'd be interested to hear how it goes :slight_smile:

[Shreyas Srinivas]

Michael Rothgang said:

Have you seen https://leanprover-community.github.io/mathlib-manual/html-multi/Guides/Shared-Mathlib-Installation/#Mathlib-Manual--Guides--Shared-Mathlib-Installation already? That's a much better explanation for Option 2.

I get a 404 error on this link

[Yury G. Kudryashov]

Web archive has a copy: https://web.archive.org/web/20250818063750/https://leanprover-community.github.io/mathlib-manual/html-multi/Guides/Shared-Mathlib-Installation/

[Shreyas Srinivas]

Thanks. Will lake support this by default some day?

[Shreyas Srinivas]

I currently have about 250-300 GB of mathlib4 projects at this point and bought an SSD last year just for them

[Jon Eugster]

Shreyas Srinivas said:

Michael Rothgang said:

Have you seen https://leanprover-community.github.io/mathlib-manual/html-multi/Guides/Shared-Mathlib-Installation/#Mathlib-Manual--Guides--Shared-Mathlib-Installation already? That's a much better explanation for Option 2.

I get a 404 error on this link

https://github.com/leanprover-community/mathlib4/wiki/Project-setup:-globally-shared-mathlib-installation

I moved it to the mathlib wiki last week.

(I've only put a redirect on the landing page, not for every subpage)

[Kim Morrison]

Shreyas Srinivas said:

Thanks. Will lake support this by default some day?

Yes, Mac is actively working on improving this situation.