Bas Spitters (Apr 15 2021 at 12:55): 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 ?
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.
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.
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.
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: Oct 13 2024 at 01:02 UTC