lake behaviour not clear

Stream: general

[Alexandre Rademaker]

I tried to update my code to Lean v4.25.0-rc2, but I got the error:

✖ [120/1438] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.

Since I have not found a solution. I cleaned up the repo

% rm -rf lake-manifest.json .lake

and manually updated the lean-toolchain to

leanprover/lean4:v4.24.0

After that, I executed

% lake build
info: fad: no previous manifest, creating one from scratch
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4
info: leanprover-community/mathlib: checking out revision 'afa82c7ce3e4de5ce7506b6766458e0b3386e0f5'
info: updating toolchain to 'leanprover/lean4:v4.25.0-rc2'
...
✖ [120/1438] Building proofwidgets/widgetJsAll
error: ProofWidgets not up-to-date. Please run `lake exe cache get` to fetch the latest ProofWidgets. If

So back to the same error! Why did the lake update to v4.25.0-rc2 automatically? What is the proper way to say 'I want to use Lean version X`

I see some error in the output of the build with -v

ℹ [451/536] Replayed proofwidgets/widgetPackageLock
trace: ././widget> npm install
trace: stdout:
added 1 package, changed 2 packages, and audited 367 packages in 2s

67 packages are looking for funding
  run `npm fund` for details

1 moderate severity vulnerability

To address all issues, run:
  npm audit fix

Run `npm audit` for details.

After running npm audit fix I got the same error!

[Malvin Gattinger]

Is your project using mathlib? What does your lakefile.toml look like?

As lake --help says: "A bare lake update will upgrade all dependencies." so if you depend on something that in its latest version wants to have a newer toolchain then lake update will also update your toolchain, I think.

(In my own projects this is why I prefer to pin a specific version of mathlib too.)

[Alexandre Rademaker]

You are right. I believe I had learn that before, but I forgot. Previously, my lakefile.toml had only:

[[require]]
name = "mathlib"
scope = "leanprover-community"

So no rev specified. So the main point here is that lean-toolchain does not dictate the version; it can be updated by the dependencies. Once I fixed the rev of Mathlib, I can now work with v4.24.0.

[Kim Morrison]

I'd like to understand the problem you're having on v4.25.0-rc2, nevertheless. Can you provide a commit SHA in a repository, such that lake build will produce the "error: ProofWidgets not up-to-date." message, but run lake exe cache get does not resolve the problem?

[Anthony Wang]

This seems to be the same bug as #new members > ProofWidgets not building, says it is out of date