An error regarding "widgetJsAll"

Stream: lean4

[Youngju Song]

Hi team, I am facing an error during lake build and it tells me to report this issue to Lean Zulip:

$ lake build
✖ [470/624] 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.
Some required targets logged failures:
- proofwidgets/widgetJsAll
error: build failed
$ lake exe cache get
Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
No files to download
Decompressing 7402 file(s)
Unpacked in 8088 ms
Completed successfully!
$ lake build
✖ [470/560] 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.
Some required targets logged failures:
- proofwidgets/widgetJsAll
error: build failed

Lean version is:

$ cat lean-toolchain
leanprover/lean4:v4.25.0-rc2%

not sure what more information should I accompany.

[Kevin Buzzard]

You could try rm -rf .lake and then starting again with lake exe cache get or whatever, but indeed there was a problem with proofwidgets recently. If this doesn't fix it then ask again.

[Damiano Testa]

There is also #mathlib4 > Building proofwidgets/widgetJsAll failed for v4.25.0, which may be relevant.

[Youngju Song]

@Kevin Buzzard Actually I have already underwent that process. Let me try that once more and get back to you.

[Kevin Buzzard]

Sounds like (reading the other threads) you might want to bump to v4.25.1.

[Youngju Song]

@Kevin Buzzard rm -rf .lake did not work. Let me try v4.25.1. Thank you for your help!!