Untracked working tree files

Stream: Polynomial Freiman-Ruzsa conjecture

[Terence Tao]

After some hiatus, I tried to open the Lean server on this project and got this error message:

`c:\Users\teort\.elan\toolchains\leanprover--lean4---v4.19.0-rc3\bin\lake.exe setup-file C:/Users/teort/Dropbox/Lean/pfr/PFR/ApproxHomPFR.lean Init Mathlib.Combinatorics.Additive.Energy Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.InnerProductSpace.PiL2 LeanAPAP.Extras.BSG PFR.HomPFR PFR.RhoFunctional` failed:

stderr:
trace: .\.\.lake/packages\mathlib> git fetch --tags --force origin
trace: stderr:
From https://github.com/leanprover-community/mathlib4
 * [new branch]              AffineLocalToPretop -> origin/AffineLocalToPretop
info: mathlib: checking out revision '6939380346f358d4da9bde8b3fbba195c3a9d014'
trace: .\.\.lake/packages\mathlib> git checkout --detach 6939380346f358d4da9bde8b3fbba195c3a9d014 --
trace: stderr:
error: The following untracked working tree files would be overwritten by checkout:
    Mathlib/Data/Int/Basic.lean
    Mathlib/Data/Nat/Basic.lean
Please move or remove 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.

Is this something to do with the upstreaming to Mathlib? What is the fix?

EDIT: AI is telling me to try git clean -fd, git checkout, lake update, and lake build. Still ongoing, but looks like it is fixing the problem...

SECOND EDIT: Okay, it worked. There was one error message during lake update (uncaught exception: Failed to prune ProofWidgets cloud release: permission denied (error code: 13)
file: .lake\packages\proofwidgets\.lake\build\lib\lean\ProofWidgets\Component
error: mathlib: failed to fetch cache) that blocked automatic fetching of the cache, but this seems to have been some local issue, as lake exe cache get later worked.

[Moritz Firsching]

Perhaps some unintended edit to files in .lake/packages/mathlib happened?
You can check with

cd .lake/packages/mathlib/
git status

This should return

[...]
nothing to commit, working tree clean

If it doesn't perhaps it would be a good idea to just rm -rf .lake?

[Terence Tao]

Yeah, I get a clean working tree now. According to an AI, it was possibly a Dropbox issue. (I really should move my Lean folders outside of Dropbox...)

[Kevin Buzzard]

Yeah I did this after various random errors. I think one way of thinking about it is that git and dropbox are both trying to do similar jobs but in different ways, so they may confuse each other.

[Shreyas Srinivas]

You shouldn’t put folders containing builds into Dropbox anyway

[Yury G. Kudryashov]

Does dropbox support ignoring files&subfolders? If yes, then you should .git, *.olean, and .lake.

[Shreyas Srinivas]

Currently the only way to do that is manually right click and ask Dropbox to ignore each folder.

[Eric Wieser]

Ignoring .git in dropbox sounds like a recipe for disaster when using multiple devices

[Yury G. Kudryashov]

Probably, you're right.