Zulip Chat Archive

Stream: mathlib4

Topic: attributes in docs


Kevin Buzzard (Dec 04 2022 at 22:17):

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 (Dec 05 2022 at 23:24):

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 (Dec 06 2022 at 07:19):

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 (Dec 06 2022 at 10:19):

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 (Dec 06 2022 at 10:20):

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

Henrik Böving (Dec 06 2022 at 10:21):

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


Last updated: Dec 20 2023 at 11:08 UTC