Zulip Chat Archive

Stream: lean4

Topic: Does getting lean4 / mathlib usually take this long?

Daniel Donnelly (Jan 11 2026 at 06:25):

Taking an hour to complete:

image.png

Also, is it against Lean4's license to include it in my own application's downloadable package because this download wait time is not very good UX?

I'm making a standalone IDE for Lean4. But it's going to have commutative diagram support via Quiver. These diagrams will just get translated into definitions in the focused Lean4 file.

Daniel Donnelly (Jan 11 2026 at 06:44):

Solution: I cloned a Lean4 project w/o mathlib dependency.

Thomas Murrills (Jan 11 2026 at 06:45):

No, it never takes me that long! Usually comfortably under a minute.

Daniel Donnelly (Jan 11 2026 at 06:46):

@Thomas Murrills I must be doing something wrong then :)

Daniel Donnelly (Jan 11 2026 at 06:47):

@Thomas Murrills So it takes you under a minute to download mathlib4?

Thomas Murrills (Jan 11 2026 at 06:50):

Daniel Donnelly said:

Thomas Murrills I must be doing something wrong then :)

Not necessarily—it's entirely possible the software is doing something wrong. :grinning_face_with_smiling_eyes: If I recall correctly people have reported weird situations where this can take very long...you might find them on zulip somewhere, but unfortunately I'm not sure where.

Others might have more insight into what could be happening, but I just wanted to let you know that this is certainly not typical! :)

Thomas Murrills (Jan 11 2026 at 06:50):

Daniel Donnelly said:

Thomas Murrills So it takes you under a minute to download mathlib4?

That's right!

Daniel Donnelly (Jan 11 2026 at 07:15):

@Thomas Murrills what do you think about this idea? It is supposed to be simpler than using VScode (original / current Lean4 ext). Though doesnt hamper you from using one or the either because we use QFileSystemWatcher to monitor a project. It's going to have easy access to many lean4-extension projects. Syntax highlighting as well as LaTeX previewing / posting on a site (whatever can be done now with that certain library, then we'll enhance it).

Eric Wieser (Jan 11 2026 at 09:27):

This can sometimes be caused by an overeager antivirus

Eric Wieser (Jan 11 2026 at 09:27):

(which intercepts every individual download and substantially slows it down)

Daniel Donnelly (Jan 11 2026 at 10:13):

@Eric Wieser it's not that for me. I don't have AV / firewall on my workstation

Daniel Donnelly (Jan 11 2026 at 10:13):

enabled

Daniel Donnelly (Jan 11 2026 at 10:15):

lake new MyProject math
cd MyProject
lake exe cache get

Using this to create a new project with mathlib. Not sure why it takes infinity time... I tried this at raw command line on Windows 10 as well.

Daniel Donnelly (Jan 11 2026 at 10:16):

Yes, even in Vscode, so if I were even doing this with usual dev environment. It's not working right....

Daniel Donnelly (Jan 11 2026 at 10:19):

Even with Edge browser downloading the .zip of the github repository is taking ages.

Daniel Donnelly (Jan 11 2026 at 10:22):

Well, I kind of see why : I'm extracting the zip now and it's taking another millenium

Daniel Donnelly (Jan 11 2026 at 10:24):

image.png

Daniel Donnelly (Jan 11 2026 at 11:03):

Okay it can be my internet provider / conn. So I got more data. Anyway testing that hypothesis out rn

Eric Wieser (Jan 11 2026 at 11:45):

Perhaps you have a very slow hard drive?

Eric Wieser (Jan 11 2026 at 11:45):

Daniel Donnelly said:

Eric Wieser it's not that for me. I don't have AV / firewall on my workstation

Not even the builtin windows defender?

Kevin Buzzard (Jan 11 2026 at 13:02):

FWIW here's a gif showing what happens on my linux machine if I type in the commands you mentioned above:

lake new MyProject math
cd MyProject
lake exe cache get

although I'm pretty sure that the third one is unnecessary as it looks to me like all this was done once during the first command. I think I was all ready to go after about 2 minutes.

Peek 2026-01-11 13-01.gif

Daniel Donnelly (Jan 12 2026 at 03:23):

