coqdoc generated index.html too verbose ?

[Casteran]

Hi,

The file index.html generated by coqtop contains a lot of links associated with bound variables.
For instance, the following lemma

Lemma eq_b_iff (alpha beta : T1) :
  eq_b alpha beta = true ↔ alpha = beta.

generates the entry

alpha:130 [binder, in hydras.Epsilon0.T1]

The same problem occurs even in the case of an explicitely quantified variable.
Thus, I get at least one thousand entries for the variable alpha !

Is it possible to tell coqdoc not to insert binders in the index ?

Pierre
(on Coq 8.12.0 (July 2020))

Coq Version

[Casteran]

Hello,

Perhaps it's just a problem of readability : Roughly 2/3 of the global index entries are binder entries (whose name is not so relevant), and the file index.html starts with the global index, where this amount of entries is merged with lemmas, definitions, etc. So, it's better to skip the global index and jump to specialized indices (at the end of the page).
Is the global index at the beginning of the page really useful, since the same information is sorted and displayed later ?

Best regards,

Pierre

[palmskog]

For the record, I have hit this issue multiple times in multiple Coq projects: the binder index takes up half or more of the global index and leads to huge HTML files. This is especially annoying when using GitHub Pages in the gh-pages branch, which has to hold all the redundant HTML. In my opinion, binder indexes should not be generated by default, but only after passing a flag.

[SkySkimmer]

The binder index seems to have been introduced by #12033 (8.12), indeed it doesn't appear in https://coq.inria.fr/distrib/V8.11.0/stdlib/genindex.html
However it doesn't seem to have been the main point of the PR, which is more about having a link between the 2 xs in fun x => x.
cc @herbelin

[herbelin]

I did not realize that adding links for binders would create an index. I don't think it is useful indeed.