Issues with cache

Stream: Polynomial Freiman-Ruzsa conjecture

[Paul Lezeau]

Hi all! When working on this project, I've kept running into issues with cache files, which tends to be rather annoying since the only workaround I've found is to delete everything and build manually, and even this doesn't work systematically.

I usually work on a fork, which I create by using the Lean "Download Project" tool on VS code, and run lake exe cache get. This seems to have issues with getting the cache for certain files (e.g. whenever I open ruzsa_distance.lean, Lean tells me that the imports of that file are out of date and I end up having to recompile most of those manually). Is there something I am doing wrong here?

I've also noticed that things seem to get even worse when I try to do git manipulations. For instance yesterday I ran git merge https://github.com/teorth/pfr on my fork to get the upstream changes, and for some reason Lean then wanted to recompile most of Mathlib.

[Yaël Dillies]

Instead of clicking Rebuild imports, you should run lake exe cache get. The fact that you have a choice here is why rebuilding is not automatic anymore.

[Yaël Dillies]

... or well that can also mean you changed one upstream file, in which case Rebuild imports will only rebuild that one file.

[Paul Lezeau]

Ok fair enough. I just ran that, and the output I got was

Attempting to download 9 file(s)
Downloaded: 0 file(s) [attempted 9/9 = 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 3922 file(s)
unpacked in 72 ms

[Yaël Dillies]

Yep, that's completely expected. We're not caching PFR.

[Paul Lezeau]

Right ok that makes sense! I thought this was a problem with my installation so I was desperately trying to figure out what was going on

[Paul Lezeau]

I restarted the Lean server on the same file ruzsa_distance.lean after following what you said, and this is what I got

`c:\Users\paull\.elan\toolchains\leanprover--lean4---v4.3.0-rc2\bin\lake.exe print-paths Init Mathlib.Probability.Notation Mathlib.Probability.ConditionalProbability Mathlib.Probability.IdentDistrib PFR.Entropy.KernelRuzsa PFR.entropy_basic PFR.ForMathlib.FiniteMeasureComponent PFR.f2_vec` failed:

stderr:
info: [623/1985] Building ProofWidgets.Compat
info: [1502/1985] Building PFR.ForMathlib.Jensen
info: [1771/1985] Building PFR.ForMathlib.Finiteness
info: [1953/1985] Building PFR.ForMathlib.Miscellaneous
info: [1953/1985] Building PFR.ForMathlib.Independence
error: >
LEAN_PATH=.\.lake/packages\std\.lake\build\lib;.\.lake/packages\Qq\.lake\build\lib;.\.lake/packages\aesop\.lake\build\lib;.\.lake/packages\Cli\.lake\build\lib;.\.lake/packages\proofwidgets\build\lib;.\.lake/packages\mathlib\.lake\build\lib;.\.lake\build\lib PATH c:\Users\paull\.elan\toolchains\leanprover--lean4---v4.3.0-rc2\bin\lean.exe .\.lake/packages\proofwidgets\.\.\ProofWidgets\Compat.lean -R .\.lake/packages\proofwidgets\.\. -o .\.lake/packages\proofwidgets\build\lib\ProofWidgets\Compat.olean -i .\.lake/packages\proofwidgets\build\lib\ProofWidgets\Compat.ilean -c .\.lake/packages\proofwidgets\build\ir\ProofWidgets\Compat.c
error: stdout:
.\.lake/packages\proofwidgets\.\.\ProofWidgets\Compat.lean:174:16: error: no such file or directory (error code: 2)
file: .\.lake/packages\proofwidgets\.\.\ProofWidgets\..\build\js\compat.js
.\.lake/packages\proofwidgets\.\.\ProofWidgets\Compat.lean:170:2: error: cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains errors
error: external command `c:\Users\paull\.elan\toolchains\leanprover--lean4---v4.3.0-rc2\bin\lean.exe` exited with code 1
info: [1954/1985] Building PFR.MeasureReal
info: [1958/1985] Building PFR.neg_xlogx
info: [1959/1985] Building PFR.Entropy.Measure
info: [1960/1985] Building PFR.Entropy.MeasureCompProd
info: [1961/1985] Building PFR.Entropy.Disintegration
info: [1962/1985] Building PFR.Entropy.Kernel
info: [1963/1985] Building PFR.Entropy.KernelMutualInformation
info: [1964/1985] Building PFR.Entropy.Group
info: [1964/1985] Building PFR.entropy_basic
info: [1965/1985] Building PFR.Entropy.KernelRuzsa
info: stdout:
.\.\.\PFR\entropy_basic.lean:157:6: warning: declaration uses 'sorry'
.\.\.\PFR\entropy_basic.lean:162:6: warning: declaration uses 'sorry'
.\.\.\PFR\entropy_basic.lean:224:6: warning: declaration uses 'sorry'
.\.\.\PFR\entropy_basic.lean:243:6: warning: declaration uses 'sorry'
.\.\.\PFR\entropy_basic.lean:741:4: warning: declaration uses 'sorry'
.\.\.\PFR\entropy_basic.lean:744:6: warning: declaration uses 'sorry'
.\.\.\PFR\entropy_basic.lean:961:6: warning: declaration uses 'sorry'
info: stdout:
.\.\.\PFR\Entropy\KernelRuzsa.lean:214:6: warning: declaration uses 'sorry'

[Paul Lezeau]

This was at the top of the file, with a bunch of red everywhere :(

[Yaël Dillies]

The latter messages are expected. The ones about ProofWidgets not so much (but it might not be our fault because there's a caching problem right for ProofWidgets).

[Paul Lezeau]

Right ok. So this possibly is a problem with my installation?

[Yaël Dillies]

I can't reproduce, so yes maybe.

[Yaël Dillies]

Try wiping .lake entirely and rerun lake exe cache get.

[Paul Lezeau]

Ok this seems to work now, thanks a lot for the help!

[Paul Lezeau]

I'm not sure how exactly this problem with the .lake file arose - I've had it on every branch I made for this project, and also when I tried to use a Codespace online

[Paul Lezeau]

(deleted)