cache rebuilding proofwidgets JS

Stream: mathlib4

[Damiano Testa]

After pulling the new master, removing .lake and getting the cache, lake build fails for me. Below is what I see.

I saw that there was some discussion about proofwidgets: should I do something special to make cache work again?

Thanks!

$ 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: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '././.lake/packages/LeanSearchClient'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
⚠ [13/24] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
Attempting to download 5235 file(s)
Downloaded: 5235 file(s) [attempted 5235/5235 = 100%] (100% success)
Decompressing 5235 file(s)
Unpacked in 6648 ms
Completed successfully!

$ lake build
⚠ [5/5247] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✖ [419/5247] 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
Some required builds logged failures:
- proofwidgets/widgetJsAll
error: build failed

[Ruben Van de Velde]

I'm guessing you don't have npm installed?

[Damiano Testa]

Oh, indeed:

$ npm
Command 'npm' not found, but can be installed with:
sudo apt install npm

[Damiano Testa]

Let me try again...

[Ruben Van de Velde]

Maybe relevant: #nightly-testing > ProofWidgets4 https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/mathlib4.20speedcenter/near/475832473

[Damiano Testa]

It's still not working, but I need to run now! I'll report better soon!

[Damiano Testa]

I think that I now see also errors from npm, but at the same time, the cache still is not working.

$ rm -rf .lake/

$ 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: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '././.lake/packages/LeanSearchClient'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
⚠ [13/24] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
No files to download
Decompressing 5235 file(s)
Unpacked in 6740 ms
Completed successfully!

$ lake build
⚠ [5/5247] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✖ [915/5247] Building proofwidgets/widgetJsAll
trace: ././.lake/packages/proofwidgets/widget> npm clean-install
trace: stdout:

added 267 packages, and audited 268 packages in 4s

29 packages are looking for funding
  run `npm fund` for details

[lots of lines that appear an npm report]

trace: ././.lake/packages/proofwidgets/widget> npm run build
trace: stdout:

> proofwidgets4@0.1.0 build
> npx tsc && rollup --environment NODE_ENV:production --config
trace: stderr:
/home/damiano/Matematica/Lean4/mathlib4/.lake/packages/proofwidgets/widget/node_modules/typescript/lib/tsc.js:92
  for (let i = startIndex ?? 0; i < array.length; i++) {
                           ^

SyntaxError: Unexpected token '?'
    at wrapSafe (internal/modules/cjs/loader.js:915:16)
    at Module._compile (internal/modules/cjs/loader.js:963:27)
    at Object.Module._extensions..js (internal/modules/cjs/loader.js:1027:10)
    at Module.load (internal/modules/cjs/loader.js:863:32)
    at Function.Module._load (internal/modules/cjs/loader.js:708:14)
    at Module.require (internal/modules/cjs/loader.js:887:19)
    at require (internal/modules/cjs/helpers.js:85:18)
    at Object.<anonymous> (/home/damiano/Matematica/Lean4/mathlib4/.lake/packages/proofwidgets/widget/node_modules/typescript/bin/tsc:2:1)
    at Module._compile (internal/modules/cjs/loader.js:999:30)
    at Object.Module._extensions..js (internal/modules/cjs/loader.js:1027:10)
error: external command 'npm' exited with code 1
Some required builds logged failures:
- proofwidgets/widgetJsAll
error: build failed

[Kim Morrison]

It's really important that this all works without npm installed.

[Kim Morrison]

So please don't install it to try to fix such problems. :-)

[Kim Morrison]

@Mac Malone?

[Damiano Testa]

Ok, I'll (happily) remove it

[Sebastian Ullrich]

warning: building from source; failed to fetch GitHub release (run with '-v' for details)

This is the relevant line, could you try that?

[Damiano Testa]

What does that mean?

[Damiano Testa]

lake exe cache get -v?

[Sebastian Ullrich]

The line is from build, so lake build -v

[Damiano Testa]

I get a really long list of trace outputs and finally

ℹ [5248/5251] Replayed Batteries.Util.Pickle
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/runner/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean -Dlinter.missingDocs=true ././././Batteries/Util/Pickle.lean -R ./././. -o ././.lake/build/lib/Batteries/Util/Pickle.olean -i ././.lake/build/lib/Batteries/Util/Pickle.ilean -c ././.lake/build/ir/Batteries/Util/Pickle.c --json
ℹ [5249/5251] Replayed Batteries
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/runner/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean -Dlinter.missingDocs=true ././././Batteries.lean -R ./././. -o ././.lake/build/lib/Batteries.olean -i ././.lake/build/lib/Batteries.ilean -c ././.lake/build/ir/Batteries.c --json
Some required builds logged failures:
- proofwidgets/widgetJsAll
error: build failed

[Damiano Testa]

It starts like this:

$ lake build -v
✖ [4/5251] (Optional) Fetching proofwidgets:optRelease
trace: .> curl -s -S -f -o ././.lake/packages/proofwidgets/.lake/ProofWidgets4.tar.gz -L ssh://git@github.com/leanprover-community/ProofWidgets4/releases/download/v0.0.43/ProofWidgets4.tar.gz
trace: stderr:
curl: (1) Protocol "ssh" not supported or disabled in libcurl
error: external command 'curl' exited with code 1
⚠ [5/5251] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (see 'proofwidgets:optRelease' for details)
ℹ [15/5251] Replayed Batteries.Tactic.Lint.Basic
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/runner/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean -Dlinter.missingDocs=true ././././Batteries/Tactic/Lint/Basic.lean -R ./././. -o ././.lake/build/lib/Batteries/Tactic/Lint/Basic.olean -i ././.lake/build/lib/Batteries/Tactic/Lint/Basic.ilean -c ././.lake/build/ir/Batteries/Tactic/Lint/Basic.c --json
ℹ [16/5251] Replayed Batteries.Tactic.Lint.Misc
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/runner/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean -Dlinter.missingDocs=true ././././Batteries/Tactic/Lint/Misc.lean -R ./././. -o ././.lake/build/lib/Batteries/Tactic/Lint/Misc.olean -i ././.lake/build/lib/Batteries/Tactic/Lint/Misc.ilean -c ././.lake/build/ir/Batteries/Tactic/Lint/Misc.c --json

[Sebastian Ullrich]

The interesting step is Ran proofwidgets:extraDep, it's likely near the top

[Damiano Testa]

lots of lines with traces, then

ℹ [394/5251] Replayed ImportGraph.Imports
trace: .> LEAN_PATH=././.lake/packages/Cli/.lake/build/lib:././.lake/packages/batteries/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/runner/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean ././././ImportGraph/Imports.lean -R ./././. -o ././.lake/build/lib/ImportGraph/Imports.olean -i ././.lake/build/lib/ImportGraph/Imports.ilean -c ././.lake/build/ir/ImportGraph/Imports.c --json
ℹ [418/5251] Replayed proofwidgets/widgetPackageLock
trace: ././widget> npm install
trace: stdout:

up to date, audited 269 packages in 891ms

29 packages are looking for funding
  run `npm fund` for details

found 0 vulnerabilities
✖ [419/5251] 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
ℹ [433/5251] Replayed Batteries.Tactic.Where
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH= /home/runner/.elan/toolchains/leanprover--lean4---v4.13.0-rc3/bin/lean -Dlinter.missingDocs=true ././././Batteries/Tactic/Where.lean -R ./././. -o ././.lake/build/lib/Batteries/Tactic/Where.olean -i ././.lake/build/lib/Batteries/Tactic/Where.ilean -c ././.lake/build/ir/Batteries/Tactic/Where.c --json
ℹ [542/5251] Replayed Batteries.Data.Nat.Gcd

[Damiano Testa]

then more lines with traces ending with what is above.

[Sebastian Ullrich]

curl: (1) Protocol "ssh" not supported or disabled in libcurl

Oh interesting, that definitely shouldn't happen

[Damiano Testa]

I'm glad to be interesting... :smile:

[Sebastian Ullrich]

I don't know why Lake would choose a different proofwidgets URL for you than, apparently, for everyone else

[Damiano Testa]

Also, this happened now, until today, I had no problem...

[Damiano Testa]

(Could have been in the last week, as I was not using this computer in the meantime, but another with a virtually identical setup.)

[Damiano Testa]

Is there a way that I can change the proofwidgets URL on my side, or is this something that I should not touch?

[Sebastian Ullrich]

Your lake-manifest.json is in fact in sync with master?

[Damiano Testa]

I think so:

$ git checkout origin/master lake-manifest.json
Updated 0 paths from 3c2bcdaae3

[Damiano Testa]

As an experiment, I cloned a new copy of mathlib, downloaded the cache and ran lake build, with the same outcome.

[Mac Malone]

@Damiano Testa For some reason, Lake has deduced an SSH URL for ProofWidgets. One thing I would check is what remote the ProofWidgets dependency is set to:

# in mathlib4
$ git -C .lake/packages/proofwidgets remote get-url origin

It should be the below, but I suspect it is probably not:

https://github.com/leanprover-community/ProofWidgets4

[Damiano Testa]

I get

ssh://git@github.com/leanprover-community/ProofWidgets4

I hope that this is different enough to justify what is happening!

[Kevin Buzzard]

I think it means that Mac's conjecture was correct!

[Damiano Testa]

Indeed, but I'm still not sure how to proceed. :smile:

[Adam Topaz]

one hack would be to edit the .git/config file and update the upstream url to that https one.

[Damiano Testa]

Adam, can you be a bit more explicit and tell me what I should write in .git/config? In my file, there is no mention of ProofWidgets...

[Damiano Testa]

Here is my .git/config file:

$ cat .git/config
[core]
    repositoryformatversion = 0
    filemode = true
    bare = false
    logallrefupdates = true
[remote "origin"]
    url = git@github.com:leanprover-community/mathlib4.git
    fetch = +refs/heads/*:refs/remotes/origin/*
[branch "master"]
    remote = origin
    merge = refs/heads/master

[Adam Topaz]

Sorry, I should have clarified: its .lake/packages/proofwidgets/.git/config. The file in my copy of mathlib looks like this:

[core]
    repositoryformatversion = 0
    filemode = true
    bare = false
    logallrefupdates = true
[remote "origin"]
    url = https://github.com/leanprover-community/ProofWidgets4
    fetch = +refs/heads/*:refs/remotes/origin/*
[branch "main"]
    remote = origin
    merge = refs/heads/main

[Adam Topaz]

But I don't think one is ever meant to edit files in the .lake/packages folder. That should all be handled properly by lake. I only made the suggestion to get you going again.

[Damiano Testa]

Ok, thanks! Anyway, my .lake/packages/proofwidgets/.git/config file is the same as yours:

[core]
    repositoryformatversion = 0
    filemode = true
    bare = false
    logallrefupdates = true
[remote "origin"]
    url = https://github.com/leanprover-community/ProofWidgets4
    fetch = +refs/heads/*:refs/remotes/origin/*
[branch "main"]
    remote = origin
    merge = refs/heads/main

[Mac Malone]

@Damiano Testa :exploding_head: Apparently Git is performing some magic to produce an SSH URL despite the repository being configured with a HTTPS one. I have no clue why (my attempts ot search for a reason this could happen failed). However, ProofWidgets4#83 should prevent whatever magic is happening is here from causing problems in the future.

[Mac Malone]

Hmm, a little more searching just now returned a Git feature that could be the culprit:

git config [--global] url.<base>.insteadOf <other_url>

(StackOverflow, Git Docs, StackOverflow example for GitHub)

[Mac Malone]

Maybe check if your global git config has this option set? (e.g., ~/.gitconfig or git config --global -e)

[Kevin Buzzard]

If it helps, I once had some git-related problem which nobody else had, and I pasted the output of git config -l here and within 4 minutes Ruben pointed out my problem and how to fix it!

[Damiano Testa]

From the home dir, I get

$ git config -l
user.email=adomani@gmail.com
user.name=adomani
core.editor=code --new-window --wait
core.excludesfile=/home/damiano/.gitignore
url.ssh://git@github.com/.insteadof=https://github.com/

and the last line looks promising...

[Damiano Testa]

Should I just delete it? I still would like to use ssh to log into git (and I thought that this was required since a few months).

[Damiano Testa]

@Mac Malone Is there a way that I can test the fix that you mention above?

[Ruben Van de Velde]

I would consider that quite a risky option, yeah. You can always change the remote in individual repositories, I believe

[Damiano Testa]

Ruben, the "risky option" is using https, right?

[Damiano Testa]

Besides, before changing anything in my configuration, I think that trying out the fix proposed above could be a good test for it.

[Mac Malone]

@Damiano Testa A global URL override like this is quite disruptive. I think the standard pratice is to set SSH urls on the indivudal repository remotes you plan to push to. However, should you not wish to change your practice, the ProofWidgets patch will hopefully fix this.

[Mac Malone]

To beta test the fix, you could manually apply the releaseRepo := patch to your current .lake/packages/proofwidgets/lakefile.lean.

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

The URL fix is merged now in v0.0.44-pre2. The proper v0.0.44 release should come out when mathlib moves over to the next Lean version.

[Damiano Testa]

I scanned the .lake/packages/proofwidgets/lakefile.lean file and I could not find releaseRepo := in it, so I give up trying to check whether the fix works on my computer.

[Damiano Testa]

Unsetting the global git option does fix the build, though!

[Damiano Testa]

Thanks for your help debugging this!

[Yury G. Kudryashov]

Now I'm getting the same error.

[Yury G. Kudryashov]

I've temporarily installed npm but this is probably not the right way to go.

[Yury G. Kudryashov]

I'm using ProofWidgets v0.0.43

[Yury G. Kudryashov]

I have *insteadOf in my git config but disabling them didn't work (and I override towards https, not ssh).

[Kim Morrison]

I just advanced the Mathlib toolchain from v4.13.0-rc3 to v4.13.0. @Mac Malone ?!?

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

@Kim Morrison I think this is just because Mac's fixes to the PW4 lakefile are included in 0.0.44, but mathlib is still on 0.0.43.

[Mac Malone]

Yury G. Kudryashov said:

Now I'm getting the same error.

What do you mean by "the same error"? The SSH one? Or simply the original "failed to fetch" error?

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

#18529 should fix this.

[Yury G. Kudryashov]

I was getting the "npm not found" error.

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

Yury G. Kudryashov said:

I was getting the "npm not found" error.

Hmm, that's different, but it does arise as a consequence of the cloud release failing to fetch, so hopefully fixing that should fix it for you.

[Eric Wieser]

Wojciech Nawrocki said:

#18529 should fix this.

@Kim Morrison, should the v4.13.0 tag in mathlib be moved to point here?

[Bhavik Mehta]

I am also getting the error "could not execute external process 'npm'", when building an external project on v4.13.0. I can't figure out from the above messages what the fix is (or if one exists?)

[Kim Morrison]

Eric Wieser said:

Wojciech Nawrocki said:

#18529 should fix this.

Kim Morrison, should the v4.13.0 tag in mathlib be moved to point here?

Sorry, missed this earlier. I've updated the tag now.

[Kim Morrison]

@Bhavik Mehta, if you can point your external project to the new v4.13.0 tag on Mathlib (or later), and let us know if that fixes things for you?

[Bhavik Mehta]

Seems to work, thanks!

[Wrenna Robson]

I am also getting this issue suddenly for no particular reason...

[Kim Morrison]

@Wrenna Robson, could you give some more details? Which project/commit? Is it something reproducible we can look at?

[Bhavik Mehta]

And also, does the fix suggested above by Kim work for you too?

[Wrenna Robson]

I am afraid I don't know how to reproduce it, but nuking my .lake worked.

[Bhavik Mehta]

Just to report that I saw this happen again when helping a Lean-beginner - they were on a project on v4.14.0-rc2, and the same npm error happened. get cache + clean + get cache is what caused it, then nuking .lake and doing clean + get cache fixed it. Unfortunately I don't quite know how to reproduce it, but recording this in case others get it too.

[Kim Morrison]

(Helpful with reports like this to include the SHA of "current master".)

[Bhavik Mehta]

(In the case I mentioned it was aef008c6189004dead2c9ab604463667f2003202)

[Sebastian Ullrich]

Parallel discussion: #mathlib4 > CI building ProofWidgets every time

[Bhavik Mehta]

Is that the same issue as this one? I don't see mention of "npm not found" errors there

[Notification Bot]

A message was moved from this topic to #mathlib4 > CI building ProofWidgets oleans every time by Sebastian Ullrich.

[Sebastian Ullrich]

Bhavik Mehta said:

Is that the same issue as this one? I don't see mention of "npm not found" errors there

Okay, I think I've now split the two threads by that distinction

[Heather Macbeth]

I have this "npm not found" ProofWidgets error on my mathlib currently. Is there a known fix yet?

[Eric Wieser]

When this happened to me it meant I had no network connection

[Eric Wieser]

The logic is something like

try
  fetchFromTheWeb
catch _ =>
  tryRunningNPM

[Heather Macbeth]

Hmm, but I am connected to the internet!

[Heather Macbeth]

Bhavik Mehta said:

nuking .lake and doing clean + get cache fixed it.

Is this the current recommended fix?

[Heather Macbeth]

OK, I just did that and it worked. (Seems like it would be useful to have a lake command lake really-clean which nukes .lake, is that on the roadmap?)

[Kim Morrison]

Pinging @Mac Malone. :-)

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

Does the fact that fully removing .lake fixes some of these issues indicate unsound (i.e., happens but should not happen) caching?

[Kim Morrison]

We are hoping that @Mac Malone's #19728 (just sent to bors) resolves the problem.