@Eric Wieser yes, that's all disabled. @Kevin Buzzard thanks for the GIF, that gives me a good idea of the timing. I'll try it again from the command line to compare.

Daniel Donnelly (Jan 12 2026 at 03:31):

@Kevin Buzzard it's totally unlike your screenshot. Stays here for a long time:

C:\Lean4Projects\blah>lake new MyProject math
info: MyProject: no previous manifest, creating one from scratch
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4

At least 5 minutes for me. Could it be because I'm on Starlink satellite internet?

Malvin Gattinger (Jan 12 2026 at 08:47):

Daniel Donnelly said:

Well, I kind of see why : I'm extracting the zip now and it's taking another millenium

This looks like the file system or something related is slowing things down. Do you have an external SSD or some other fast usb stick? Then you could try to download the zip to that and extract there to see if whatever is C: is the culprit.

Shubakur Mitra (Jan 12 2026 at 11:57):

1 hour and 20 minutes

time lake new MyProject math

Kevin Buzzard (Jan 12 2026 at 15:16):

That looks like it didn't actually work, so maybe something took a long time to time out?. On a mac on wireless at work (in the UK) I get 2.5 minutes:

time lake new MyProject math

Julian Berman (Jan 12 2026 at 15:19):

@Daniel Donnelly does git clone https://github.com/leanprover-community/mathlib4 work? How long does it take?

Julian Berman (Jan 12 2026 at 15:23):

@Shubakur Mitra your output shows 479.0 MiB / 479.0 MiB (100 %) 272.0 KiB/s -- at 200Kib/s that means like 30 minutes or more is spent just downloading. If you go to https://fast.com/ how fast does it say your connection is acting?

Note also that that 500MB download is a Lean toolchain you didn't have, so if you run it a second time, it will skip the first part but still run the second part -- which still involves downloading stuff of similar size, so there a bunch more time is taken just downloading things over your connection.

Shubakur Mitra (Jan 12 2026 at 15:50):

My comment is not a complaint but a reference point, answering the original question about download times for Lean, Mathlib, and fetching the cache on different machines. Of course, a slow connection is the main culprit here. The "failed to fetch cache" error is somewhat misleading; it fetched all but one file (at only 1 KB/s!), and the remaining file can be compiled locally.

Shubakur Mitra (Jan 12 2026 at 15:53):

Julian Berman said:

that means like 30 minutes or more is spent just downloading.

1 hour and 19 minutes is spent downloading.

Daniel Donnelly (Jan 13 2026 at 09:23):

