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.

[Yaël Dillies]

Mario Carneiro said:

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

Is #8361 going to cause a problem, then?

[Mario Carneiro]

I think cache doesn't care about mathlib's utils, the only reason the above was a problem was because it was used for the TacticCaches folder which is distributed via cache. The utils are normally compiled on the spot by lake, so we can use any method for specifying the exes that lake accepts

[Mario Carneiro]

that said I think #8361 made the same mistake I highlighted above: it should be using a srcDir instead of a longer module path for identifying the Utils folder

[Mario Carneiro]

I haven't checked if lake has since been fixed to allow srcDir on lean_exe

[Mario Carneiro]

it has

[Yaël Dillies]

Regardless of whether it would cause a cache problem, do you think LongestPole should create a new Util/Utils folder or use the existing MathlibExtras ?

[Mario Carneiro]

I think it should be in the same directory as shake, cache, checkYaml exes

[Mario Carneiro]

MathlibExtras is a library, it's a bit different

[Mario Carneiro]

(it's also now nonexistent, if I've been following the news correctly)

[Yaël Dillies]

Mario Carneiro said:

I think it should be in the same directory as shake, cache, checkYaml exes

... which is partly https://github.com/leanprover/std4/tree/main/Std/Util but not completely?

[Mario Carneiro]

??

[Mario Carneiro]

We're talking about mathlib here, not std

[Mario Carneiro]

shake, cache, checkYaml are utility programs provided by the mathlib project

[Yaël Dillies]

Uh wait we have Cache in both mathllib and Std?!

[Mario Carneiro]

there is no cache in std

[Mario Carneiro]

mathlib's cache also caches all of mathlib's dependencies

[Yaël Dillies]

Oh I thought Cache had been upstreamed since we've talked about it for so long

[Mario Carneiro]

if you are not using std via mathlib, you are currently compiling it from source

[Yaël Dillies]

but I see https://github.com/leanprover/std4/blob/main/Std/Util/Cache.lean is something different

[Mario Carneiro]

yes, that's the thing that generates the exact? cache in MathlibExtras

[Mario Carneiro]

which no longer exists

[Yaël Dillies]

Okay so we have a lot of dead code, and no Util-like directory anymore

[Yaël Dillies]

Hence we might as well have a LongestPole library?

[Mario Carneiro]

it's not a library though IIUC

[Mario Carneiro]

it's an exe

[Mario Carneiro]

which is why I grouped it with the other mathlib exes

[Mario Carneiro]

but I do agree that all the exes should live in a subfolder, maybe scripts/

[Mario Carneiro]

(I also think sources should live in src/ but I'm not sure I'll live to see that day)

[Yaël Dillies]

I see scripts as the "collection of all non-Lean exes", but maybe that could change

[Mario Carneiro]

If lean scripts require no additional infrastructure beyond a single file and a line in the lakefile, I think they could reasonably live in a scripts folder along non-lean exes

[Mario Carneiro]

and for the ones that require a subfolder, I think that's fine too

[Yaël Dillies]

Okay, should I make a PR then?