How to lake update? Best practices?

Stream: new members

[Malvin Gattinger]

Each time a new lean version comes out or when I want something that was only added to mathlib recently, I need to update the dependencies of my project. I figured this out more or less by trial and error and basically do this:

1. Change lean-toolchain manually.
2. In lakefile.lean update my pinning of mathlib.
3. rm -rf lake-manifest.json .lake :see_no_evil:
4. lake update -R (which regenerates the manifest and downloads the mathlib cache)
5. lake build (to actually check if my stuff builds with the new versions)

Is this a reasonable way to do it? Or unnecessarily manual? Or dangerous?

For my future self and someone who asked about this me today, I just now wrote down more details in a blog post here and I'd be happy to hear more what is the "official right way" to do this. Here on zulip there are multiple threads of the form "I ran lake update and it broke ..." so some general advice on it might be good. Is there something in the Lean manual or elsewhere?

[Ruben Van de Velde]

You should be able to drop step 3, otherwise this is reasonable enough

[Ruben Van de Velde]

Though I'm not sure why you're pinning mathlib in your lakefile.lean

[Paul Schwahn]

On the leanprover community website, the updating process is described as follows:

1. Update lean-toolchainby running curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain in the directory of your repository.
2. Run lake update.
3. (optional) Build files with lake exe mk_all && lake build.
   For me this has worked so far, and I've always understood it to be the "official way". However I don't understand enough of the process to judge how this differs from @Malvin Gattinger's approach. Can anyone explain this?

[Ruben Van de Velde]

There's two main ways you might depend on mathlib in your lakefile: either depend on master or on a specific v4.X.0 tag. I guess Malvin is using the latter and you are using the former

[Ruben Van de Velde]

In the tag case, you also need to update the lakefile before you can update mathlib

[Sebastian Ullrich]

• Update lean-toolchainby running curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain in the directory of your repository.

This step should be obsolete starting with Lean 4.15.0, lean#5684. Obviously we shouldn't delete that text yet but maybe make it conditional?

[Sebastian Ullrich]

Ruben Van de Velde said:

There's two main ways you might depend on mathlib in your lakefile: either depend on master or on a specific v4.X.0 tag. I guess Malvin is using the latter and you are using the former

This discrepancy can be avoided by pinning the stable branch instead of a fixed tag in the lakefile. Perhaps this should even be advertised as the default way of depending on Mathlib for anyone not interested in the bleeding edge?

[Sebastian Ullrich]

IOW: Use master or stable, then lake update should be the only command necessary going forward.

[Ruben Van de Velde]

Huh, I didn't know mathlib had a stable branch

[Philippe Duchon]

Concretely, what should the configuration files in a Lean project (say, using Mathlib) look like, and which files are these? I have no real project underway, and what little I created was copy/paste from tutorial webpages, but lake update fails with a invalid toolchain name: 400: Invalid request error.

At the moment it's no big deal because I can easily create a new project from scratch and copy the one or two Lean files over, but I'd like to do things semi-right in the future (and, hopefully, will end up having more content to copy over).

[Malvin Gattinger]

I assume for making new projects the recommendation is to run lake init myProject math. That creates a lean-toolchain and lakefile.toml (even though lake init --help says "the default is Lean" :ladybug: ?). Notable the lakefile does not specify a tag or version of mathlib, but the first lake build then creates a manifest.

[Yicheng Tao]

To me, use lake new ProjectName math.lean works just fine. But the initial toolchain will be the latest Mathlib and the lakefile doesn't specify a tag. I will choose to modify the lean-toolchain to a stable version like v4.14.0 and specify the tag in lakefile.

In lakefile.lean:

require "leanprover-community" / "mathlib" @ "git#v4.14.0"

In lakefile.toml:

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.14.0"

Then run lake update and generate a manifest. These steps will ensure running lake update won't change the current manifest. Everything is stable now.

[Ruben Van de Velde]

Why?

[Yicheng Tao]

Oh, I was talking about non-mathlib development. I prefer working in a 100% stable environment. If keep up with the latest mathlib is necessary, then of course you need to change the tag to master and then lake update.

[Yicheng Tao]

In my own project, I will only update when mathlib release a new tag.

[Ruben Van de Velde]

No, my point is - it's very easy to have a fully stable environment: never run lake update. I don't see why you'd want a setup where you do run lake update but don't want it to do anything

[Yicheng Tao]

Partly because I often work with people who are new to Lean and know little about how these things work. I need to make sure they won't mess up the environment by running command they don't really know.