Npm errors when building proof widgets from mathlib4

Stream: mathlib4

[Jonathan Reicher]

Hey, I've been running into an issue building a mathlib project with lean4. When cloning the repo, and immediatly after running lake build I run into the following error:

info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision '50c9a9bd433367a722e0b109c04b3514e0eb2ea7'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '59a8514bb0ee5bae2689d8be717b5272c9b3dc1c'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '003ff459cdd85de551f4dcf95cdfeefe10f20531'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '5013810061a18ca1f5510106172b94c6fbd0a2fc'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '8fff3f074da9237cd4e179fd6dd89be6c4022d41'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'ba9a63be53f16b3b6e4043641c6bad4883e650b4'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '7b3b0c8327b3c0214ac49ca6d6922edbb81ab8c9'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '24cbb071689802fd6d3ff42198b19b125004c4e3'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc'
⚠ [38/2637] Ran proofwidgets:extraDep
warning: building from source; failed to fetch GitHub release (run with '-v' for details)
✖ [39/2637] Building proofwidgets/widgetJsAll
trace: .\.\.lake/packages\proofwidgets\widget> npm.cmd clean-install
trace: stderr:
node:internal/modules/cjs/loader:1228
  throw err;
  ^

Error: Cannot find module 'C:\ty\Polymorphisms\.lake\packages\proofwidgets\widget\node_modules\npm\bin\npm-prefix.js'
    at Function._resolveFilename (node:internal/modules/cjs/loader:1225:15)
    at Function._load (node:internal/modules/cjs/loader:1055:27)
    at TracingChannel.traceSync (node:diagnostics_channel:322:14)
    at wrapModuleLoad (node:internal/modules/cjs/loader:220:24)
    at Function.executeUserEntryPoint [as runMain] (node:internal/modules/run_main:170:5)
    at node:internal/main/run_main_module:36:49 {
  code: 'MODULE_NOT_FOUND',
  requireStack: []
}

Node.js v22.14.0
node:internal/modules/cjs/loader:1228
  throw err;
  ^

Error: Cannot find module 'C:\ty\Polymorphisms\.lake\packages\proofwidgets\widget\node_modules\npm\bin\npm-cli.js'
    at Function._resolveFilename (node:internal/modules/cjs/loader:1225:15)
    at Function._load (node:internal/modules/cjs/loader:1055:27)
    at TracingChannel.traceSync (node:diagnostics_channel:322:14)
    at wrapModuleLoad (node:internal/modules/cjs/loader:220:24)
    at Function.executeUserEntryPoint [as runMain] (node:internal/modules/run_main:170:5)
    at node:internal/main/run_main_module:36:49 {
  code: 'MODULE_NOT_FOUND',
  requireStack: []
}

Node.js v22.14.0
error: external command 'npm.cmd' exited with code 1
⣟ [706/2637] Running Mathlib.Algebra.Group.Units.Basic (+ 7 more)

I have also tried many variations of running lake clean, removing .lake, switching to different versions of mathlib and even after switching to mathlib with rev = "v4.16.0", and using lean-toolchain of 4.16.0, and removing .lake and lake-manifest.json it did not change.
And it should be noted as well, I disabled my anti-virus.

Also attaching the repo's lakefile.toml.
Any help will be greatly appriciated!

Link to the repo: https://github.com/YuvalFilmus/Polymorphisms/

[Jon Eugster]

did you run lake exe cache get at any point?

[Jon Eugster]

Indeed, the following seems to work fine on my machine:

git clone https://github.com/YuvalFilmus/Polymorphisms.git
cd Polymorphisms
lake exe cache get
lake build

Although, arguably for me even building from scratch works fine, so ... :man_shrugging: