coqdoc with -g option omits all sentences with decorations

[palmskog]

Description of the problem

Consider the following example file, mysum.v, adapted from Datatypes.v in the stdlib:

#[universes(template)]
Inductive mysum (A B:Type) : Type :=
  | myinl : A -> mysum A B
  | myinr : B -> mysum A B.

Now, assume we run coqdoc with the -g option (used when generating the official HTML documentation):

coqdoc --html -g mysum.v

This results in a HTML file where the mysum definition is missing:

<div id="main">

<h1 class="libtitle">Library mysum</h1>

<div class="code">
</div>
</div>

This is not restricted to HTML, e.g., the following gives a PDF without the mysum definition:

coqdoc --pdf -g mysum.v -o mysum.pdf

Note that this is restricted to inductives with #[universes(template)] annotations, and dropping the -g option makes everything work as expected.

The absence of these annotated inductives makes it difficult to read the stdlib documentation for Coq 8.10, and invalidates many links in generated HTML documentation.

For example, here is the URL failing to pinpoint the definition of sum: https://coq.inria.fr/distrib/V8.10.2/stdlib/Coq.Init.Datatypes.html#sum
This URL was actually fully functional in the 8.9 documentation: https://coq.inria.fr/distrib/V8.9.0/stdlib/Coq.Init.Datatypes.html#sum

Coq Version

This affects coqdoc in all released 8.10 versions, 8.11beta1 and master.

[palmskog]

I've now checked that, unsurprisingly, any sentence is omitted by coqdoc -g if it is preceded by an attribute list, e.g., #[program] and #[local]. However, since #[universes(template)] is the near-exclusive annotation used in the stdlib, this is probably the only way real users are affected.

[palmskog]

@ppedrot I propose that, unless someone fixes this issue soon, you use a workaround for producing the HTML documentation of stdlib for 8.11.0. For example, @SkySkimmer suggested that one can simply remove all annotations/decorations from stdlib before the coqdoc run. @ejgallego indicated that this could be scripted quite easily.

As I'm sure other users can also attest, having accurate coqdoc HTML documentation of stdlib is crucial. Also, any coqdoc for user projects automatically links to the stdlib HTML pages, meaning there will be many dead anchor links in all deployed project HTML documentation.

[Zimmi48]

before the coqdoc run

Documentation is automatically built and deploy. I'd rather not change this, so if this must be the temporary solution, I'd rather go for an actual removal of the annotations until this is fixed. Given that the warning is off by default now, we wouldn't even need to do anything else.

[ppedrot]

This needs a fix, be it hackish, like, now.

[Zimmi48]

@ppedrot Just remove the attributes for now. Not having them doesn't trigger any warning anymore IIUC.

[ppedrot]

Will wait for a quick input from @palmskog, and in the absence of answer, I'll open a 8.11 PR removing the template attributes.