Defining & using attributes in the same file?

Stream: lean4

[Siddharth Bhat]

I'm playing around with declaring attribute with initialize registerBuiltinAttribute. It seems that one can only use the attribute in a file that is _different_ from the one where one has called registerBuiltinAttribute? So in the example below, I would like to uncomment the declaration foo in the file Dummy.lean, but I am unable to do so. Having the ability to declare and use attributes in the same file would help in writing tutorials about attributes. I tried futzing around with namespaces, but that didn't seem to help.

-- Dummy.lean
import Lean
open Lean

syntax (name := dummy_attr) "dummy_attr"  str : attr
initialize registerTraceClass `dummy_attr

initialize registerBuiltinAttribute {
    name := `dummy_attr
    descr :="dummy_attr print information"
    add := fun src stx kind => do
      return ()
  }

-- Can I uncomment this?
-- @[dummy_attr "foo"]
-- def foo : Int := 42

-- Test.lean
import Test.Dummy

-- v this works
@[dummy_attr "main"]
def main : IO Unit := return ()

[Siddharth Bhat]

CC @Arthur Paulino , since if we must have two files, it's going to affect how we structure the chapter on attributes in the Lean4 metaprogramming book

[Henrik Böving]

If I understand the mechanism correctly this is not so much a limitation of attributes but a limitation of the initialization mechanism although I do not know how the initialization mechanism works internally.

[Arthur Paulino]

Siddharth Bhat said:

CC Arthur Paulino , since if we must have two files, it's going to affect how we structure the chapter on attributes in the Lean4 metaprogramming book

Yeah I thought about that too. But we can "take advantage" of this limitation to show the limitation itself. That is, explaining the limitation and then embracing the fact that we'll need to show the attribute usage on a different (next) file

[Jannis Limperg]

Yes, this is a general limitation of initialize.