ProofWidgets4

Stream: nightly-testing

[Kim Morrison]

@Wojciech Nawrocki I'm having trouble bumping ProofWidgets to v4.11.0-rc1 (and I think this will block me bumping Mathlib, as I don't dare have inconsistent Batteries imports...)

Could you (or anyone else who know more about npm!) please take a look at https://github.com/leanprover-community/ProofWidgets4/pull/73?

[Yakov Pechersky]

I think this issue is relevant https://github.com/nodejs/node/issues/52682

[Yakov Pechersky]

So I think adding a step to the workflow of npm i -g npm prior to the lake build step should work...?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Let's try it! (But how can we run npm i if npm isn't working?)

[Yakov Pechersky]

npm is working, that's the utility giving the error messages. But the build is looking for npm source js inside the widgets subfolder

[Yakov Pechersky]

Which I'm not sure why it'd be looking there to begin with. Perhaps if the global install doesn't fix it, then npm install npm might. npm install places the source code in the node_modules folder, which is what the build error is complaining about being missing.

[Yakov Pechersky]

I see, I think the error occurs during this line, right? https://github.com/leanprover-community/ProofWidgets4/blob/main/lakefile.lean#L99

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Attempting to install it globally failed with missing permissions, so I tried your local install suggestion. That seems to have worked. We should remove it when MSYS2 NPM is more recent and no longer has the issue.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I was a little worried that this step modifies package-lock.json which is then no longer considered up-to-date by Lake. Luckily we upload release archives from Ubuntu, and the npm install npm only runs on Windows. The whole setup is quite brittle.

[Yakov Pechersky]

npm install --no-save won't modify the lockfile