Downloaded: 7717 file(s) [attempted 7717/7816 = 98%, 651 KB/7816 = 100%, 73 KB/s]Downloaded: 7720 file(s) [attempted 7720/7816 = 98%, 195 KBDownloaded: 7725 file(s) [attempted 7725/7816 = 98%, 434 KBDownloaded: 7768 file(s) [attempted 7768/7816 = 99%, 69 KB/Downloaded: 7785 file(s) [attempted 7785/7816 = 99%, 123 KBDownloaded: 7809 file(s) [attempted 7809/7816 = 99%, 55 KB/Downloaded: 7812 file(s) [attempted 7812/7816 = 99%, 153 KBDownloaded: 7814 file(s) [attempted 7814/7816 = 99%, 73 KB/Downloaded: 7816 file(s) [attempted 7816/7816 = 100%, 73 KB/s]
Decompressing 7816 file(s)
C:\Users\fruit\.cache\mathlib\c760715337f7bfc0.ltar: removing corrupted file
C:\Users\fruit\.cache\mathlib\69d5a457a2708031.ltar: removing corrupted file
C:\Users\fruit\.cache\mathlib\67b72aceb1067fb5.ltar: removing corrupted file
C:\Users\fruit\.cache\mathlib\cd64103bcfa2d2b6.ltar: removing corrupted file
C:\Users\fruit\.cache\mathlib\5f03f77954

I started the command:

"lake exe cache get"

About 20 minutes ago, and it's still running. When I saw a lot of console traffic, I felt like an internet god with my T-mobile data plan on my phone. Now it seems to be stuck at a removing corrupted file line -_-. Can we possibly get Mathlib in small chunks?

Daniel Donnelly (Jan 13 2026 at 09:27):

Well, I see an issue I have 0MB of space left on my hard drive. Time to delete some apps.

Daniel Donnelly (Jan 13 2026 at 09:31):

I don't know how many times I've downloaded mathlib4 ;d My recycle bin is 21GB though....

Daniel Donnelly (Jan 13 2026 at 11:14):

Julian Berman said:

Daniel Donnelly does git clone https://github.com/leanprover-community/mathlib4 work? How long does it take?

@Julian Berman Running this now.

It took 6minutes :) But I'm not sure how this relates to lake command.... is there a guide somewhere on what each command does?

Well, I found this on readme front page of mathlib4:

The complete documentation for contributing to mathlib is located on the community guide contribute to mathlib

You may want to subscribe to the mathlib4 channel on Zulip to introduce yourself and your plan to the community. Often you can find community members willing to help you get started and advise you on the fit and feasibility of your project.

  • To obtain precompiled olean files, run lake exe cache get. (Skipping this step means the next step will be very slow.)

  • To build mathlib4 run lake build.

Hopefully this method will work for me now that I have free space, internet bandwidth, and know a little bit more of what to do.

Kevin Buzzard (Jan 14 2026 at 08:08):

If it takes 6 minutes to clone mathlib using git then your problem is not with lean, your problem is elsewhere.

Bbbbbbbbba (Jan 14 2026 at 09:32):

Kevin Buzzard said:

If it takes 6 minutes to clone mathlib using git then your problem is not with lean, your problem is elsewhere.

Is there an easy way to avoid cloning mathlib repeatedly?

Anne Baanen (Jan 14 2026 at 11:22):

That question is going to be hard to answer without knowing what you are trying to do. Unless you need to create new Lean projects as a fundamental part of your workflow (for example, you're testing the lake new command), you should almost never have to clone Mathlib repeatedly.

Bbbbbbbbba (Jan 14 2026 at 11:24):

Well I just want to organize my work in different projects, and also so that I only need to fix one project at a time when I want to bump up the version.

Anne Baanen (Jan 14 2026 at 11:32):

If you want different versions of Mathlib for different projects to depend on, I don't know any practical way to achieve this without having different clones of Mathlib inside those projects.

Snir Broshi (Jan 14 2026 at 12:28):

You can use Git worktrees to have only one .git folder, which would save you about 700MB per copy

Snir Broshi (Jan 14 2026 at 12:29):

That's what I use to work on multiple Mathlib things in parallel

$ git worktree list
mathlib4          ae275c9caf8 [master]
mathlib4-copy     b1e306623a0 [pr/30658]
mathlib4-copy2    ae275c9caf8 [feature/linter/factorial-notation]
mathlib4-nightly  ce00192bf80 [nightly-testing-green]

Daniel Donnelly (Jan 15 2026 at 01:17):

@Snir Broshi thanks! That is really useful and we will need exactly that.

Daniel Donnelly (Feb 02 2026 at 18:27):

@Snir Broshi So for my use case I'm assuming I have to do this:

Have the user first fork Mathlib so that they can create worktree branches inside of it. But that's not really proper use of git if it's for an project independent of Mathlib.

What about this: 1) Fork mathlib creating a "worktree space containing mathlib" then: 2) Adding in a project (separate github repository) as a git submodule?

Would this work? I am indeed looking for a way to download mathlib once (or whenever needing update) and re-using / linking lean4 projects to that one copy.

Snir Broshi (Feb 02 2026 at 18:40):

I don't understand your use case, but I think you're using the word "worktree" incorrect here- forks have nothing to do with worktrees, worktrees are a local concept.
To use worktrees, git clone mathlib, then if you need multiple versions you can git worktree add ....
If you need these in some Lean copy, you can create the worktrees right where you need them, or use symbolic links to place them inside Lean (mklink /s on Windows, ln -s otherwise)

Daniel Donnelly (Feb 02 2026 at 19:13):

Decided to not support worktrees unless they create them manually. At least in version 0. I think the solutions in the other thread are more appropriate for now.

Last updated: Feb 28 2026 at 14:05 UTC