Proofwidgets now needs `npm`?

Stream: general

[Sky Wilshaw]

I've just run a fresh clean and rebuild of my project, and I'm getting the following error (Windows 11) - do we now need npm to build proofwidgets, even with cache? This seems like something's misconfigured.

PS C:\Users\skywi\Documents\code\con-nf> lake exe cache clean!
PS C:\Users\skywi\Documents\code\con-nf> lake exe cache get
Attempting to download 5641 file(s)
Downloaded: 5641 file(s) [attempted 5641/5641 = 100%] (100% success)
Decompressing 5641 file(s)
Unpacked in 42721 ms
Completed successfully!
PS C:\Users\skywi\Documents\code\con-nf> lake build
Ô£û [440/1047] Building proofwidgets/widgetJsAll
trace: .\.\.lake\packages\proofwidgets\widget> npm.cmd clean-install
error: failed to execute 'npm.cmd': no such file or directory (error code: 2)
Some required builds logged failures:
- proofwidgets/widgetJsAll
error: build failed
PS C:\Users\skywi\Documents\code\con-nf> lake build
Ô£û [440/1047] Building proofwidgets/widgetJsAll
trace: .\.\.lake\packages\proofwidgets\widget> npm.cmd clean-install
error: failed to execute 'npm.cmd': no such file or directory (error code: 2)
Some required builds logged failures:
- proofwidgets/widgetJsAll
error: build failed
PS C:\Users\skywi\Documents\code\con-nf> npm
npm : The term 'npm' is not recognized as the name of a cmdlet, function, script file, or operable program. Check the
spelling of the name, or if a path was included, verify that the path is correct and try again.
At line:1 char:1
+ npm
+ ~~~
    + CategoryInfo          : ObjectNotFound: (npm:String) [], CommandNotFoundException
    + FullyQualifiedErrorId : CommandNotFoundException

PS C:\Users\skywi\Documents\code\con-nf>

[Julian Berman]

I think #mathlib4 > cache rebuilding proofwidgets JS (and maybe one other recent thread) is relevant.

[Julian Berman]

Looks like rm -r .lake and then trying again is probably your first step at the minute.

[Sky Wilshaw]

Thanks, I'll give it a shot.

[Sky Wilshaw]

That seems to have done the trick, thanks!

[Kim Morrison]

I think we now have a fix in place for this, so hopefully it's not going to keep happening!

[Nailin Guan]

I think I met this problem too just now, even after re-downloading the repo it still have this problem.
图片.png

[Kim Morrison]

Could you give the exact instructions for reproducing? That would be really helpful.

[Nailin Guan]

This happens after only running lake exe cache get in a newly cloned Mathlib4, when building it got this error. Sorry that I don't know anything else that might cause this.

[Nailin Guan]

But it is resolved for now, after deleting .lake and rerun lake exe cache get, I don't really know the difference between the two.

[Kim Morrison]

@Nailin Guan, unfortunately I can't reproduce. When did you do this? If it happens again, to you or anyone else, please ignore the git SHA for the commit you were using. This may be essential for reproducing whatever problems are occurring.

Here's what I see, on a machine without npm installed:

kim@carica scratch % git clone git@github.com:leanprover-community/mathlib4.git
Cloning into 'mathlib4'...
remote: Enumerating objects: 688856, done.
remote: Counting objects: 100% (8116/8116), done.
remote: Compressing objects: 100% (3922/3922), done.
remote: Total 688856 (delta 5613), reused 6228 (delta 4152), pack-reused 680740 (from 1)
Receiving objects: 100% (688856/688856), 312.67 MiB | 8.43 MiB/s, done.
Resolving deltas: 100% (559449/559449), done.
Updating files: 100% (5858/5858), done.
kim@carica scratch % cd mathlib4
kim@carica mathlib4 % git rev-parse HEAD
deb1faaee197406368b6bc1f680c5c242c955045
kim@carica mathlib4 % lake exe cache get
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '8e5cb8d424df462f84997dd68af6f40e347c3e35'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision 'd7caecce0d0f003fd5e9cce9a61f1dd6ba83142b'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'ed3b856bd8893ade75cafe13e8544d4c2660f377'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '2b000e02d50394af68cfb4770a291113d94801b5'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '8b6048aa0a4a4b6bcf83597802d8dee734e64b7e'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'ad942fdf0b15c38bface6acbb01d63855a2519ac'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '7805acf1864ba1a2e359f86a8f092ccf1438ad83'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '0c8ea32a15a4f74143e4e1e107ba2c412adb90fd'
Attempting to download 3296 file(s)
Downloaded: 3296 file(s) [attempted 3296/3296 = 100%] (100% success)
Decompressing 5698 file(s)
Unpacked in 12969 ms
Completed successfully!
kim@carica mathlib4 % lake build
Build completed successfully.

[Kim Morrison]

It will really help the next time anyone encounters this if they can give the exact steps that led up to it, including the git SHA of the branch they are on. But even with that it may be a transient issue with some corruption inside .lake... Hopefully not!

[Kim Morrison]

I just encountered this again, but was unable to reproduce. What I didn't try was zipping up the contents of .lake, and seeing if I could reproduce using that.

