Error after updating mathlib

Stream: mathlib4

[Esteban Martínez Vañó]

Hi everyone.

I've updated mathlib in my project and now I get some errors with the imports.

If I create a new lean file and I start with, for example, import Mathlib.Topology.Instances.Real I get the following error:

c:\Users\Usuario\.elan\toolchains\leanprover--lean4---v4.15.0-rc1\bin\lake.exe setup-file C:/Users/Usuario/Desktop/Lean/Functional_Analysis/Topology/Nets/Test.lean Init Mathlib.Topology.Instances.Real` failed:

stderr:
✖ [406/1253] 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

The same happens with many more imports with almost identical errors but, for example, it doesn't give any error with import Mathlib.Order.Defs.LinearOrder

What is happening?

If any file is needed I'll upload it, sorry for not posting anything else, but I don't know what do you need.

[Ruben Van de Velde]

Search for npm on this zulip - you'll find a number of threads about it

[Kim Morrison]

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

[Esteban Martínez Vañó]

Kim Morrison ha dicho:

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

That's what I've seen after looking up for it. I solved it by deleting the whole folder and importing it again.