Zulip Chat Archive
Stream: mathlib4
Topic: ProofWidgets not up-to-date.
xinrui zhang (Jul 03 2025 at 03:19):
I entered the "lake build" command in the terminal of the MATHEMATICE _IN_LEAN project, and it prompted me "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." I have re-entered the "lake exe cache get" command according to his instructions, but after entering "lake build" again, the same problem occurs. How can I solve it?
PS D:\0.lean\mathematics_in_lean> lake exe cache get
Mathlib repository: leanprover-community/mathlib4
No files to download
Decompressing 6772 file(s)
Unpacked in 288 ms
Completed successfully!
PS D:\0.lean\mathematics_in_lean> lake build
ℹ [1/377] Replayed MIL.C01_Introduction.S01_Getting_Started
info: D:\0.lean\mathematics_in_lean\MIL\C01_Introduction\S01_Getting_Started.lean:1:0: "Hello, World!"
✖ [418/701] 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.
⣷ [1290/2931] Running Mathlib.Order.Bounds.OrderIso (+ 5 more)
Aaron Liu (Jul 03 2025 at 11:28):
Try lake clean and then lake exe cache get again
Last updated: Dec 20 2025 at 21:32 UTC