Updating mathlib4

Stream: mathlib4

[Dan Velleman]

I have a project that uses a little bit of mathlib4. When something I want to use gets added to mathlib4, I update the version in my project, and it never goes smoothly.

My lakefile.lean file contains:

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

When I want to update mathlib4, I give the command lake update in the terminal. Then I update my lean-toolchain file to match the lean-toolchain file in mathlib, and I restart Lean. It starts building files, and usually at some point I get an error message. I restart Lean again, or I quit VSCode and then reopen it, and the building process starts again. Sometimes I get errors more than once. Eventually it completes and everything is fine, so it's more of an annoyance than a serious problem. But why do I keep getting errors? Am I doing something wrong?

Here's the most recent error I got:

Watchdog error: no such file or directory (error code: 2)
  file: ./lake-packages/mathlib/build/lib/Mathlib/Order/BoundedOrder.olean.tmp
[Error - 9:36:21 AM] Client Lean 4: connection to server is erroring. Shutting down server.
[Error - 9:36:21 AM] Connection to server got closed. Server will not be restarted.
[Error - 9:36:21 AM] Stopping server failed
  Message: Pending response rejected since connection got disposed
  Code: -32097
[Error - 9:36:21 AM] Stopping server failed
  Message: Pending response rejected since connection got disposed
  Code: -32097

[Arthur Paulino]

This is looking more like a general Lake issue. I believe the #lean4 stream is more appropriate for this discussion

[Jeremy Avigad]

There are issues with dependencies. lake update updates all the packages the project depends on, which may or may not be compatible. with each other and with the latest version of mathlib.

Instead, I avoid lake update and try to update the dependencies for mathlib by hand. I do that by changing the version of mathlib4 in my lake-manifest.json file to the latest commit, and then I go to the corresponding file in the mathlib4 repository, and cut-and-paste those into my lake-manifest.json file as well:
https://github.com/leanprover-community/mathlib4/blob/master/lake-manifest.json

Then I do lake build, and, I think, that usually works.

[Ruben Van de Velde]

When doing an update like that, I'd quit all vscode processes and build with lake build from the terminal - not sure if that would help with your issue

[Sebastian Ullrich]

I have been annoyed by these errors as well the few times I've used mathlib4 so far, https://github.com/leanprover/lean4/pull/2144 should help with that

[Jon Eugster]

For lean.math.hhu.de, which updates to the newest mathlib multiple times a day, I have now the following routine in a crontab:

(cd MyProject &&
  rm -f ./lake-manifest.json &&
  lake update && # download latest mathlib
  cp ./lake-packages/mathlib/lean-toolchain . && # copy lean version of mathlib
  lake exe cache get &&
  lake build)

with this in the lakefile.lean:

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

This has worked for me for the last couple months now.

[James Gallicchio]

Jon's process should "just work" so long as mathlib is the only dependency explicitly listed in your lakefile.

@Jeremy Avigad Lake now looks at the dependencies of your dependencies to find compatible versions (e.g. what you're doing manually right now). Do you have mathlib's transitive dependencies in your lakefile?

[Jeremy Avigad]

My lakefile requires only mathlib and Marc Huisinga's Cli. Jon's process sounds good! I'll try that next time I update.