exact? cares about imports?

Stream: general

[Alex Meiburg]

So I had a lemma in a file and when I used it later, exact? found it just fine. But then I moved it to a file that I directly import, and exact? became unable to find it. There is no namespacing involved, it's the last file imported, and precisely the same exact lemma_name line closes the goal.

Why is this / how do I make my lemma discoverable?

[Yaël Dillies]

Is this not a cache issue?

[Alex Meiburg]

Is it? What does that mean?

[Alex Meiburg]

To be clear it's not a Lean server "I don't know this lemma exists" issue, because explicitly naming the lemma with exact, or just using it in term mode, works fine.

The term mode also has me convinced that this isn't some snazzy extra stuff exact is doing. It's not just defeq, the lemma is character-for-character identical to the goal, with the appropriate hypothesis

[Alex Meiburg]

Alright, I'm pretty sure it's nothing about caching on any level. Changing the imported file to force a fresh build, restarting the Lean server, etc. all doesn't change it.

exact? just doesn't find lemmas defined in the other file. It does find ones defined in the current file.

[Alex Meiburg]

I see in LibrarySearch.lean,

def cachePath : IO FilePath :=
  try
    return (← findOLean `MathlibExtras.LibrarySearch).withExtension "extra"
  catch _ =>
    return ".lake" / "build" / "lib" / "MathlibExtras" / "LibrarySearch.extra"

/--
Retrieve the current current of lemmas.
-/
initialize librarySearchLemmas : DiscrTreeCache (Name × DeclMod) ← unsafe do
  let path ← cachePath
  if (← path.pathExists) then
    -- We can drop the `CompactedRegion` value from `unpickle`; we do not plan to free it
    let d := (·.1) <$> unpickle (DiscrTree (Name × DeclMod)) path
    DiscrTreeCache.mk "apply?: using cache" processLemma (init := d)
  else
    buildDiscrTree

which makes me wonder if there is some "deeper" cache that is not refreshed just by restarting the Lean server and rebuilding the file. (That would feel very louser as a user experience.)

[Yaël Dillies]

Yes, that's I was trying to tell you. Sorry if I was unclear

[Alex Meiburg]

I see. Yeah, I'd never really peeked inside LibrarySearch before and I don't know how this caching happens. How can I clear this cache? Just deleting the LibrarySearch.extra file? -- will that force a whole rebuild?

[Alex Meiburg]

oh --- is the issue that MathlibExtras/LibrarySearch.lean imports Mathlib but not my own custom library, so that will make it unable to find those lemmas I proved?

I thought exact? would search through all of the current working context, I didn't realize it only searches mathlib

[Mauricio Collares]

Are you using an old version of mathlib? exact? moved to core a while ago (in v4.7.0), and I think the new version should search everything.

[Alex Meiburg]

Ahhh. Hmm, ok

[Notification Bot]

Jordan has marked this topic as resolved.

[Notification Bot]

Jordan has marked this topic as unresolved.

[Jordan]

Sorry about that. I was trying to mark this thread as read.

[Jovan Gerbscheid]

Yes, the old mathlib version of exact? only searches in the current file, and in mathlib. Not in imported files outside of mathlib.