need to run lake exe cache twice to get cache

Stream: mathlib4

[Kevin Buzzard]

Is this related to the fact that I can never get cache for #30989 ? I always get some spurious error "This usually means that your local checkout of mathlib4 has diverged from upstream." and then have to build 1500 files manually.

[Bryan Gin-ge Chen]

Oh wow, I don't know if it's related to the sporadic errors in CI but something weird is going on there.

I was able to get the cache but I had to run lake exe cache get twice (once to grab files from the default cache for leanprover-community/mathlib4 and once with --repo=kckennylau/mathlib4 like our CI does:

gh pr checkout 30989
lake exe cache get # this gets 6055 files and complains about missing files
lake exe cache --repo=kckennylau/mathlib4 get # this gets the remaining 1386 files
lake build # this is fast

If I try getting lake exe cache --repo=kckennylau/mathlib4 get first then it only gets 1386 files and complains about missing files, and I have to run lake exe cache get after that for lake build to be fast again.

I remember that after we switched to forks, we just had to switch to running lake exe cache --repo=name-of-fork/mathlib4 get for the cache to work properly, but now it looks like the required files can end up being split across the caches for two repos instead of being available just from one.

@Matthew Ballard I seem to recall that you worked on / looked at this part of cache around when we switched to forks? Is this intended?

[Damiano Testa]

I'm not at a computer now, but when I run lake exe cache get there are usually two phases, one where it downloads files from master and one where it uses the branch. I don't have to do anything special for that, though.

[Bryan Gin-ge Chen]

Odd, it doesn't seem to work for me for that branch. I just tested again. First I cleared all caches:

rm -rf .lake
rm -rf ~/.cache/mathlib

Here's the output of lake exe cache get and lake build --no-build afterwards, showing that only one repo is tried:

> lake exe cache get
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '8864a73bf79aad549e34eff972c606343935106d'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '2ed4ba69b6127de8f5c2af83cccacd3c988b06bf'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '451499ea6e97cee4c8979b507a9af5581a849161'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'fb8ed0a85a96e3176f6e94b20d413ea72d92576d'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '1fa48c6a63b4c4cda28be61e1037192776e77ac0'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '95c2f8afe09d9e49d3cacca667261da04f7f93f7'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '43f271c492f815dbbb9a4b753d6ccc9d19b5609a'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '72ae7004d9f0ddb422aec5378204fdd7828c5672'
installing leantar 0.1.16
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
100  884k  100  884k    0     0  2513k      0 --:--:-- --:--:-- --:--:-- 2513k

Fetching ProofWidgets cloud release... done!
Current branch: teichmuller-cdvr
Using cache (Azure) from upstream: leanprover-community/mathlib4
Attempting to download 7441 file(s) from leanprover-community/mathlib4 cache
Downloaded: 6055 file(s) [attempted 7441/7441 = 100%, 212 KB/s]
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.
Alternatively, if you already have pushed your commits to a branch, this may mean the CI build has failed part-way through building.
Decompressing 6055 file(s)
Unpacked in 6901 ms
Completed successfully!
> lake build --no-build
✖ [1636/2915] Building Mathlib.Algebra.CharP.Lemmas
error: target is out-of-date and needs to be rebuilt
✖ [2825/2915] Building Mathlib.Algebra.CharP.Quotient
error: target is out-of-date and needs to be rebuilt
✖ [3172/4152] Building Mathlib.LinearAlgebra.SModEq.Basic
error: target is out-of-date and needs to be rebuilt
Some required targets logged failures:
- Mathlib.Algebra.CharP.Lemmas
- Mathlib.Algebra.CharP.Quotient
- Mathlib.LinearAlgebra.SModEq.Basic

It looks like master was merged into that branch fairly recently so there shouldn't be a difference in Cache versions?

[Matthew Ballard]

Bryan Gin-ge Chen said:

Matthew Ballard I seem to recall that you worked on / looked at this part of cache around when we switched to forks? Is this intended?

The assumptions made about git states in the logic are bad. We need to identify the use cases we care about and then write behavior tests to assure things work as expected.

[Notification Bot]

5 messages were moved here from #mathlib4 > "verify that everything was available in the cache" fails CI by Bryan Gin-ge Chen.