mathlib caching doesn't work for me

Stream: new members

[Geoffrey Irving]

Each time I upgrade mathlib using leanproject upgrade-mathlib, it downloads a bunch of cache files but then seems to ignore the cache when I go to rebuild my project (it rebuilds a ton of mathlib files). This makes builds after upgrades take a long time. Any ideas why the caching might not be working? I'm on an M1 Mac if that's relevant, and using Lean from homebrew rather than elan since when I first installed Lean elan didn't support M1.

[Eric Wieser]

Does lean --version output something that matches the contents of your leanproject.toml?

[Geoffrey Irving]

It looks like

% lean --version
Lean (version 3.50.3, Release)

and

[package]
name = "ray"
version = "0.1"
lean_version = "leanprover-community/lean:3.50.3"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "44b58b42794e5abe2bf86397c38e26b587e07e59"}

[Eric Wieser]

What does lean --make one_of_your_files do? Does it start building files in mathlib rather than your stuff?

[Eric Wieser]

leanproject --version would also be a good thing to check

[Geoffrey Irving]

It complains that I haven't updated my files for the mathlib changes, and then starts building part of mathlib (some measure theory, in this case).

% lean --make uniform.lean
/Users/geoffreyi/ray/_target/deps/mathlib/src/algebra/order/ring.lean:1:0: error: file '/Users/geoffreyi/ray/_target/deps/mathlib/src/algebra/order/ring.lean' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more
/Users/geoffreyi/ray/src/tactics.lean:1:0: error: file '/Users/geoffreyi/ray/_target/deps/mathlib/src/algebra/order/ring.lean' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more
/Users/geoffreyi/ray/_target/deps/mathlib/src/measure_theory/measure/haar.lean: parsing at line 288

[Eric Wieser]

And leanproject --version?

[Geoffrey Irving]

% leanproject --version
leanproject, version 1.1.1

[Eric Wieser]

Try deleting _target/deps, then running leanpkg configure, then leanproject get-mathlib-cache

[Eric Wieser]

Although if you're curious what went wrong, before you do that...

[Eric Wieser]

Cd into Users/geoffreyi/ray/_target/deps/mathlib and run git diff

[Geoffrey Irving]

git diff doesn't show anything, since I'm on a detached HEAD branch with no changes. To clarify, do you know what went wrong, or is this a guess?

[Eric Wieser]

My guess was that you modified something by accident. I know that you can safely delete that folder and regenerate it; and I'm guessing that the regenerated version might magically fix everything

[Kevin Buzzard]

Try leanproject get-mathlib

[Eric Wieser]

Kevin, I already wrote that above. get-mathlib is just a truncated spelling of get-mathlib-cache.