Imports are out of date even after getting cache.

Stream: mathlib4

[Wrenna Robson]

Trying to work on one of my PRs, just pushed it and got a build failure. Was going to try and diagnose it but even when I do lake exe cache get! it tells me that the imports are out of date and must be rebuilt. But I'm getting 4080/4120 cache files. What could be going on?

[Mauricio Collares]

Is that #9571 (branch#snoc_cons_optimise)?

[Wrenna Robson]

No, #9145

[Wrenna Robson]

#9571 is broken but not because of a merge, I just haven't got round to fixing it yet.

[Josha Dekker]

(deleted)

[Mauricio Collares]

I see the same thing, but "Rebuild Imports" takes just a second here (and needs to be done only once)

[Wrenna Robson]

Oh, I didn't actually press it out of fear :P

[Wrenna Robson]

That has crashed my computer before

[Wrenna Robson]

That worked. Thanks!

[Notification Bot]

Wrenna Robson has marked this topic as resolved.

[Mauricio Collares]

The only thing that gets rebuilt is ImportGraphs.Import, and I think this is a new dependency. Maybe it isn't being cached properly?

[Mauricio Collares]

cc @Jon Eugster

[Jon Eugster]

ImportGraph is in another repo and its not cached at all currently. (it contains lake exe graph and some commands, mentioned below, which were in mathlib previously)

I asked Scott Morrison about this and he claimed there should be no problem with cache. Maybe that's not true?

There's no necessity for ImportGraph.Imports to be imported in mathlib except for having the commands like #find_home and #minimize_imports still available in mathlib without adding the import manually.

How are other projects like aesop or proof-widgets cached? Maybe that should be done for the import-graph too?

https://github.com/leanprover-community/import-graph

[Kim Morrison]

Sorry about the bad information, cache does need an update.

[Notification Bot]

Scott Morrison has marked this topic as unresolved.

[Kim Morrison]

If you search for aesop with the Cache/ directory of Mathlib you will find the function that needs a line added!

[Kim Morrison]

This is an unfortunate consequence of cache being a giant (lovely, essential) hack. :-)

[Mario Carneiro]

why is ImportGraph a dependency of mathlib in the first place? surely it isn't imported by anything

[Mario Carneiro]

we really need dev-dependencies...

[Kim Morrison]

Similarly lean4-cli is only used by auxiliary utilities.

[Eric Wieser]

Is lean4-cli not used by cache get?

[Kim Morrison]

No, cache just handles command line arguments manually.

[Joachim Breitner]

But ImportGraph is imported, by Mathlib.Tactic.Common:

~/build/lean/mathlib4 $ git log -n 1
commit 5964134838f12fb0ea6fde72764f6d985c312842 (HEAD -> master, origin/staging, origin/master, origin/HEAD)
Author: Kyle Miller <kmill31415@gmail.com>
Date:   Mon Jan 15 11:29:49 2024 +0000

    refactor: make `SimpleGraph.chromaticNumber` be `ENat`-valued (#8883)

    This removes an awkwardness of the API, where theorems had to include colorability hypotheses. This trades that awkwardness for a smaller one, which is that one writes `G.Colorable (ENat.toNat G.chromaticNumber)` rather than `G.Colorable G.chromaticNumber`.

    It would be good to have a followup refactoring PR to more carefully evaluate the API after this change.

~/build/lean/mathlib4 $ rm -rf .lake
~/build/lean/mathlib4 $ lake exec cache unpack
info: Cli: cloning https://github.com/leanprover/lean4-cli to './.lake/packages/Cli'
info: importGraph: cloning https://github.com/leanprover-community/import-graph.git to './.lake/packages/importGraph'
info: [0/9] Downloading proofwidgets cloud release
info: [0/9] Unpacking proofwidgets cloud release
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: [4/9] Compiling Cache.Requests
info: [4/9] Building Cache.Main
info: [6/9] Compiling Cache.Main
info: [9/9] Linking cache
Decompressing 4120 file(s)
unpacked in 7537 ms
~/build/lean/mathlib4 $ ls .lake/packages/importGraph/.lake/build/lib/ImportGraph/Imports.olean
ls: Zugriff auf '.lake/packages/importGraph/.lake/build/lib/ImportGraph/Imports.olean' nicht möglich: No such file or directory
~/build/lean/mathlib4 $ find Imports.olean
find: ‘Imports.olean’: No such file or directory
~/build/lean/mathlib4 $ git grep ImportGraph
Mathlib/Tactic/Common.lean:import ImportGraph.Imports
~/build/lean/mathlib4 $ lake build Mathlib.Tactic.Common
[115/193] Building ImportGraph.RequiredModules
[433/435] Building ImportGraph.Imports

[Joachim Breitner]

Plausible fix: https://github.com/leanprover-community/mathlib4/pull/9760