Zulip Chat Archive

Stream: new members

Topic: understanding update-mathlib

Adam Topaz (Dec 11 2019 at 17:29):

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 (Dec 11 2019 at 18:53):

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 (Dec 11 2019 at 18:58):

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 (Dec 11 2019 at 21:26):

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

Adam Topaz (Dec 11 2019 at 21:32):

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 (Dec 11 2019 at 21:34):

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 (Dec 11 2019 at 21:34):

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

Adam Topaz (Dec 11 2019 at 21:36):

Ah! I see. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC