2.2. Follow Stable Dependencies

(written by Jon Eugster)

This tip should be considered a workaround, some care is adviced when trying this non-standard setup!

Note: Things here might change as lake is being developed, as features described here are not necessarily officially supported by lake. This file has been written for Lean v4.16.0. If in doubt, ask for help on Zulip.

If your Lean project only wants to following the stable releases of dependencies (i.e. v4.16.0, v4.17.0, etc.) you could do the following trick:

In your lakefile.lean, add

and then suffix all requires with @ leanVersion:

require "leanprover-community" / "mathlib" @ leanVersion

Note: for this to work, the repository of each dependency needs to have a tag (or branch) for the Lean version you're using, e.g. look at the mathlib tags.

If you specified the version for all dependencies in your project, you can then update your project simply by

• Edit lean-toolchain to have the new toolchain leanprover/lean4:v4.17.0.

• Call lake update -R.

Note: a blank lake update -R is only reasonable if all required dependencies in your project have a version specified with @.