Stream: Coq users

Topic: Pointers in the stdlib documentation


view this post on Zulip Bas Spitters (Apr 15 2021 at 12:55):

A small usability issue. If I google for things in the stdlib I often end up on an old version of Coq.
E.g. "coq stdlib int63" for me points to: https://coq.github.io/doc/v8.11/stdlib/Coq.Numbers.Cyclic.Int63.Int63.html

The refman gives gentle pointers to newer versions. Would it be helpful to do the same for the stdlib?
@Théo Zimmermann ?

view this post on Zulip Théo Zimmermann (Apr 15 2021 at 12:58):

Yes, but this is beyond my area of expertise. I would welcome any improvements to the stdlib documentation, but I know nothing about coqdoc and how to customize it.

view this post on Zulip Théo Zimmermann (Apr 15 2021 at 12:58):

So if you find a volunteer to write a widget adding this feature, their PR would be most welcome.

view this post on Zulip Bas Spitters (Apr 15 2021 at 14:05):

Alternatively, one could remove these old copies, or use robot.txt to tell google not to index them.
Not sure about the right solution.

view this post on Zulip Théo Zimmermann (Apr 15 2021 at 14:44):

Remove: definitely not. People citing things in papers need permalinks to documentation for a fixed version of Coq. Avoiding indexing by Google, maybe, I'm not sure what is possible to do.


Last updated: Jan 28 2023 at 07:30 UTC