strange failure

Stream: mathlib4

[Edward van de Meent]

in my local clone of mathlib, trying to get the build cache of master gives an error...
This happens regardless of if i do it via the VSCode extension or manually:

• manually:

$ lake exe cache get
info: proofwidgets: checking out revision '6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294'
error: external command 'git' exited with code 1

• via extension:

lake serve -- c:\Users\edege\OneDrive\Documenten\Lean\mathlib4
info: proofwidgets: checking out revision '6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294'
error: external command 'git' exited with code 1
warning: package configuration has errors, falling back to plain `lean --server`

[Edward van de Meent]

when looking in the infoview, i see the following message:

`c:\Users\edege\.elan\toolchains\leanprover--lean4---v4.28.0-rc1\bin\lake.exe setup-file C:/Users/edege/OneDrive/Documenten/Lean/mathlib4/Mathlib/CategoryTheory/Subobject/Lattice.lean - --no-build --no-cache` failed:

stderr:
trace: C:\Users\edege\OneDrive\Documenten\Lean\mathlib4\.lake/packages\proofwidgets> git fetch --tags --force origin
info: proofwidgets: checking out revision '6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294'
trace: C:\Users\edege\OneDrive\Documenten\Lean\mathlib4\.lake/packages\proofwidgets> git checkout --detach 6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294 --
trace: stderr:
error: Your local changes to the following files would be overwritten by checkout:
    widget/package-lock.json.hash
Please commit your changes or stash them before you switch branches.
Aborting
error: external command 'git' exited with code 1
Failed to configure the Lake workspace. Please restart the server after fixing the error above.

However, VSCode shows me no changes, staged or unstaged?

[Ruben Van de Velde]

There is a change in a git repository that is nested under your git repository, in an ignored folder. So you need to navigate to .lake/packages/proofwidgets and run git there to see the changes

[Edward van de Meent]

it seems to be working now, thanks!