error after updating Mathlib

Stream: lean4

[Floris van Doorn]

I have experienced this twice in the last week: I move to a new version of Mathlib, get the cache, I open a file somewhere in the import hierarchy and I have to rebuild the file. During the rebuild, I get an error in proofwidgets.

Last time I deleted by .lake file and that solved the issues, but since it is a recurring problem, here is the error I get.

I am on the current Mathlib bbaf1a0ef4e have gotten the cache (lake env lean Mathlib.lean succeeds) and then open Mathlib.Topology.Basic. I get the message that I have to rebuild imports, and upon doing that I get the following error.

`c:\Users\Floris\.elan\toolchains\leanprover--lean4---v4.15.0-rc1\bin\lake.exe setup-file C:/Users/Floris/projects/mathlib/Mathlib/Topology/Basic.lean Init Mathlib.Order.Filter.Lift Mathlib.Topology.Defs.Filter Mathlib.Topology.Defs.Basic Mathlib.Data.Set.Lattice Mathlib.Order.Filter.AtTopBot` failed:

stderr:
✖ [519/648] 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:\Users\Floris\projects\mathlib\.lake\packages\proofwidgets\widget\node_modules\npm\bin\npm-prefix.js'
    at Module._resolveFilename (node:internal/modules/cjs/loader:1225:15)
    at Module._load (node:internal/modules/cjs/loader:1051:27)
    at Function.executeUserEntryPoint [as runMain] (node:internal/modules/run_main:174:12)
    at node:internal/main/run_main_module:28:49 {
  code: 'MODULE_NOT_FOUND',
  requireStack: []
}

Node.js v20.17.0
node:internal/modules/cjs/loader:1228
  throw err;
  ^

Error: Cannot find module 'c:\Users\Floris\projects\mathlib\.lake\packages\proofwidgets\widget\node_modules\npm\bin\npm-cli.js'
    at Module._resolveFilename (node:internal/modules/cjs/loader:1225:15)
    at Module._load (node:internal/modules/cjs/loader:1051:27)
    at Function.executeUserEntryPoint [as runMain] (node:internal/modules/run_main:174:12)
    at node:internal/main/run_main_module:28:49 {
  code: 'MODULE_NOT_FOUND',
  requireStack: []
}

Node.js v20.17.0
error: external command 'npm.cmd' exited with code 1
Some required builds logged failures:
- proofwidgets/widgetJsAll
error: build failed

After opening these files, running lake build from the command line also gives this error.

[Floris van Doorn]

(this is on Windows)

[Ruben Van de Velde]

I think the conclusion was that local builds should never try to run npm

[Ruben Van de Velde]

And the reason they sometimes try to is related to lake caching conflicting with lake exe cache (?) or your local network connection (?)

[Floris van Doorn]

This happens when I open a file in Mathlib, while having a cache that seems to work on the command line.

[Sébastien Gouëzel]

This happened to me several times this week when updating a branch to last mathlib version. Also on windows, working network connection. I solved it each time by deleting .lake, as you did.

[Kim Morrison]

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

[Floris van Doorn]

I think it's indeed fixed now.

[Weihang Xu]

@Floris van Doorn I've run into exactly the same error. So do I need to Update my Mathlib to the latest version (Right now I'm using v4.13.0)? Thanks. :blush:

[Ruben Van de Velde]

Try removing .lake and getting the cache again first

[Weihang Xu]

Thank you for your suggestion! Now I'm building the latest mathlib4 project directly using leanprover/lean4:v4.15.0-rc1, instead of importing Mathlib as a package, the issue doesn't occur anymore. :frowning: