Coq: Feature Request: Documentation in the texinfo format

[co-dan]

I think it would be nice to have Coq Reference Manual available also in the texinfo format.
I am no expert on Sphinx, but I think it should be possible to make it output texinfo files.

[Zimmi48]

If it's doable easily, why not? But let's not take any engagements in case it turns out to be a pain to maintain.

[co-dan]

I will try to look into it myself later this week, if I can get my head around the the build system.

[Zimmi48]

Feel free to ask as many questions as you need!
Note that for 8.10 we plan to get rid of the Makefile.* and use dune only for the build. However, in the case of Sphinx, the support is still pretty rudimentary (see https://github.com/coq/coq/blob/master/doc/dune). In particular, it does not support yet building the PDF version of the manual, although that shouldn't be too much work.

[co-dan]

I looked into it, and here are my basic findings.

I've tried to enable the TeXinfo generation for Sphinx using this change:

diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst
index c66202877..8c2b5cad8 100644
--- a/doc/sphinx/refman-preamble.rst
+++ b/doc/sphinx/refman-preamble.rst
@@ -1,6 +1,6 @@
 .. This file is automatically prepended to all other files using the ``rst_prolog`` option.

-.. only:: html
+.. only:: html, texinfo

    .. This is included once per page in the HTML build, and a single time (in the
       document's preamble) in the LaTeX one.

and running make refman-texinfo. Unfortunately the texinfo that it generates is not very pretty:

1. https://user-images.githubusercontent.com/2814972/52719634-4af29800-2fa6-11e9-9ae5-58317275bf6b.png
2. https://user-images.githubusercontent.com/2814972/52719635-4b8b2e80-2fa6-11e9-8d0c-03081d46a23c.png

For the html output the corresponding sections look like this: https://coq.inria.fr/refman/language/cic.html#admissible-rules-for-global-environments, https://coq.inria.fr/refman/language/gallina-specification-language.html#definition-of-recursive-functions.
In the first case the web page uses MathJax (or something similar) for rendering mathematics. I am not sure what can be done to the texinfo output, IIRC you can't just display mathematics inline.

The latter issue (the "see .." prefix for all the cross-references) is the artefact of the default Emacs behavior and, I guess, the way that info files are normally written. To mitigate this you can set Info-hide-note-references to (quote hide) and Info-refill-paragraphs to t. But even then it still puts periods after the identifiers.

I guess I will try to use the generated info page by consulting it for my work, and see if it is actually useful or not.

[Zimmi48]

Very cool @co-dan! It is my impression that fixing the second issue only would already be an acceptable compromise. People can understand that when they see LaTeX, it means that they need to view this in another format so that it is displayed right.

[vapniks]

If you can figure out a way to generate images for the latex snippets, you should be able to insert inline links to the images which are displayed by emacs: https://www.gnu.org/software/texinfo/manual/texinfo/html_node/Image-Syntax.html

[co-dan]

Hi! Sorry for abandoning this thread.

@vapniks I see, this might be interesting, but I have no idea how to generate all those images

meanwhile I've been using the TeXInfo manual in my emacs and it's been kinda nice, if you know about the limitations of it that is