Issue with ProofWidgets on build

Stream: mathlib4

[Tyler]

On building a lean project, I get error: ProofWidgets not up-to-date. Please run lake exe cache get to fetch the latest ProofWidgets. If this does not work, report your issue on the Lean Zulip.

I have ran lake exe cache get but this does not fix the issue. I am using the master branch of mathlib.

[Kevin Buzzard]

Can you post your lakefile.toml or lakefile.lean? This issue should have been sorted out a while ago.

[Tyler]

I have it as follows:

name = "test"
version = "0.1.0"
defaultTargets = ["test"]

[[lean_lib]]
name = "Test"

[[lean_exe]]
name = "test"
root = "Main"

[[require]]
name = "mathlib"
scope = "leanprover-community"
branch = "master"

[Tyler]

This is still the same when swapping branch for

rev = "v4.15.0-rc1"

[Tyler]

The error on lake update is as follows:

info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '2b000e02d50394af68cfb4770a291113d94801b5'
error: C:\Users\roche\Documents\dissertation\.lake\packages\proofwidgets\lakefile.lean:28:63: Function expected at
  BuildJob
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  (Array FilePath)
error: C:\Users\roche\Documents\dissertation\.lake\packages\proofwidgets\lakefile.lean:40:13: Invalid field notation: Type is not of the form `C ...` where C is a constant
  BuildJob
has type
  x✝
error: C:\Users\roche\Documents\dissertation\.lake\packages\proofwidgets\lakefile.lean:46:29: Invalid field notation: Type of
  deps
is not known; cannot resolve field `bindSync`
warning: C:\Users\roche\Documents\dissertation\.lake\packages\proofwidgets\lakefile.lean:77:7: declaration uses 'sorry'
warning: C:\Users\roche\Documents\dissertation\.lake\packages\proofwidgets\lakefile.lean:80:7: declaration uses 'sorry'
error: C:\Users\roche\Documents\dissertation\.lake\packages\proofwidgets\lakefile.lean: package configuration has errors

With leanprover/lean4:v4.25.0-rc1 (default)

[Tyler]

The issue seems to only be on Windows, I have tried the same on my Linux machine (which uses the same version of lean) and it works.

Any help (Windows specific) would be much appreciated

[Kevin Buzzard]

You can't be on mathlib master and Lean (some random version which isn't the same as mathlib master) I don't think. If you want today's mathlib then lake update mathlib and don't pin your lean version. Mathlib master is currently on v4.26.0rc2.

[Tyler]

I have found the issue, ProofWidgets uses some webserver internally, because of this, Node/Npm has to be installed. This solves the problem

[Kevin Buzzard]

Nice!

[Kim Morrison]

No, @Tyler building projects with ProofWidgets should not (and does not for most people!) require having npm installed. You are still doing something wrong! It looks to me from the above like you are just on some random toolchain unrelated to the commit of Mathlib master you are using.

[Ruben Van de Velde]

Do you have an elan override set up?