Cache acting weird

Stream: general

[Andrew Yang]

For the past few days cache had some weird behaviors that I have never seen before. I thought it was a transient issue on my local machine but yesterday at Xena there were several people hitting this issue. The error messages comes in several flavours but here is one

failed to read file '/Users/erd1/Desktop/lean/mathlib4/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Classes/Cast.olean', incompatible header

I assume this means the cache is out of date but restarting the file nor the server works. Sometimes lake build fixes this but sometimes you need to lake clean.

This usually happens when opening a new file or importing a new file that has no cache but it is very unreproducible. I wonder if there are other people facing this that knows better about what is going on?

[Kevin Buzzard]

I did rm -rf .lake in FLT for the first time in a very long time today after getting cache looked like it worked but lake build started to build the second half of mathlib instead of FLT. Nuking .lake fixed it. Also someone just starting to help with FLT DMed me on Tuesday or so with a weird cache error complaining about proofwidgets and I commented that usually nowadays we didn't have to rm -rf .lake but I didn't understand his error so he should try it. It also fixed his problems.

[Yaël Dillies]

It sounds like you simply corrupted your cache by partially rebuilding it

[Andrew Yang]

But usually restarting file will solve this.

[Yaël Dillies]

No, restarting a file never solved a corrupted cache for me

[Yaël Dillies]

Corrupting is quite rare IME. It might be the first time it happens to you?

[Andrew Yang]

Then maybe we are not talking the same corrputed cache.
Currently if I open two fresh new file and try to import one from the other I get

object file '/Users/erd1/Desktop/lean/mathlib4/.lake/build/lib/lean/Mathlib/NumberTheory/NumberField/Foo.olean' of module Mathlib.NumberTheory.NumberField.Foo does not exist

And the only way to solve it is to run lake build a few times.

[Yaël Dillies]

Ah! That's a different error from the one you mentioned in your original post

[Eric Wieser]

I get corruptions pretty often if I switch branch with an editor open

[Andrew Yang]

Yeah I said "The error messages comes in several flavours" and that one in the OP is the one I happen to see when I started this thread. But probably as you said they are different things.

[Andrew Yang]

I got a new variant again

`/Users/erd1/.elan/toolchains/leanprover--lean4---v4.20.0-rc5/bin/lake setup-file /Users/erd1/Desktop/lean/mathlib4/Mathlib/NumberTheory/NumberField/Representation/Basic.lean Init Mathlib Mathlib.NumberTheory.NumberField.Representation.Lemmas --no-build --no-cache` failed:

stderr:
✖ [6752/6753] Running Mathlib.NumberTheory.NumberField.Lemmas
error: no such file or directory (error code: 2)
  file: /Users/erd1/Desktop/lean/mathlib4/Mathlib/NumberTheory/NumberField/Lemmas.lean
✖ [6753/6753] Running setup (Mathlib.NumberTheory.NumberField.Representation.Basic)
error: /Users/erd1/Desktop/lean/mathlib4/Mathlib/NumberTheory/NumberField/Representation/Basic.lean: bad import 'Mathlib.NumberTheory.NumberField.Lemmas'
Some required builds logged failures:
- Mathlib.NumberTheory.NumberField.Lemmas
- setup (Mathlib.NumberTheory.NumberField.Representation.Basic)
error: build failed

which was still fixed by a lake build but not via restart file.