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