Updating Dependencies in a Lean (+ Mathlib) Project

Whenever a new Lean version comes out — or whenever I want to use something only recently added to mathlib — then I need to update the dependencies of my project.

This is something I have to do every few weeks and each time it was basically trial and error. But today also someone else asked me how this is done, so this time I documented it.

Concretely, I wrote this note here while upgrading my project lean4-pdl from Lean 4.13 to 4.14, released on 2 December 2024.

Disclaimer: I am not an expert on any of this stuff, and this is probably not the best advice you can find. Please contact me if something mentioned here is wrong or not recommended, I’ll be happy to update the post!

Background

Where are dependencies defined?

Dependencies of a Lean project are managed by three files:

lean-toolchain is very short and specifies which version of Lean itself we want. In my case, before the update it consisted of:
```
leanprover/lean4:v4.13.0
```
lakefile.lean

This file is listing the dependencies. In my case, the only dependency is mathlib. Without comments it looks like this:
```
import Lake
open Lake DSL

package «pdl»

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

@[default_target]
lean_lib «Pdl»

lean_lib «Bml»
```
I think the newer way of doing things is to use a lakefile.toml file instead of a lakefile.lean. I’ll make that switch some other day.
lake-manifest.json is automatically generated from the other two files. Do not edit it manually. The manifest actually pins down fully specified versions by referring to a git commit of mathlib. This ensures reproducibility: someone downloading the project later can compile it without guessing versions of dependencies. You can also notice that the manifest contains a lot more dependencies besides mathlib — in my case 9 repositories! This is because mathlib itself depends on those things: plausible, LeanSearchClient, import-graph, ProofWidgets4, aesop, quote4, batteries and lean4-cli.

All three files should be tracked by git.

Can’t I do this without terminal voodoo?

Officially, yes, I guess? In VS codium, we can click on the ∀ logo and then under “Project actions…” click on “Update dependency”. But for me this does not (always) seem to work. In particular it sometimes took very long because it started compiling Mathlib instead of downloading cache files. It also did not seem to update the manifest file, even though I guess it should do that.

The second naive way: `lake update`

It seems one should be able to run lake update and be done, but in practice this has hurt me a few times. In particular as far as I understand, lake update updates everything (Lean, mathlib, other dependencies) to the latest versions. I like to have a bit more control and stick to the stable version of Lean instead of jumping to release candidates. Hence, see the next section.

Safety measures

Above you can see that my lakefile.lean does not just say “I want mathlib” but says “I want a mathlib that works with Lean version v4.13.0”. This is possible because in the mathlib4 repository there is tag for it. See https://github.com/leanprover-community/mathlib4/tags for all available tags.

The actual update

Now here is the actual update procedure.

Close VS codium and make sure git status is clean.
Change the content of the file lean-toolchain to refer to the new version:
```
leanprover/lean4:v4.14.0
```
In the file lakefile.lean, change v4.13.0 to v4.14.0.
Delete the old manifest and all built files:

rm -rf lake-manifest.json .lake

Deleting .lake here is a bit radical and does mean that the next step will take even longer But for some previous updates this was the easiest way to fix things.
Run lake update -R.

This will take a long time and output many things, including this crucial line:
```
info: pdl: no previous manifest, creating one from scratch
```
And indeed, at that moment a new lake-manifest.json is generated.
Now check that the project still compiles and run lake build.

For example, I got error: no such file or directory because I had import Running Mathlib.Order.BoundedOrder in a file. A search in mathlib shows that apparently this file no longer exists, so I changed the import to Mathlib.Order.BoundedOrder.Basic.

Also plenty of warnings came up, but they are usually easy to fix:
- The `unfold_let` tactic is deprecated. Please use `unfold` instead.
- `List.mem_join` has been deprecated, use `List.mem_flatten` instead
Once everything compiles, make a commit!

I usually do that as soon as there are no more errors, but before fixing all the warnings.

To sum it up, for my project you can see all the changes needed for the update in the diff for the commit c7a2dd0a272a71660dbd7f7bbe858edc31668ee5.

Simple Method without Pinning

If you do not care which Lean version to use, but just want the latest, then the instructions on this page under the heading “Updating Mathlib in your project” provide a two step method:

Overwrite the lean-toolchain in your project with the one from mathlib.
Run lake update.

After this, check if all your files compile, for example with lake build. The page also suggests to run lake exe mk_all for which I could not find documentation but which seems to regenerate the top-level files (in my case Pdl.lean and Bml.lean).