On the implementation of attributes in doc-gen

Stream: lean4

[Henrik Böving]

After reading through https://leanprover-community.github.io/mathlib4_docs/Lean/Attributes.html (yay I can use my own tool for something useful by now \o/) and the corresponding code it seems to me that implementing these pure tag based attributes is a triviality really but the ones that attach information won't be possible to do generically? After all there is never a constriant on the associated value to have a representation or to string.

Hence my question: Which non tag based attributes should doc-gen look for per default? The only one that comes to mind from the top of my head would be the implementedBy one.

[Gabriel Ebner]

This is a great question.

[Gabriel Ebner]

To explain the status quo: in Lean 4 there are attributes, and then there's environment extensions. Attributes are not persisted, they are similar to commands like #eval, they are triggered when a definition is elaborated but they are responsible to save any needed information. After an attribute is elaborated, there is no record of its existence.

Environment extensions are an API to store whatever data you want in the environment. There is no way to inspect this data in a generic way.

[Gabriel Ebner]

Practically, what you can do today is gather all the attributes that we care about and query the corresponding environment extensions about relevant information. Hopefully this information can be translated back to a nice @[simp].

[Gabriel Ebner]

While this separation is bad to inspect attributes, it's actually a much better fit for some of the attributes we have in mathlib. Attributes like @[ext], @[simps], @[toAdditive] are mostly used for their side effects (generating extensionality lemmas, projection lemmas, additive versions of definitions, resp.). In Lean 3 we usually had to use two attributes, e.g. ext which triggered the side effect, and _ext_core which recorded the data in the environment.

[Mario Carneiro]

Should we have a generic interface for attributes that want to be visible on inspection? Perhaps attributes can register a #print-callback which queries their internal state and prints some additional information to be added to the report

[Gabriel Ebner]

I'm not sure if you're mixing up attributes and env extensions. Printing the internal state makes sense for environment extensions (and I think that would be a great idea, it only requires recording a Format/ToMessageData instance in the extension registration.)

It would also be very useful (but much less clearly defined) to dump the state of the environment as attributes (i.e., syntax objects in the attr category).

[Mario Carneiro]

I meant attribute in the organizational sense. A single attribute might correspond to one or more environment extensions, but from the user perspective it's probably the attribute that is naming the file, for instance

[Mario Carneiro]

Actually, one such logical unit could correspond to many attributes and one env extension, or one attribute and many env extensions, and print-extensions would be another axis along which these components interact

[Mario Carneiro]

Re: attribute syntax, I think both options are reasonable. Perhaps a print-extension returns an object that can be printed either as a message data or as a syntax (with possibility for failure / opt out). I doubt we can "round trip" very effectively in general though

[Mac]

There is also already functions like registerTagAttribute that add both the syntax and environment extension at the same time. Such functions could also register some other piece of information that could be used by doc-gen to retag definitions.

[Gabriel Ebner]

AFAICT registerTagAttribute does not store the syntax anywhere. (Though it's trivial to get back an equivalent attribute syntax since there's no parameters and the environment extension is essentially a list of declaration names.)

[Henrik Böving]

I came up with this implementation for now https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Attributes.lean ...I guess it is possible to generalize the special snowflake simp to a tag attribute and the tag attribute also to a ValueAttr with a bit more abstraction but I think it's fine like this for now :sweat_smile:

It also felt both amazing (as in that this works) but also hacky to abstract it this way, is this actually reasonable code or did I come up with a complete monstrosity?

[Henrik Böving]

At least it works https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html :octopus:

[Edward Ayers]

I bumped in to this too when implementing to_additive. In mathlib3 to_additive will copy over all of the attributes (from a fixed list) to the new additive definition, but you can't do this in Lean 4 because the attributes for a given declaration are not stored anywhere. Any ideas on how to implement a to_additive that copies over attributes?

[Alex J. Best]

I think that's part of the reason a fixed list is used in Lean 3 too, there isn't a way to get all attributes for a given decl, but only a way to check if the declaration has an explicitly named attribute IIRC.
The fact that there are a lot of random attributes that are used internally too that we didn't want to copy, but it sounds like it should be similar in 4?

[Alex J. Best]

Me and Johan had to do something similar for the import optimizing tool we wrote, where we began with the full list of used attributes in mathlib and pruned it down: see
https://github.com/alexjbest/dag-tools/blob/master/src/import_optimizer.lean#L67

[Henrik Böving]

Edward Ayers said:

I bumped in to this too when implementing to_additive. In mathlib3 to_additive will copy over all of the attributes (from a fixed list) to the new additive definition, but you can't do this in Lean 4 because the attributes for a given declaration are not stored anywhere. Any ideas on how to implement a to_additive that copies over attributes?

In fact just straight up doing this might be something you do not want to do because there are attributes like export which would cause the same name to appear twice in the resulting c binary

[Edward Ayers]

I have a list of attributes that to_additive cares about so I'm not too worried about getting other attributes like export. The main problem is getting the attributes for a decl at all since they are not stored anywhere. I was thinking that it might be possible to implement an ad-hoc 'hasAttribute' for each of the attributes in my list.

[`reducible, `_refl_lemma, `simp, `norm_cast, `instance, `refl, `symm, `trans, `elab_as_eliminator, `no_rsimp,
`continuity, `ext, `ematch, `measurability, `alias, `_ext_core, `_ext_lemma_core, `nolint, `protected]

[Leonardo de Moura]

@Edward Ayers We will try to add APIs for retrieving all attributes associated with a declaration.

[Gabriel Ebner]

Note that the main use case with to_additive is to support @[simp, to_additive] (or was it @[to_additive, simp]?). One option could be to have the to_additive attribute accept a list of attributes that are applied to both the additive and multiplicative definition. Something like @[to_additive [simp, norm_cast]]. This would also clarify the order in which the two attributes must be written.

[Damiano Testa]

I'm talking about this, without ever having used Lean4, so I feel that whatever I say might be out of place. There has been a few times where something "like" to_additive, but for other pairs of operations/relations. The ones that appeared were

• proving a lemma about semigroups for the "opposite semigroup",
• proving a lemma about orders for the "dual order".

[Bryan Gin-ge Chen]

See #13461 as well for some more discussion on possible to_* analogues.

[Damiano Testa]

#13461 is an issue about this for mathlib.

[Damiano Testa]

Btw, I have been recently introduced to the (Lean3) meta-world by Arthur Paulino, so have very limited experience, but found the experience really rewarding.

I would be happy to collaborate on helping with these issues, but I do not feel at all qualified to take them on alone.

[Edward Ayers]

Gabriel Ebner said:

Note that the main use case with to_additive is to support @[simp, to_additive] (or was it @[to_additive, simp]?). One option could be to have the to_additive attribute accept a list of attributes that are applied to both the additive and multiplicative definition. Something like @[to_additive [simp, norm_cast]]. This would also clarify the order in which the two attributes must be written.

Right I'll implement it for simp for now, then it should be ready for review