What happened to lake exe cache get

Stream: general

[Nick_adfor]

I have the following error:

C:\Users\xxx\.cache\mathlib\xxx.ltar: The requested operation cannot be performed on a file opened with user-mapped sections. (os error 1224)
uncaught exception:leantar failed with error code 1

[Nick_adfor]

Just yesterday I lake update and lake build and then it took more than 24h to import Mathlib in a new file... I must get cache or every time I would wait for 24h...

[Nick_adfor]

I do not know what happens now. But every time I start a new .lean file (Press Restart File) I will start from (1500/xxxx) to build the whole Mathlib.

[Nick_adfor]

I just import four:

import Mathlib.Algebra.Field.ZMod
import Mathlib.Algebra.Lie.OfAssociative
import Mathlib.Algebra.Order.Star.Basic
import Mathlib.Combinatorics.Nullstellensatz

But why Lean Infoview shows me

✔ [1269/1609] Built Mathlib.Data.Finset.NoncommProd (78s)

I mean that I never import Mathlib.Data

[Kim Morrison]

Have you tried deleting your .lake directory? What about your ~/.cache directory?

[Robin Arnez]

This might have to do with antivirus?

[Junyan Xu]

Make sure you stop the server before running lake exe cache get (for the os error 1224)
image.png

[Edward van de Meent]

image.png
note that there is also an option to straight-up update the cache

[Jireh Loreaux]

Nick_adfor said:

lib.Data.Finset.NoncommProd (78s)

I mean that I never import Mathlib.Data

Just FYI, I'm pretty sure that your imports transitively import Mathlib.Data.Finset.NoncommProd. Although having a working cache should still mean you don't have to build files.

[Nick_adfor]

I may paste my file here.

[Nick_adfor]

lake-manifest.json
lakefile.lean
lean-toolchain