Zulip Chat Archive

Stream: mathlib4

Topic: Building proofwidgets/widgetJsAll failed for v4.25.0


Stefan Kusterer (Nov 15 2025 at 07:17):

Hello,
I just tried to upgrade from v4.24.0 to v4.25.0 and got error: build failed - see below.
I ran the following command sequence twice, first with .lake unchanged and then a second time
after rm -rf .lake. Unfortunately, the result was the same.
How can I fix this?
Thanks for your support in advance!
Kind Regards, Stefan

■■■■■■■■■■■■■■■:~/math$ lake update
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4
info: leanprover-community/mathlib: checking out revision '029db123ddaa7f8fd0d18cea3b1b33bf84dacd1e'
info: toolchain not updated; already up-to-date
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '2503bfb5e2d4d8202165f5bd2cc39e44a3be31c3'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '2ed4ba69b6127de8f5c2af83cccacd3c988b06bf'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '009064c21bad4d7f421f2901c5e817c8bf3468cb'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'fb8ed0a85a96e3176f6e94b20d413ea72d92576d'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '26e4c7c0e63eb3e6cce3cf7faba27b8526ea8349'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '2781d8ad404303b2fe03710ac7db946ddfe3539f'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '39260e31b7b3f7f05643da95242463b462dc05f1'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '1dae8b12f8ba27576ffe5ddee78bebf6458157b0'
info: mathlib: running post-update hooks
Not running `lake exe cache get` yet, as the `lake` version does not match the toolchain version in the project.
You should run `lake exe cache get` manually.
■■■■■■■■■■■■■■■:~/math$ lake exe cache get
Fetching ProofWidgets cloud release... done!
Current branch: HEAD
Using cache (Azure) from origin: leanprover-community/mathlib4
No files to download
Decompressing 7506 file(s)
Unpacked in 19769 ms
Completed successfully!
■■■■■■■■■■■■■■■:~/math$ lake build
 [472/501] 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.
 [3011/3015] Built Math.Problem002_2
warning: Math/Problem002_2.lean:153:8: declaration uses 'sorry'
Some required targets logged failures:
- proofwidgets/widgetJsAll
error: build failed

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 (Nov 15 2025 at 07:18):

Hi @Stefan Kusterer ! I think this is currently being discussed in #new members > ProofWidgets not building, says it is out of date . Are you also using the v4.25.0 tagged release of mathlib?

Stefan Kusterer (Nov 15 2025 at 07:20):

Hello @𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 ,

Are you also using the v4.25.0 tagged release of mathlib?

Yes


Last updated: Dec 20 2025 at 21:32 UTC