some Stacks tag doesn't show up in docs

[alreadydone]

IsLocalRing.local_hom_TFAE is labelled @[stacks 07BJ] but this doesn't show up in the docs.

[hargoniX]

Stacks is not a built-in environment extension and can thus not be understood by doc-gen at the moment due to architectural reasons, sorry.

[alreadydone]

It looks like the Stacks tag will be ignored by doc-gen if the decl has a docstring. Though "docstrings" enclosed quotation marks after a Stacks tag will not affect display of the Stacks tag in the docs. Compare Module.support and Module.support_subset_of_injective.

[erdOne]

I don't think this is a doc-gen issue though. I think the issue is that stacks tag once appended the stacks links to actual docstrings (and doc-gen can see docstrings) but now the code doesn't really work.

[acmepjz]

I don't think this is a doc-gen issue though. I think the issue is that stacks tag once appended the stacks links to actual docstrings (and doc-gen can see docstrings) but now the code doesn't really work.

Yes, the stacks tag logic is not in doc-gen, but in mathlib itself. Seems that the code added in leanprover-community/mathlib4#19131 stopped working properly, but not sure why.

https://github.com/leanprover-community/mathlib4/pull/23614/files#diff-84134e313ce3b4ad1c920b80fdf1fccf38864e3d8c76556032c71484e74d92ba changes addDocString to addDocStringCore, does it cause the problem?

[Vierkantor]

addDocString and addDocStringCore seem to both do the same thing with respect to environment extensions. Maybe the issue is that replacing the docstring of an existing declaration doesn't work? On the other hand, when staring at the code for docStringExt nothing jumps out at me as weird.