Problem getting ProofWidgets

Stream: general

[Jeremy Parker]

I'm trying to get set up to develop mathlib on a new machine and I'm having problems with lake (invoked through VS code) when it tries to download artifacts for proofWidgets

It looks like it's trying to get
https://github.com/leanprover-community/ProofWidgets4/releases/download/0.0.75-pre/ProofWidgets4.tar.gz
but it should instead be downloading
https://github.com/leanprover-community/ProofWidgets4/releases/download/v0.0.75-pre/ProofWidgets4.tar.gz
Notice the extra "v"

The output:

✖ [824/1474] (Optional) Fetching proofwidgets:optRelease (159ms)
trace: .> curl -s -S -f -o C:\Users\jparker002\mathlib4\.lake\packages\proofwidgets\.lake\ProofWidgets4.tar.gz -L https://github.com/leanprover-community/ProofWidgets4/releases/download/0.0.75-pre/ProofWidgets4.tar.gz
trace: stderr:
curl: (22) The requested URL returned error: 404
error: external command 'curl' exited with code 22
⚠ [825/1474] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (see 'proofwidgets:optRelease' for details)
✖ [826/1474] 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.

[Kenny Lau]

related to #mathlib4 > CI failure ?

[Sebastian Ullrich]

This issue has now been resolved. Users with checkouts that have already run into this issue will need to delete their .lake folder first (lake clean does not suffice in this case).

[tsuki（Hao Shen)]

Sebastian Ullrich said:

This issue has now been resolved. Users with checkouts that have already run into this issue will need to delete their .lake folder first (lake clean does not suffice in this case).

I just tried it, and it seems there's still an issue. :sob: I've tried rm -rf .lake && lake exe cache get

[Riccardo Brasca]

Does it work?

[Anatole Dedecker]

Works for me

[Sebastian Ullrich]

@tsuki（Hao Shen) Could you try running lake build -v and posting the error message of (likely) proofwidgets:optRelease as in the first post of this thread?

[tsuki（Hao Shen)]

截屏2025-09-22 21.43.14.png

[tsuki（Hao Shen)]

The error message is

✖ [1258/7253] (Optional) Fetching proofwidgets:optRelease (4.7s)
trace: .> curl -s -S -f -o /Users/tsuki/groebner_proj/.lake/packages/proofwidgets/.lake/ProofWidgets4.tar.gz -L https://github.com/leanprover-community/ProofWidgets4/releases/download/0.0.75-pre/ProofWidgets4.tar.gz
trace: stderr:
curl: (22) The requested URL returned error: 404
error: external command 'curl' exited with code 22
⚠ [1259/7253] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (see 'proofwidgets:optRelease' for details)
✖ [1260/7253] 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

[Sebastian Ullrich]

Mmh, could you try running

git -C .lake/packages/proofwidgets/ tag --delete 0.0.75-pre

?

[tsuki（Hao Shen)]

Sebastian Ullrich said:

Mmh, could you try running

git -C .lake/packages/proofwidgets/ tag --delete 0.0.75-pre

?

It works for me!

[Mattias Ehatamm]

Sebastian Ullrich said:

Mmh, could you try running

git -C .lake/packages/proofwidgets/ tag --delete 0.0.75-pre

?

thanks, this was really helpful!