tagged attributes not persisting across imports

Stream: general

[Frederick Pu]

I'm registering a tagged attribute:

import Lean

open Lean Meta Elab Command

initialize euclidAttr : TagAttribute ←
  registerTagAttribute `euclid "Used to mark System E inference axioms"

elab "#printTagged" : command => do
  let env ← getEnv
  let decls := euclidAttr.ext.getState env
  for decl in decls do
    logInfo m!"Tagged: {decl}"

When I printTagged in a file where the attributes are declared it works fine ```

import SystemE.Theory.Relations
import SystemE.Meta.Attr
@[euclid]
axiom two_points_determine_line :
  ∀ (a b : Point) (L M : Line), distinctPointsOnLine a b L ∧ (a.onLine M) ∧ (b.onLine M) → L = M

However if I import the above file and printTagged I don't get anything

import SystemE.Theory.Inferences.Diagrammatic
import SystemE.Theory.Inferences.Metric
import SystemE.Theory.Inferences.Transfer
import SystemE.Theory.Inferences.Superposition

#printTagged

Is it my way getting the enviroment that's wrong or is the attribute simply not persisting across imports?

[Kyle Miller]

Is it my way getting the enviroment that's wrong

Yes, getState gets the module-local state. Take a look at the source for docs#Lean.TagAttribute.hasTag (the intended interface). In the source you can see that there's getModuleEntries for the tagged declarations per imported module.

[Frederick Pu]

so how would I get all imported modules?

[Frederick Pu]

actually I would like to do it in a similar way that simp does it where a single Extension gets updated everytime. Any tips?

[Adam Topaz]

You can make your own persistent env extension and attribute from scratch.

[Kyle Miller]

docs#Lean.LabelExtension is probably what you want

[Frederick Pu]

thx!