Proof widget cloud release

Stream: mathlib4

[Andrew Yang]

After #14092, I start getting errors

info: proofwidgets: wanted prebuilt release, but no tag found for revision
warning: failed to fetch cloud release; falling back to local build

when running lake exe cache get, and

/Users/erd1/Desktop/lean/mathlib4/.lake/packages/proofwidgets/widget/node_modules/typescript/lib/tsc.js:92
  for (let i = startIndex ?? 0; i < array.length; i++) {
                           ^

SyntaxError: Unexpected token '?'

when using vscode, presumably because my node is too old to support the newest ECMAScript standard?

[Andrew Yang]

That is ES10... seems like I've never written JS for 3+ years...
Anyways I managed to dig through my nvm and updated node and the error went away.

[Joël Riou]

(deleted)

[Kim Morrison]

Oh dear, that is bad, we really don't want to require local builds here!

[Kim Morrison]

If anyone (@Andrew Yang?) can reproducibly get the "wanted prebuilt release" info message, please let us know ASAP.

[Kim Morrison]

@Wojciech Nawrocki, just a heads up on this thread, not sure there is anything to do for now.

[Andrew Yang]

Yes it is still the case for me.

[Kim Morrison]

Which OS? Which commit do you see this on?

[Andrew Yang]

MacOS Ventura 13.6.6.
Do you mean mathlib commit? I'm on current master i.e. 55f6240.

[Andrew Yang]

If it helps, this is the full lake -v exe cache get output

❯ lake -v exe cache get
⚠ [1/10] Fetched proofwidgets:optRelease
info: proofwidgets: wanted prebuilt release, but no tag found for revision
warning: failed to fetch cloud release; falling back to local build
ℹ [2/10] Replayed Cache.IO
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/build/lib /Users/erd1/.elan/toolchains/leanprover--lean4---v4.9.0-rc3/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././Cache/IO.lean -R ./././. -o ././.lake/build/lib/Cache/IO.olean -i ././.lake/build/lib/Cache/IO.ilean -c ././.lake/build/ir/Cache/IO.c --json
ℹ [3/10] Replayed Cache.Hashing
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/build/lib /Users/erd1/.elan/toolchains/leanprover--lean4---v4.9.0-rc3/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././Cache/Hashing.lean -R ./././. -o ././.lake/build/lib/Cache/Hashing.olean -i ././.lake/build/lib/Cache/Hashing.ilean -c ././.lake/build/ir/Cache/Hashing.c --json
ℹ [4/10] Replayed Cache.Requests
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/build/lib /Users/erd1/.elan/toolchains/leanprover--lean4---v4.9.0-rc3/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././Cache/Requests.lean -R ./././. -o ././.lake/build/lib/Cache/Requests.olean -i ././.lake/build/lib/Cache/Requests.ilean -c ././.lake/build/ir/Cache/Requests.c --json
ℹ [5/10] Replayed Cache.Main
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/build/lib DYLD_LIBRARY_PATH=././.lake/build/lib /Users/erd1/.elan/toolchains/leanprover--lean4---v4.9.0-rc3/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././Cache/Main.lean -R ./././. -o ././.lake/build/lib/Cache/Main.olean -i ././.lake/build/lib/Cache/Main.ilean -c ././.lake/build/ir/Cache/Main.c --json
ℹ [6/10] Replayed Cache.Main:c.o (with exports)
trace: .> /Users/erd1/.elan/toolchains/leanprover--lean4---v4.9.0-rc3/bin/leanc -c -o ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/Main.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [7/10] Replayed Cache.IO:c.o (with exports)
trace: .> /Users/erd1/.elan/toolchains/leanprover--lean4---v4.9.0-rc3/bin/leanc -c -o ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/IO.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [8/10] Replayed Cache.Hashing:c.o (with exports)
trace: .> /Users/erd1/.elan/toolchains/leanprover--lean4---v4.9.0-rc3/bin/leanc -c -o ././.lake/build/ir/Cache/Hashing.c.o.export ././.lake/build/ir/Cache/Hashing.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [9/10] Replayed Cache.Requests:c.o (with exports)
trace: .> /Users/erd1/.elan/toolchains/leanprover--lean4---v4.9.0-rc3/bin/leanc -c -o ././.lake/build/ir/Cache/Requests.c.o.export ././.lake/build/ir/Cache/Requests.c -O3 -DNDEBUG -DLEAN_EXPORTING
ℹ [10/10] Replayed cache
trace: .> /Users/erd1/.elan/toolchains/leanprover--lean4---v4.9.0-rc3/bin/leanc -o ././.lake/build/bin/cache ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/Hashing.c.o.export ././.lake/build/ir/Cache/Requests.c.o.export
No files to download
Decompressing 4702 file(s)
Unpacked in 1534 ms
Completed successfully!

[Kim Morrison]

Hmm, can't reproduce on that commit. @Andrew Yang, does it persist if you do a rm -rf .lake?

[Andrew Yang]

Seems to be gone now. Maybe it's just a transient issue.

[Ruben Van de Velde]

Kim Morrison said:

If anyone (@Andrew Yang?) can reproducibly get the "wanted prebuilt release" info message, please let us know ASAP.

I get it on 9f3f9927310c0cd0d1cc1b4114b099563221c597 (master 7bdafea99c391569e07ecb1d8a33a576e0c8b5ba)

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Oh dear, I also observed a discrepancy:
Scenario A:

1. Clone mathlib
2. lake exe cache get
3. lake build

Here all is well (so in particular, CI succeeded).

Scenario B:

1. Clone mathlib
2. lake build

Here the prebuilt release is not used and NPM starts building. This is not expected, right?

[Kim Morrison]

That is not expected!

[Kim Morrison]

@Ruben Van de Velde, could you explain how to reproduce what you see?

I tried

git checkout 7bdafea99c391569e07ecb1d8a33a576e0c8b5ba
lake exe cache get
lake build

and didn't see anything wrong.

[Kim Morrison]

@Wojciech Nawrocki, I can't reproduce your scenario B, however. I just ran:

git clone https://github.com/leanprover-community/mathlib4/
cd mathlib4
git checkout dc8cf8b25927b121ce49a85d620be120409d51a0
lake build

and a normal local build proceeds okay apparently. (I've removed npm locally for testing.)

[Ruben Van de Velde]

$ lake exe cache get
⚠ [1/10] Fetched proofwidgets:optRelease
info: proofwidgets: wanted prebuilt release, but no tag found for revision
warning: failed to fetch cloud release; falling back to local build
No files to download
Decompressing 4703 file(s)
Unpacked in 34 ms
Completed successfully!

[Ruben Van de Velde]

Doing the same in another clone seems to work

[Ruben Van de Velde]

So this seems almost certainly path dependent. I can keep this tree around for a bit if you want me to debug anything

[Kim Morrison]

But I need to know which commit you're on.

[Ruben Van de Velde]

9f3f9927310c0cd0d1cc1b4114b099563221c597

[Kim Morrison]

Hmm, can't reproduce, either before or after a rm -rf .lake.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kim Morrison said:

Wojciech Nawrocki, I can't reproduce your scenario B, however. I just ran:

git clone https://github.com/leanprover-community/mathlib4/
cd mathlib4
git checkout dc8cf8b25927b121ce49a85d620be120409d51a0
lake build

and a normal local build proceeds okay apparently. (I've removed npm locally for testing.)

Ah sorry, I must have lost track of which terminal I was looking at. Scenario B uses 2. lake build ProofWidgets (from within mathlib). However, if you don't do that and just run lake build, it all works.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

As for 'no tag found revision', a (rather far-fetched) hypothesis is that it is caused by the fact that we previously had a v0.0.37 release with different contents, after which point I removed the release and the tag, and then later made a different commit with the same tag. Maybe GitHub has a stale cache on some server?

[Kim Morrison]

Weird, now that I've uninstalled npm is seems easy to repro

git checkout dc8cf8b25927b121ce49a85d620be120409d51a0
rm -rf .lake
lake build

which prints

info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to '././.lake/packages/importGraph'
✖ [96/4707] Building proofwidgets/widgetJsAll
trace: ././.lake/packages/proofwidgets/widget> npm clean-install
trace: stderr:
could not execute external process 'npm'
error: external command 'npm' exited with code 255
⣽ [620/4707] Running Mathlib.Data.Int.Defs (+ 9 more)

(and then seems to continue into the Mathlib build)

[Kim Morrison]

So, what do we do? Move Mathlib back to v0.0.36 until we can sort this out?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kim Morrison said:

So, what do we do? Move Mathlib back to v0.0.36 until we can sort this out?

This seems necessary.

[Kim Morrison]

The rewritten v0.0.37 tag hypothesis isn't obviously correct, but it seems hard to rule out, as well. (Sorry for polluting your tags in my earlier attempts at doing this... :-(

[Kim Morrison]

Okay, I'll make that PR now.

[Kim Morrison]

#14113

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Kim Morrison said:

Weird, now that I've uninstalled npm is seems easy to repro

git checkout dc8cf8b25927b121ce49a85d620be120409d51a0
rm -rf .lake
lake build

which prints

info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to '././.lake/packages/importGraph'
✖ [96/4707] Building proofwidgets/widgetJsAll
trace: ././.lake/packages/proofwidgets/widget> npm clean-install
trace: stderr:
could not execute external process 'npm'
error: external command 'npm' exited with code 255
⣽ [620/4707] Running Mathlib.Data.Int.Defs (+ 9 more)

(and then seems to continue into the Mathlib build)

Can you still reproduce this now? I just tried those exact instructions, and it reliably builds using the cloud release for me.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Okay, regardless of the above, I think we finally have a correct lakefile thanks @Mac Malone's help; mathlib4#14198.

[Ralf Stephan]

How can I fix this on my machine? rm -rf .lake/ does not suffice:

ralf@ark:~/Lean/mathlib4> rm -rf .lake/
ralf@ark:~/Lean/mathlib4> lake exe cache get
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to '././.lake/packages/importGraph'
⚠ [1/10] Fetched proofwidgets:optRelease
info: proofwidgets: wanted prebuilt release, but no tag found for revision
warning: failed to fetch cloud release; falling back to local build
Attempting to download 4727 file(s)
Downloaded: 0 file(s) [attempted 4727/4727 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
No cache files to decompress
ralf@ark:~/Lean/mathlib4> lake build
⚠ [1/4731] Fetched proofwidgets:optRelease
info: proofwidgets: wanted prebuilt release, but no tag found for revision
warning: failed to fetch cloud release; falling back to local build
✖ [270/4731] Building proofwidgets/widgetJsAll
trace: ././.lake/packages/proofwidgets/widget> npm clean-install
info: stderr:
npm ERR! Cannot read properties of undefined (reading '@leanprover/infoview')

npm ERR! A complete log of this run can be found in:
npm ERR!     /home/ralf/.npm/_logs/2024-06-29T18_02_10_615Z-debug.log
error: external command 'npm' exited with code 1
Some builds logged failures:
- proofwidgets/widgetJsAll
error: build failed

[Ralf Stephan]

Never mind. I tried building in a branch, but in master it works now.

[Floris van Doorn]

I'm trying to update a repository, and I get the following error:

Floris@Dell-E MINGW64 ~/projects/BonnAnalysis (master)
$ lake exe cache get!
⚠ [1/10] Fetched proofwidgets:optRelease
info: proofwidgets: wanted prebuilt release, but no tag found for revision
warning: failed to fetch cloud release; falling back to local build
Attempting to download 4776 file(s)
Downloaded: 4776 file(s) [attempted 4776/4776 = 100%] (100% success)
Decompressing 4776 file(s)
Unpacked in 70274 ms
Completed successfully!

Floris@Dell-E MINGW64 ~/projects/BonnAnalysis (master)
$ lake build
⚠ [1/2093] Fetched proofwidgets:optRelease
info: proofwidgets: wanted prebuilt release, but no tag found for revision
warning: failed to fetch cloud release; falling back to local build
✖ [414/2093] Fetching proofwidgets:release
info: proofwidgets: wanted prebuilt release, but no tag found for revision
error: failed to fetch cloud release
Some builds logged failures:
- proofwidgets:release
error: build failed

Repo here: https://github.com/fpvandoorn/BonnAnalysis/tree/update

[Floris van Doorn]

Now trying again after (re)moving my .lake folder. Is it interesting if I share the contents of my .lake folder, or is it known what is going on?

[Notification Bot]

2 messages were moved here from #general > v4.10.0-rc1 discussion by Floris van Doorn.

[Floris van Doorn]

Deleting .lake did work for me. I still have a backup of the folder, if that is interesting.

[Floris van Doorn]

(This is with the latest Mathlib, so ProofWidgets was updated to v0.0.39)

[Kim Morrison]

Unfortunately this is just a known problem, and a lot of people are going to have to rm -rf .lake when moving to v4.10.0-rc1.

From what I understand there is reason to believe this is a one off, but @Mac Malone has been on vacation and I've also had some time off and I'm not certain of the details here.