lake exe cache get: "Warning: some files were not found ..."

Stream: new members

[mars0i]

What does this warning mean? I am not hacking mathlib4 as far as I know, nor any other library.

~/docs/src/LeanProver/LearnLean(main)*$ lake exe cache get
info: downloading component 'lean'
Total: 223.9 MiB Speed: 47.7 MiB/s
info: installing component 'lean'
Attempting to download 3610 file(s)
Downloaded: 0 file(s) [attempted 3610/3610 = 100%] (0% success)
Warning: some files were not found in the cache.
This usually means that your local checkout of mathlib4 has diverged from upstream.
If you push your commits to a branch of the mathlib4 repository, CI will build the oleans and they will be available later.
Decompressing 1580 file(s)
Unpacked in 196 ms
Completed successfully!

(Searching on "Warning: some files were not in the cache", I found a suggestion for a different context to run elan toolchain uninstall $(<lean-toolchain), but that didn't change the warning.)

[Ruben Van de Velde]

What does your lakefile.lean/toml look like?

[mars0i]

Thanks @Ruben Van de Velde. I don't know about toml files, but I assume you mean that I could either have a lakefile.lean or a lakefile.toml. Here's the lakefile.lean:

import Lake
open Lake DSL

require mathlib from git
  "https://github.com/leanprover-community/mathlib4"

require batteries from git
  "https://github.com/leanprover-community/batteries" @ "main"

package «LearnLean» where
  -- add package configuration options here

lean_lib «LearnLean» where
  -- add library configuration options here

@[default_target]
lean_exe «learnlean» where
  root := `Main

I should mention that at the moment I'm not using mathlib or batteries, so I could take those lines out. I have used them for some experiments.

[Ruben Van de Velde]

Yes, you might drop mathlib and batteries there. lake exe cache get only works for mathlib anyway

[mars0i]

Thanks @Ruben Van de Velde. OK, trying that.

(The underlying problem I'm trying to solve is that sometimes I change something in a file I'm working on, and Lean gets stuck in "Processing file ..." even though I'm not loading libraries, and even though other changes didn't have this effect. If I restart my editor, everything's fine with the saved file--so it's not that my code broke Lean. :smile: That's what I was trying to solve by reinitializing Lean, the libraries, etc. I haven't asked about it here because I couldn't identify the conditions under which Lean went off into space. I'll be curious as to whether this change makes that problem go away.)