`uncaught exception: unknown package 'ImportGraph'` when Mathlib is not built

[dranov]

If I run lake exe loogle '(List.replicate (_ + _) _ = _)' (the example command in the README) without running lake build LoogleMathlibCache beforehand, I get the following very uninformative error:

uncaught exception: unknown package 'ImportGraph'

Running lake build LoogleMathlibCache fixes the issue.

[nomeata]

Thanks!

Essentially, if you don’t pass --module, it tries to load Mathlib and its dependencies. Probably lake build LoogleMathlibCache, besides building the cache, built Mathlib.

So I expect lake build Mathlib would have helped just the same (but building the cache is of course also good, makes the queries faster).

Did you run lake exe cache get before?

[dranov]

Hi @nomeata. Yes, I did run lake exe cache get before. I followed the README steps, which (given your explanation) seem to assume that lake exe cache get does build Mathlib. Looking at the output in step 2 below, it doesn't seem that is true.

Either running lake build Mathlib or lake build LoogleMathlibCache makes the query in step 3 work rather than end with an exception.

---

Steps to reproduce:

1. Run git clone https://github.com/nomeata/loogle.git
2. Run lake exe cache get. Output is:

$lake exe cache get
info: mathlib: cloning https://github.com/leanprover-community/mathlib4 to './.lake/packages/mathlib'
info: std: cloning https://github.com/leanprover/std4 to './.lake/packages/std'
info: Qq: cloning https://github.com/leanprover-community/quote4 to './.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to './.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to './.lake/packages/proofwidgets'
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: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [6/9] Compiling Cache.Main
info: [9/9] Linking cache
No files to download
Decompressing 4120 file(s)
unpacked in 26821 ms

3. Run loogle '(List.replicate (_ + _) _ = _)'. Output:

   info: [21/130] Compiling Std.Util.Pickle
   <other compilation elided>
   info: stdout:
   [INFO] LOOGLE_SECCOMP is not set
   <other compilation elided>
   info: [159/182] Building Loogle.Find
   info: [177/182] Compiling Loogle.Find
   info: [177/182] Building Loogle
   info: [179/182] Compiling Loogle
   info: [182/182] Linking loogle
   uncaught exception: unknown package 'ImportGraph'

---

Environment:

$elan --version
elan 3.0.0 (cdb40bff5 2023-09-08)
$lake --version
Lake version 5.0.0-ca7d6da (Lean version 4.4.0)

[nomeata]

I think this used to work, ImportGraph is a new dependency, so there is something to debug here… ah, yes, it’s a problem with mathlib: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Imports.20are.20out.20of.20date.20even.20after.20getting.20cache.2E/near/412772807

So once that’s resolved it should work here as well again.

[nomeata]

Should be fixed now that I updated mathlib. Thanks for reporting!