Automatic nightly Lean update?

Question

I recently answered my own question for how to set up a Lean project with Mathlib dependencies. I realize I don't know everything about this. The route I follow starts by navigating to the correct folder in a terminal and running

lake +leanprover/lean4:nightly-2023-02-04 new my_project math

I then navigate to my_project, run lake update, lake exe cache get, and then mkdir MyProject.

All this is according to the documentation. Will this project automatically update with Lean nightly changes? If not, how do I do this safely?

Answer 1

No, this project will not update the Lean toolchain automatically.

The only way to change the Lean toolchain that a project uses is to edit the lean-toolchain file for that project.

If you would like to change to the current nightly, then you can change the contents of lean-toolchain to, e.g.

leanprover/lean4:nightly-2023-09-23

However! Your upstream dependencies, in particular Mathlib, may not work on this toolchain. At present Mathlib uses the release candidates and stable releases, but does not update to each nightly toolchain.

There is a nightly-testing branch of Mathlib, which does track the nightly releases (sometimes with breakages).

Thus you could use

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

in your lakefile.lean, and then whenever you run lake update (which will move your Mathlib dependency to the latest commit on the nightly-testing branch), also remember to

cp lake-packages/mathlib/lean-toolchain .

(To bring your lean-toolchain up to what nightly-testing is using.)