Stream: Coq devs & plugin devs

Topic: coqdoc and binder index


view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (Mar 26 2022 at 20:08):

https://github.com/coq/coq/issues/13155 ?

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Mar 26 2022 at 20:19):

you should do it
Hugo is pretty busy AFAIK

view this post on Zulip 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

view this post on Zulip 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:.

view this post on Zulip 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: Feb 06 2023 at 00:03 UTC