[Eric Wieser]

I ran into it while trying to prepare a hot cache of both the latest mathlib head and two previous stable releases, possibly also with some lake exe cache unpacks mixed in

[Nailin Guan]

Maybe this is just some problem with my internet connection, never mind.

[Eric Wieser]

Could the logic be changed so that the behavior isn't dependent on how reliable the Internet connection is?

[Eric Wieser]

That is, make the user set a PROOFWIDGETS_LOCAL_BUILD environment variable or something if they want the npm build, and let the network error propagate normally when this isn't set.

[Filippo A. E. Nuccio]

I just run in the same problem with SHA
bfa197c8cff3cb63a8115130b7a43ef4cb15efbe

[Filippo A. E. Nuccio]

I am now trying to delete .lake and move on.

[Filippo A. E. Nuccio]

Indeed, after deleting the .lake folder altogether and calling lake exe cache get everything works perfectly./

[Mac Malone]

A fix for what is believed to be the issue here is up at mathlib4#19728.

[Bhavik Mehta]

I hit this problem again on 4.15.0

[Bhavik Mehta]

mathlib SHA 9837ca9d65d9de6fad1ef4381750ca688774e608

[Mauricio Collares]

I think the current diagnosis is that the error now means "the prebuilt version couldn't be fetched, so we are building it from source". Unfortunately this information is probably cached, so you might have to delete .lake/packages/proofwidgets/.lake/build and try again

[Mauricio Collares]

But if the fetch failure is indeed cached, that's still good to report

[Bhavik Mehta]

I've done the usual fix of deleting .lake and doing clean + get cache twice, and I'm still getting the npm error

[Mauricio Collares]

Oh, that's bad

[Bhavik Mehta]

Yeah, no idea how to resolve this...

[Mauricio Collares]

Does lake build --no-build proofwidgets:release print anything else?

[Bhavik Mehta]

That says build completed successfully

[Mauricio Collares]

And then lake build proofwidgets:releaseerrors out, I assume

[Bhavik Mehta]

That also builds successfully

[Mauricio Collares]

Which file fails to build when you do a normal lake build?

[Bhavik Mehta]

$ lake build
✖ [416/5851] Building proofwidgets/widgetPackageLock
trace: ././.lake/packages/proofwidgets/widget> npm install
trace: stderr:
could not execute external process 'npm'
error: external command 'npm' exited with code 255
Some required builds logged failures:
- proofwidgets/widgetPackageLock
error: build failed

[Sky Wilshaw]

Incidentally, my cache seems to be broken, even after executing cache get it needs to rebuild mathlib since updating yesterday. Could be linked?

[Bhavik Mehta]

That might be #mathlib4 > lake exe cache get error instead. Right now I'm on 4.15.0, which I think doesn't have that problem

[Mauricio Collares]

Hmm, ProofWidgets in mathlib was bumped straight from 0.0.48 (4.15.0-rc1) to 0.0.50 (4.16.0-rc1).lake-manifest.json at the v4.15.0 mathlib tag points to ProofWidgets 0.0.48. The 0.0.49 release corresponds to v4.15.0. That shouldn't matter unless there were breaking changes, but maybe the cloud release feature needs an exact match.

[Mauricio Collares]

Still, I don't see why this would fail on some machines and not others (and it works for me)

[Bhavik Mehta]

Oh, maybe it has to do with how my manifest references proofwidgets

[Kim Morrison]

@Bhavik Mehta, could you give us a complete repro? (e.g. git clone ...; git checkout ...; lake exe cache get; lake build, and on which OS?)

[Kim Morrison]

Just checking out Mathlib master at that commit (v4.15.0) I can't reproduce.

[Bhavik Mehta]

Yes, sorry I should have clarified that this is on a project depending on mathlib, rather than mathlib itself

[Bhavik Mehta]

I'll wipe everything and try to repro again, one moment. I'm on MacOS Ventura

[Kim Morrison]

Trying to reproduce by rebasing #20532 onto v4.15.0. Have to run to a meeting now.

[Kim Morrison]

It's working fine for me in a downstream project, also on macos.

[Bhavik Mehta]

Bah, I fixed it. The problem was that my version of ProofWidgets in the manifest was 0.0.50

[Bhavik Mehta]

Thanks for the attempt anyway Kim!

[Sebastian Ullrich]

How did you end up in that state, through lake update? That would still be something worth investigating

[Mauricio Collares]

I assume you can get there by running lake update to update to mathlib master, then editing the lakefile and running lake update mathlib to downgrade to v4.15.0

[Mauricio Collares]

Oh, I just tested it and I'm wrong. Sorry!

[Bhavik Mehta]

Sebastian Ullrich said:

How did you end up in that state, through lake update? That would still be something worth investigating

Unfortunately that might be self-inflicted - I was intending to be on 4.15.0 but something changed it to 4.16.0-rc1, and to downgrade I changed the SHAs in the manifest manually. And I presumably copied the wrong one for ProofWidgets, to end up with this error.

I tried to reproduce what changed my toolchain (with Marc) but I've had no luck yet.