Warning: some files were not found in the cache.

Stream: mathlib4

[Kevin Buzzard]

This is now happening to me consistently, and it doesn't seem to matter but I thought I'd report it anyway. Note that lake exe cache get! doesn't fix the problem.

buzzard@buster:~/lean-projects/mathlib4$ lake exe cache get!
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [6/9] Compiling Cache.Requests
info: [9/9] Linking cache
Attempting to download 3552 file(s)
Downloaded: 3551 file(s) [attempted 3552/3552 = 100%] (99% 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 3551 file(s)
buzzard@buster:~/lean-projects/mathlib4$ lake build
[1886/3569] Building Mathlib.LinearAlgebra.Basic
buzzard@buster:~/lean-projects/mathlib4$ git status
On branch master
Your branch is up-to-date with 'origin/master'.

Untracked files:
  (use "git add <file>..." to include in what will be committed)
    alg_geom_notes.txt
    alg_geom_notes.txt~
    crap
    universe_dagur.txt

nothing added to commit but untracked files present (use "git add" to track)
buzzard@buster:~/lean-projects/mathlib4$

[Sebastien Gouezel]

If I understand correctly, this happens when some file did not compile correctly in your branch (and then of course it's not in the cache). The error message is quite misleading then.

[Kevin Buzzard]

This is on master

[Mauricio Collares]

At least here, the cache miss is https://lakecache.blob.core.windows.net/mathlib4/f/11451517259001675684.tar.gz, corresponding to Util/TacticCaches.lean. I can't explain the Mathlib.LinearAlgebra.Basic (re)build.

[Mauricio Collares]

I guess the cause is that lake build TacticCaches creates build/{ir,lib}/TacticCaches.* and not build/{ir,lib}/Util/TacticCaches.* for some reason.

[Scott Morrison]

Ugh, my fault. :-)

[Scott Morrison]

Hmm, actually maybe not entirely my fault.

[Scott Morrison]

@Mac (or anyone interested in lakefile details), when we run lake exe cache in Mathlib master at the moment, the following weird thing happens:

• build/ir/Util/Cache/Main.c is created (along with the corresponding .o and .o.trace
• build/ir/Cache/Hashing.c is created (along with IO.c and Requests.c, and their .o and .o.traces)

however Main/Hashing/IO/Requests all live in the same directory, and the intent was certainly that their build artifacts all live at the same location.

How can we achieve this?

[Scott Morrison]

For reference, the relevant section of the lakefile is:

lean_lib Cache where
  moreLeanArgs := moreLeanArgs
  roots := #[`Cache]
  srcDir := "Util"

lean_exe cache where
  root := `Util.Cache.Main

[Scott Morrison]

I suspect the problem is in the root := `Util.Cache.Main line. I had originally wanted to write root := `Cache.Main here, on the principle that this was a module name rather than a filename-mysteriously-written-as-a-Name.

However with this change lake exe cache fails with:

% lake exe cache
error: no such file or directory (error code: 2)
  file: ./././Cache/Main.lean

[Scott Morrison]

Separately from the above question, hopefully #5824 will fix Kevin's observed problem above, but still needs testing after CI.

[Mario Carneiro]

yeah I think this setup is wrong, and the cache change was not ready to be merged and we should probably back it out

[Mario Carneiro]

The issue is that cache is using a half-baked version of the source path lookup implemented in getPackageDirs, and this was not updated for the Util folder

[Mario Carneiro]

You should be using root := `Cache.Main for the lake_exe line, but with a srcDir of "Util"

[Mario Carneiro]

Util is not a module name and should not appear in such, it is just a folder

[Mario Carneiro]

Oh, there is a lake issue here after all: there is no srcDir for lean_exe targets @Mac

[Mario Carneiro]

There is a function LeanExeConfig.toLeanLibConfig in lake for converting an exe config into a lib config, but it sets a lot of things to default values and that seems like a bit of missing config

[Mario Carneiro]

I suggest just reverting the Util change for now, I don't think we can quick fix this

[Scott Morrison]

#5825 is the revert PR.

[Mac Malone]

Mario Carneiro said:

Oh, there is a lake issue here after all: there is no srcDir for lean_exe targets Mac

I think my original rationale was that it would not matter whether the srcDir was part of the module name since a main file should not be imported and the finer details of the build layout should not be a user's concern.

But, for consistency's sake, better aligning the lean_exe / lean_lib configuration options seems like a good idea!

I am currently at a conference, so I will not be able to code this myself until I get back. However, if someone wants to PR a fix beforehand, I can review and merge it.