attributes in docs

Stream: mathlib4

[Kevin Buzzard]

I just noticed that docs4#CategoryTheory.Iso.symm doesn't indicate that the declaration is tagged with @[symm]. Is this expected? Note that later declarations on that web page are correctly shown with the @[simp] attribute attached.

[Scott Morrison]

I suspect this is an aspect of the whole "there is no uniform mechanism for asking which attributes are on a declaration" problem. :-(

[Kevin Buzzard]

I guess that it's not the end of the world if we can't see these in the docs. I've got used to them from mathlib3 but at the end of the day I'm not sure I'm particularly interested in seeing whether something is tagged symm apart from when I'm trying to debug teething troubles with symm.

[Henrik Böving]

The issue is that doc-gen4 needs to know about the environment extension and its types etc. In order to access this information. But since symm is not in core (I thibk?) That would require it to pull that in as a dependency cycle :/

[Scott Morrison]

It's increasingly clear we need a centralised store of which declarations have which attributes, no?

[Henrik Böving]

Thinking further though there might be a way for a package to provide extractor functions to doc-gen via some meta programming mechanism but I'm not sure.

And I agree that that would be the simpler solution

[Filippo A. E. Nuccio]

I am reviving this old topic to ask whether there is

1. A list of all mathlib attributes?
2. A reference about "what" an attribute is and how it works. I have tried looking at the doc for the ext one and it looks daunting. Is there perhaps an easier example to understand what lies behind the scene?

[Yury G. Kudryashov]

AFAIR, currently, an attribute is a syntax for calling any metaprogram. It is responsible for maintaining its data, and there is no uniform way to query all attributes. If you want to support specific attributes in your code, then you have to look at each of them and see how it stores its data (probably, in some env extension).

[Filippo A. E. Nuccio]

Thanks! As a matter of fact mine was more of a pedagogical question, aimed at understanding what is there under the hood rather than adding something to my code.

[Filippo A. E. Nuccio]

I'll try to keep on digging.

[Edward van de Meent]

Yury G. Kudryashov said:

and there is no uniform way to query all attributes.

doesn't #help attribute do this?

[Kyle Miller]

I think Yury was indirectly answering your question about "what" an attribute is @Filippo A. E. Nuccio, since the point of view of the metaprogrammer is as under the hood as you can get.

In short: if you write @[my_attr] before a declaration, then this causes a metaprogram to run at some stage of elaboration (configuration: docs#Lean.AttributeApplicationTime), and it can do anything.

A common sort of attribute is one that has an associated environment extension. The environment extension is often a table that keeps track of some collection of declarations, maybe with some associated data, and the data is saved to disk (in olean files) and loaded again by import.

Here are the key parts of the @[ext] system.

• https://github.com/leanprover/lean4/blob/ffac974dba799956a97d63ffcb13a774f700149c/src/Lean/Elab/Tactic/Ext.lean#L199-L205 defines the environment extension. The tree field indexes ext theorems based on the resulting types, for fast lookup.
• The add field for when the ext attribute is declared gives the metaprogram. It is given the declaration being defined. In the basic case of an ext lemma, this line is where the lemma is installed in the environment extension (where it is added to tree).
• Much of the other code is for realizing ext theorems for structures and ext_iff theorems from ext theorems. There's also some validation that the ext theorems have the correct form.

Then, the ext tactic reads this environment extension when trying to find an applicable ext lemma. If there were no ext tactic, there would still be a case for having a @[ext] attribute: we could delete the environment extension, and then @[ext] would just be responsible for realizing ext theorems for structures and for realizing ext_iff theorems from ext theorems. In that case, there would be no way to know for sure whether @[ext] was ever applied (all we can see is that there are the ext and ext_iff theorems available, which may have been written by hand).

[Kyle Miller]

@Edward van de Meent Yury means "there's no uniform way to query the data of attributes". You are right that you can query Lean for the list of all attributes that exist.

[Kyle Miller]

There's a core PR in progress for "attribute delaborators" to give an interface where attributes can read their own data and represent themselves as syntax, on a best-effort basis. lean4#6115

[Filippo A. E. Nuccio]

Wow, thanks a lot for the detailed explanation. It'll take time to digest, in the meanwhile I am really grateful.