Build errors at a specific version of mathlib and toolchain

Stream: new members

[Ryan Smith]

I'm trying to get Aristotle to run in order to try it out. It requires two things: mathlib version d62eab0cc36ea522904895389c301cf8d844fd69 and lean toolchain version leanprover/lean4:v4.20.0-rc5. Git checkout gives us the correct mathlib version, and the lean-toolchain file shows leanprover/lean4:v4.20.0-rc5 so that part looks good. Opening a file in vscode produces

`/Users/bixbyr/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/bin/lake setup-file /Users/bixbyr/mathlib4/Mathlib/GroupTheory/Fitting.lean Init Mathlib Mathlib.GroupTheory.Nilpotent` failed:

stderr:
warning: proofwidgets: repository '/Users/bixbyr/mathlib4/.lake/packages/proofwidgets' has local changes
✖ [575/803] Building proofwidgets/widgetJsAll
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.
Some required builds logged failures:
- proofwidgets/widgetJsAll
error: build failed

So we run lake exe cache get and it says

warning: proofwidgets: repository '/Users/bixbyr/mathlib4/.lake/packages/proofwidgets' has local changes
Warning: recommended `curl` version ≥7.81. Found 7.78.0
warning: proofwidgets: repository '/Users/bixbyr/mathlib4/.lake/packages/proofwidgets' has local changes
No files to download
Decompressing 6663 file(s)
Unpacked in 351 ms
Completed successfully!

Reloading everything in vscode brings us back to where we started. I tried git reset --hard but it seems like the issue might be out of date untracked files? Is the .lake directory something which can be deleted and will be re downloaded automatically?

[Ryan Smith]

In my defense, it does say to ask on Zulip if that didn't fix the issue :)

[Ruben Van de Velde]

Yes, you can delete .lake/ and run lake exe cache get again