Issue running lake update

Stream: lean4

[Wrenna Robson]

The last day or so, when running lake update or lake exe cache get, I got the following error the first time:

✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required targets logged failures:
- proofwidgets:release

Though it then completes successfully. Running the same command again it seems to be fine - but this has happened in a few repos for me. Anyone know what's going on?

[Kevin Buzzard]

I saw this phenomenon in FLT today and also in a student's repo-which-depended-on-mathlib. Trying it now on a machine at home:

buzzard@brutus:~/FLT$ git pull
[stuff I did today on a machine at work, including a bump from 4.22.0 to 4.23.0-rc2, gets pulled]
buzzard@brutus:~/FLT$ lake exe cache get
info: downloading https://releases.lean-lang.org/lean4/v4.23.0-rc2/lean-4.23.0-rc2-linux.tar.zst
416.3 MiB / 416.3 MiB (100 %)   8.8 MiB/s ETA:   0 s
info: installing /home/buzzard/.elan/toolchains/leanprover--lean4---v4.23.0-rc2
info: mathlib: checking out revision '9e0bebc63f8bcc1df0884cafebaab2673c6d57b0'
info: plausible: checking out revision '240eddc1bb31420fbbc57fe5cc579435c2522493'
info: LeanSearchClient: checking out revision '99657ad92e23804e279f77ea6dbdeebaa1317b98'
info: importGraph: checking out revision 'dba7fbc707774d1ba830fd44d7f92a717e9bf57f'
info: proofwidgets: checking out revision '6e47cc88cfbf1601ab364e9a4de5f33f13401ff8'
info: aesop: checking out revision '3b779e9d1c73837a3764d516d81f942de391b6f0'
info: Qq: checking out revision 'f85ad59c9b60647ef736719c23edd4578f723806'
info: batteries: checking out revision '6e89c7370ca3a91b7d1f29ef7d727a9d027d7b0d'
info: Cli: checking out revision 'cacb481a1eaa4d7d4530a27b606c60923da21caf'
✖ [2/2] Running proofwidgets:release
error: failed to fetch GitHub release (run with '-v' for details)
Some required targets logged failures:
- proofwidgets:release
Current branch: HEAD
Using cache from origin: leanprover-community/mathlib4
Attempting to download 7091 file(s) from leanprover-community/mathlib4 cache
[etc etc]

and everything seems to work fine.

[Ruben Van de Velde]

Yeah, I've been seeing ignorable warnings about proof widgets as well

[Michael Stoll]

I'm seeing it right now when updating my repos to v4.23.0.
Maybe this should be fixed?

[Kim Morrison]

@Mac Malone, do you know what is going on here? I've been seeing this too, but it seems to have no ill effects.

[Mac Malone]

@Kim Morrison This is caused by an unfortunate interaction between optional builds (i.e., the proofwidgets release) and the new --no-build approach. I have fixing this on my TODO list, but I have ye to prioitize it is not currently breaking anything.

[Bulhwi Cha]

I tried to update the Lean toolchain, but got the following error:

chabulhwi@desktop ~/l/lean-playground (master)> lake update
info: toolchain not updated; already up-to-date
info: mathlib: running post-update hooks
✖ [2/12] Building Cache.Lean
trace: .> LEAN_PATH=/home/chabulhwi/lean-projects/lean-playground/.lake/packages/batteries/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/Qq/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/aesop/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/importGraph/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/plausible/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/BibtexQuery/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/Cli/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/mathlib/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/doc-gen4/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/packages/Paperproof/lean/.lake/build/lib/lean:/home/chabulhwi/lean-projects/lean-playground/.lake/build/lib/lean /home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.23.0/bin/lean /home/chabulhwi/lean-projects/lean-playground/.lake/packages/mathlib/Cache/Lean.lean -o /home/chabulhwi/lean-projects/lean-playground/.lake/packages/mathlib/.lake/build/lib/lean/Cache/Lean.olean -i /home/chabulhwi/lean-projects/lean-playground/.lake/packages/mathlib/.lake/build/lib/lean/Cache/Lean.ilean -c /home/chabulhwi/lean-projects/lean-playground/.lake/packages/mathlib/.lake/build/ir/Cache/Lean.c --setup /home/chabulhwi/lean-projects/lean-playground/.lake/packages/mathlib/.lake/build/ir/Cache/Lean.setup.json --json
error: Cache/Lean.lean:7:0: object file '/home/chabulhwi/.elan/toolchains/leanprover--lean4---v4.23.0/lib/lean/Lean/Util/Paths.olean' of module Lean.Util.Paths does not exist
error: Lean exited with code 1
Some required targets logged failures:
- Cache.Lean
error: build failed

[Bulhwi Cha]

Jon Eugster said:

If that doesn't work, post the content of your lean-toolchain and your lakefile.lean (or .toml), at least the part about the required dependencies.

Never mind. I hadn't updated my lakefile.toml file.

[Kim Morrison]

Mac Malone said:

Kim Morrison This is caused by an unfortunate interaction between optional builds (i.e., the proofwidgets release) and the new --no-build approach. I have fixing this on my TODO list, but I have ye to prioitize it is not currently breaking anything.

Okay, if it's possible to bump it up I would vote for that. It's not actually breaking, but we're showing a spurious error message to every user, and it's burning cycles ignoring it.