Build Issue with Mathlib4

Stream: mathlib4

[Zhu]

Hi!
I've encountered a build issue while working on the Mathlib4 source code locally.

After pulling the latest version, I noticed that the VSCode Lean4 plugin reports a "build failed" error. The error message suggests it's related to npm and the module proofwidgets/widgetJsAll.

I'm running this on Windows and and I suspect this issue might be caused by the Windows environment. Also I noticed a similar issue discussed here, but I'm not quite clear the steps to resolve it.
Could anyone provide guidance on how to resolve this issue?

Thanks in advance for your help!

Here's the error message:

stderr:
✖ [399/1622] 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

1111.png

[Kim Morrison]

Sorry, as far as I understand, this is a bug in Lake, and we are waiting for @Mac Malone to decide how to fix it.

[Kim Morrison]

Have you tried deleting your .lake directory and trying again? That seems to be fixing the problem for others.

[Mac Malone]

@Kim Morrison We are? Oh, I had not realized that. My apologies! My understanding was the last development on my side in this issue was what I posted here. The cache corruption did not seem like something I coud fix. However, if the cache cloberring is currrently primary problem, I should be able to fix that in Lake by only fetching GitHub cloud releases if the build directory is missing.

[Zhu]

Kim Morrison said:

Sorry, as far as I understand, this is a bug in Lake, and we are waiting for Mac Malone to decide how to fix it.

I deleted the .lean directory and re-ran lake exe cache get, and the issue was resolved.
(Before that, I also ran git pull, which brought in a few new commits. I'm not sure if they're related to the issue.)

Anyway, thanks again for the help! :smiley:

[Kim Morrison]

Mac Malone said:

Kim Morrison We are? Oh, I had not realized that. My apologies! My understanding was the last development on my side in this issue was what I posted here. The cache corruption did not seem like something I coud fix. However, if the cache cloberring is currrently primary problem, I should be able to fix that in Lake by only fetching GitHub cloud releases if the build directory is missing.

@Mac Malone, I don't know where the problem is in between lake and cache, but it would be great if you could take ownership of the whole problem (namely, that users of Mathlib are regularly get errors from lake build, and told by lake that they need to do something with npm).

I'm happy to make changes to cache, and/or coordinate with owners of various repos to do things, but I think you, as lake owner, needs to be in the drivers seat here.

(More generally, I'm still really looking forward to cache being deprecated in favour of lake, and so I'm pretty inclined to suggest you take ownership of cache too, if only as a way of incentivizing you to make it obsolete. :-)

[Kim Morrison]

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

[Zhu]

image.png
It seems that the problem still exists :|

[Zhu]

But when I opened the folder in VSCode, it automatically started to recompile. I'm waiting for it to finish, hoping it will be successful. :octopus:

[Zhu]

It works :tada: