Error updating mathlib

Stream: new members

[Benjamin]

I am trying to update my mathlib dependency to 4.15.0 for a project I am working on. To do this, I clicked "Project: Update Dependency" in VS Code. I get the following error: "Cannot update dependency. Command output: error: external command 'git' exited with code 1". How can I fix this?

[Ruben Van de Velde]

Can you figure out what git was doing?

[Benjamin]

I don't see what git was doing, but I see that VS Code tried to run the command lake update mathlib.

[Benjamin]

What's also weird is that it runs lean --version and the output is Lean (version 4.15.0-rc1, x86_64-w64-windows-gnu, commit ffac974dba79, Release). But that is not the version I should have installed. When I run the same command in my own terminal, I get Lean (version 4.15.0, x86_64-w64-windows-gnu, commit 11651562caae, Release), which is what I expect.

[Ruben Van de Velde]

The version of lean used depends on the lean-toolchain file in your project

[Ruben Van de Velde]

Each project can use a different version of lean, if it wants to

[Benjamin]

OK, so should I change leanprover/lean4:v4.15.0-rc1 to leanprover/lean4:v4.15.0?

[Benjamin]

And is there anything else I need to change if I want to have the latest version of other dependencies, like batteries? Or will these be updated automatically?

[Ruben Van de Velde]

Do you depend on mathlib?

[Benjamin]

I do.

[Ruben Van de Velde]

Okay, then you need to make sure you depend on the "v4.15.0" revision of mathlib, and then lake update should update your lean-toolchain by itself

[Benjamin]

What do you mean by 'make sure you depend on the "v4.15.0" revision of mathlib'? How do I do that without changing lean-toolchain?

[Benjamin]

I ran lake update --verbose, and this is the output:

trace: celine: updating 'mathlib' with {}
trace: .\.\.lake\packages\mathlib> git fetch --tags --force origin
trace: stderr:
error: cannot lock ref 'refs/remotes/origin/SM.AdjointTriangulated': is at 6372b3aa48ddaf69fadf52c677ee53f95f766deb but expected 8705b21ea16aa7d2b8b94af1295cd1f81f83586f
From https://github.com/leanprover-community/mathlib4
 ! 8705b21ea1..cc486a7f77  SM.AdjointTriangulated -> origin/SM.AdjointTriangulated  (unable to update local ref)
error: external command 'git' exited with code 1

[Ruben Van de Velde]

!

[Ruben Van de Velde]

At this point I would delete the .lake folder in your project directory and try again

[Benjamin]

I did that and now my lean-toolchain file says leanprover/lean4:v4.16.0-rc1, but I wanted leanprover/lean4:v4.15.0.

[Benjamin]

Is there a reason lake automatically updates to the release candidate? I prefer to use the stable release.

[Mauricio Collares]

Lake should never automatically update anything, but it will try to update lean-toolchain to match whatever version of mathlib is in your lake-manifest.json. If you're not requiring a specific version of mathlib in your lakefile, you can manually ask for mathlib updates by running lake update (which will update the manifest).

[Benjamin]

So if I update to the latest version of mathlib, do I have to use v4.16.0-rc1?

[Benjamin]

I think I understand now. Mathlib depends on v4.16.0-rc1, so updating mathlib bumps Lean to that version as well.

[Mauricio Collares]

Yes, mathlib tracks the most recent version of Lean, which is almost always an unstable one. But whenever a stable version of Lean is released, a mathlib commit compatible with that stable version is tagged v4.X.0 for the appropriate value of X. You can change your lakefile to point to such tags if you want to use a stable version.

[Jireh Loreaux]

Mauricio Collares said:

Lake should never automatically update anything

I don't think this is true at the moment. I think lake now always tries to update to the latest Lean toolchain (regardless of which one is specified in Mathlib), which has caused some recent headaches with downstream projects and the cache. But as I understand it, this is also on track to be fixed sometime this week.

[Mauricio Collares]

Do you mean it does that even if you don't run lake update? I've never seen that, and I'm curious now. Do you have an example?

[Mauricio Collares]

What I've definitely seen is lake updating the toolchain to match some dependency's lean-toolchain file, even if that dependency is not mathlib.

[Ruben Van de Velde]

Yes, this is a relatively new feature - mathlib has had something like it since before it was built into lake

[Ruben Van de Velde]

Now, right this week, you do not want to create a project that depends on the most recent version of mathlib. You should stick to the "v4.15.0" revision due to a bug that will hopefully be fixed in the next few days

[Mauricio Collares]

Ruben Van de Velde said:

Yes, this is a relatively new feature - mathlib has had something like it since before it was built into lake

Yes. lake update --keep-toolchain helps with that. But, still, I think the lean-toolchain overwriting only happens when you run lake update (or when you don't have a lake-manifest.json at all).