Entries from all modules of persistent env extension

Stream: metaprogramming / tactics

[Adam Topaz]

What's the preferred way to get a list of all the entries from all modules associated with a persistent env extension? Do I just need to iterate over all modules and use docs#Lean.PersistentEnvExtension.getModuleEntries or are there some helper functions for this?

[Patrick Massot]

Do you mean all modules, even if they are not imported by the current file?

[Adam Topaz]

no, just the ones that are imported.

[Patrick Massot]

Actually I may have misunderstood the question. Do you really mean entry and not state?

[Patrick Massot]

Because the state is accessible by docs#Lean.PersistentEnvExtension.getState and usually contains more information that the entries.

[Adam Topaz]

oh yeah I see now. I'm juts misunderstanding what's actually hapenning with the state so I probably have another issue.

[Adam Topaz]

let me make things more precise. one sec.

[Adam Topaz]

Here's the situation: I have three files in a project Test/Init.lean, Test/Basic.lean and Test.lean with the following contents:

-- Test/Init.lean
import Lean
open Lean

initialize testAttr : TagAttribute ← registerTagAttribute `test_attr ""

elab "foo" : term => do
  let state := testAttr.ext.getState (← getEnv)
  return mkNatLit <| state.toList.length

-- Test/Basic.lean

import Test.Init

@[test_attr]
def a := 0

#eval foo -- 1 (as expected)

and

-- Test.lean

import Test.Basic

#eval foo -- 0

I just want to understand how to get 1 from foo in Test.lean.

[Adam Topaz]

now, I can modify the elaborator for foo to pick up a by iterating through the imported modules as indicated in the original question.

[Jannis Limperg]

See docs#Lean.TagAttribute.hasTag. The state of a tag attribute only stores tagged decls from the current module. Tagged decls from imported modules are stored in one sorted array per module, and to determine whether a decl from a module is tagged, you can do binary search on that module's array. To get the number of tagged decls, you can sum up the sizes of the module arrays.

[Adam Topaz]

okay, what's exactly what I was trying to ask in the original question :)

[Adam Topaz]

is there no way to collect all names of constants which have been tagged without iterating through the modules?

[Jannis Limperg]

Don't think so. It's a bit annoying, but this representation is much more efficient. (In particular, it has zero import overhead.)

[Adam Topaz]

yeah, I figured it had to do with efficiency. It's a bit confusing that the env extension in TagAttr is a PersistentEnvExtension, but the state doesn't persist :(

[Adam Topaz]

structure TagAttribute where
  attr : AttributeImpl
  ext  : PersistentEnvExtension Name Name NameSet
  deriving Inhabited

[Adam Topaz]

how do tactics like simp keep track of names of lemmas tagged with simp? Is there some custom env extension used?

[Jannis Limperg]

Yes, simp uses docs#Lean.Meta.SimpTheorems (and now a similar structure for simprocs). There the state of the extension really contains all simp theorems registered in the current or imported modules.

[Jannis Limperg]

The extension for a tag attribute is still 'persistent' in the sense that its entries are written to the oleans for each module, rather than thrown away after the module has been checked. That's what technically distinguishes a persistent from a non-persistent env extension. How an extension represents its state, including imported entries, is for each extension to determine.

[Adam Topaz]

okay, fair enough. So it's really about the implementation of registerTagAttribute, is that right?

[Jannis Limperg]

Yes, that one defines exactly what happens with the entries at import/export and when a decl is tagged.

[Adam Topaz]

I see now, the code for addImportedFn in this implementation is addImportedFn := fun _ _ => pure {}.

[Patrick Massot]

This is indeed what prevents you from doing anything here.

[Thomas Murrills]

Related discussion (though it might not seem so by the name): #lean4 > Label attribute improvements? (Oops, realizing I’m late to this thread. But here it is in case anyone reads the thread later. :) )