KeyedDeclsAttribute

Stream: lean4

[Daniel Selsam]

Does anybody have a working example of declaring a new (non-builtin) KeyedDeclsAttribute?

[Mario Carneiro]

I thought that custom attributes were not yet supported? I tried going through the motions a while ago and hit some error about initialize not working after initialization

[Daniel Selsam]

Okay, thanks.

[Mac]

Mario Carneiro said:

I thought that custom attributes were not yet supported? I tried going through the motions a while ago and hit some error about initialize not working after initialization

What makes you think that custom attributes are not yet supported? It seems to me one can register attributes the same way core Lean does (with builtin_initialize).

[Mario Carneiro]

that's what I thought as well, but I tried it and it didn't work

[Mario Carneiro]

and I didn't know enough about how initialize is set up to troubleshoot it

[Mario Carneiro]

Here's a MWE:

-- A.lean
initialize fooAttr : TagAttribute ←
  registerTagAttribute `foo "test"

-- B.lean
import A -- error: failed to register environment, extensions can only be registered during initialization

[Mac]

Yes, you can't use initialize, but you can use builtin_initialize

[Mac]

I think initialize, despite its name, actually runs after initializing the environment, whereas bulitin_initialize actually runs during initialization.

[Mac]

However, I think this may mean you need to feed in the code that initializes the attribute as a --plugin to lean.

[Mac]

Unfortunately, I had trouble testing this due to issue #486 (which I just posted).