no interactiveExpr.js while build mathlib

Stream: new members

[Shanghe Chen]

Hi I am trying to build mathlib in my laptop inside WSL (just for kind of checking my laptop’s performance) I got the error:

[177/4314] Building Qq.Macro
[178/4314] Building Std.Data.Sum
[179/4314] Building Aesop.Util.EqualUpToIds
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/packages/importGraph/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/packages/proofwidgets/.lake/build/lib /home/riv/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/bin/lean ./.lake/packages/proofwidgets/././ProofWidgets/Component/Basic.lean -R ./.lake/packages/proofwidgets/./. -o ./.lake/packages/proofwidgets/.lake/build/lib/ProofWidgets/Component/Basic.olean -i ./.lake/packages/proofwidgets/.lake/build/lib/ProofWidgets/Component/Basic.ilean -c ./.lake/packages/proofwidgets/.lake/build/ir/ProofWidgets/Component/Basic.c
error: stdout:
./.lake/packages/proofwidgets/././ProofWidgets/Component/Basic.lean:73:16: error: no such file or directory (error code: 2)
  file: ./.lake/packages/proofwidgets/././ProofWidgets/Component/../../.lake/build/js/interactiveExpr.js
./.lake/packages/proofwidgets/././ProofWidgets/Component/Basic.lean:71:2: error: cannot evaluate code because 'ProofWidgets.InteractiveExpr' uses 'sorry' and/or contains errors
error: external command `/home/riv/.elan/toolchains/leanprover--lean4---v4.7.0-rc2/bin/lean` exited with code 1
[179/4314] Building Mathlib.Tactic.Explode.Pretty
[180/4314] Building Std.Data.RBMap.Basic
[181/4314] Building Std.Lean.Util.EnvSearch
[182/4314] Building Mathlib.Tactic.Replace
[183/4314] Building Mathlib.Tactic.Monotonicity.Basic
[184/4314] Building Mathlib.Tactic.SwapVar

[Shanghe Chen]

anyone got similar error too?

[Shanghe Chen]

cd into proofwidgets and do lake update std and then rebuild again it works now:tada: