Karl Palmskog (Mar 26 2022 at 19:14): Karl Palmskog (Mar 26 2022 at 19:14):In the Coq stdlib index, about 65% of the entries are binders. Similarly, in a randomly chosen project of mine, the binders are 45% of the entries in the index.
It's likely that nobody ever consults the binder index, for any reason. Yet, I can't find an easy way to disable binder index generation and listing... Worth an issue, or is this well known?
Gaëtan Gilbert (Mar 26 2022 at 20:08):https://github.com/coq/coq/issues/13155 ?
Karl Palmskog (Mar 26 2022 at 20:17):OK, I'm tempted to just do a PR purging the binder index from everywhere, but hopefully Hugo can suggest something less radical
Gaëtan Gilbert (Mar 26 2022 at 20:19):you should do it
Hugo is pretty busy AFAIK
Karl Palmskog (Mar 26 2022 at 20:21):OK, I guess he might just do a :thumbs_up: or :thumbs_down: on the PR if he's still monitoring coqdoc stuff
Hugo Herbelin (Mar 28 2022 at 16:46):Copying my comment on #13155: I did not realize that adding links for binders would create an index. I don't think it is useful indeed. If there is a PR for removing it, it is a :+1:.
Karl Palmskog (Mar 28 2022 at 17:16):OK, I will put this on my plate then, hopefully a PR in 1-2 days.
Last updated: Apr 19 2024 at 16:01 UTC