understanding update-mathlib

Stream: new members

[Adam Topaz]

Hi! I've been interested in lean for a while, and I finally have some time to play around with it.

I'm trying to get mathlib set up on my computer, but I have a fairly uncommon system (based on nixos), so I would like to understand precisely how leanpkg and update-mathlib interact (eventually it would be nice to write a nix derivation that sets everything up automatically using, e.g. nix-shell).

Suppose I follow the following (standard?) workflow:

1. Use leanpkg new foo && cd foo to start a new lean project in the folder foo and change to that directory.
2. Use leanpkg add leanprover-community/mathlib to add mathlib source to _target/deps/mathlib and update leanpkg.toml and leanpkg.path accordingly.
3. Use update-mathlib to do various things...

Assume I have used update-mathlib in the past so the directory $HOME/.mathlib already exists, and assume that the .mathlib folder does not contain a cached olean archive of the current version of mathlib. I would like to understand what step 3 above actually does.

I looked at the update-mathlib python script itself. If I understand correctly, step 3 should be (more-or-less) equivalent to the following:

• Download the olean tarball from github.com/leanprover-community/mathlib-nightly corresponding to the commit hash of the current version of mathlib (as defined in leanpkg.toml) and save it in ~/.mathlib for future use.
• Extract that tarball into foo/_target/deps/mathlib thereby adding .olean files in foo/_target/deps/mathlib without any actual compilation using lean.

It would be great if someone more familiar with the tooling could verify that this is indeed all that is happening. Is it true that the main reason to use update-mathlib in step 3 above is to avoid compiling mathlib entirely from source (which takes quite a while)?

[Kevin Buzzard]

Yes, the point of update-mathlib is precisely that if you download mathlib from e.g. github and then change directory into src and type lean --make, it will take 15 minutes or more to compile the .lean files into the .olean bytecode. We wanted users to be able to get going more quickly, so people wrote update-mathlib to download some precompiled binaries.

[Kevin Buzzard]

If you are happy to just make one project foo, download today's mathlib master, compile from source by running lean --make in _target/deps/mathlib/src and then go and have a cup of tea, then you won't need update-mathlib. If you want to make a second project with mathlib as a dependency then you could literally just copy _target over although (a) you would have to be careful with timestamps (i.e. preserve them!) and (b) you would in theory have to edit leanpkg.toml yourself to point to the correct commit (this is what leanpkg add does, as well as cloning the mathlib repo).

If on the other hand you want to update mathlib to get some new exciting feature, then you'll have to compile again.

[Patrick Massot]

Yes, you can emulate what update-mathlib is doing by downloading a mathlib nightly and extracting it in the relevant folder.

[Adam Topaz]

Great! Thanks for the responses. One more quick question regarding Kevin's response: Where do timestamps come in the picture and what will break if they're not preserved? (Are these just filesystem timestamps you're referring to? I don't see timestamps inside of any file generated by leanpkg.)

[Patrick Massot]

If Lean sees foo.lean file which is newer than foo.olean it will recompile foo.lean and every files depending on it.

[Patrick Massot]

Some OS manage to mess up time stamps when extracting archives...

[Adam Topaz]

Ah! I see. Thanks!