The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Clément,

Thanks for your answer. If that's not something that would be too demanding, I think it would be great to be able to continue to provide a single page PDF document for the manual. For instance, for embedding in future Zenodo biblio entries: like it was the case for 8.7 (https://zenodo.org/record/1174360).

The rendering of the PDF you shared is great. While browsing I noticed a small issue though: in section "4.2.3 Advanced recursive functions", there's a blank Coq block. I checked the HTML version and the Coq block is not blank there.

Thanks,

Théo

Le ven. 11 mai 2018 à 00:32, Clément Pit-Claudel <cpitclaudel AT gmail.com> a écrit :

Hi Michael and Théo,

> Or maybe the installer should install the documentation, if it consists out of many files.

I think we should be able to ask Sphinx for a one-page copy of the manual, which should be easy to download.

> There won't be a pdf manual for Coq 8.8.0. If you think it is unfortunate, please open a new issue: so far the lack of clear use cases has not permitted to motivate anyone to work on the additional infrastructure that this would require.

The original prototype I wrote was supposed to allow building PDFs, but indeed the version that's in the repo currently can't build a valid PDF.  There are very few blocking issues, though (maybe 3-5 LaTeX mistakes and a few reST issues).  I've uploaded a copy of the manual generated by Sphinx after fixing these errors to https://people.csail.mit.edu/cpitcla/coq-8.8.pdf (2.2MB a bit too heavy to attach).  There are still presentation issues, but if there is interest in a PDF manual they should not be difficult to fix.

Building a LaTeX copy of the manual would give us a good way to check the correctness of embedded math, by the way.

Cheers,
Clément.

On 2018-05-10 13:45, Théo Zimmermann wrote:
> Indeed, it would be great to have the Windows installer ship the documentation. The new Python dependencies of the manual should be easier to install on Windows. So far the AppVeyor infrastructure used to build the installer has been very close to timeout and adding the doc to it would be probably too much, but the move to GitLab CI should solve this by allowing longer timeouts.
>
> Best,
> Théo
>
> Le jeu. 10 mai 2018 à 19:34, Soegtrop, Michael <michael.soegtrop AT intel.com <mailto:michael.soegtrop AT intel.com>> a écrit :
>
>     Dear Théo,____
>
>     __ __
>
>     It is ok – the new format is indeed easier to read. Just it would be nice to have an easy way to download it. Or maybe the installer should install the documentation, if it consists out of many files. I sometimes do Coq in places with bad network infrastructure.____
>
>     __ __
>
>     I can take care of this for Windows.____
>
>     __ __
>
>     Best regards,____
>
>     __ __
>
>     Michael____
>
>     __ __
>
>     *From:*coq-club-request AT inria.fr <mailto:coq-club-request AT inria.fr> [mailto:coq-club-request AT inria.fr <mailto:coq-club-request AT inria.fr>] *On Behalf Of *Théo Zimmermann
>     *Sent:* Thursday, May 10, 2018 5:36 PM
>     *To:* coq-club AT inria.fr <mailto:coq-club AT inria.fr>
>     *Subject:* Re: [Coq-Club] Will there be a pdf manual for 8.8.0?____
>
>     __ __
>
>     Dear Michael,____
>
>     There won't be a pdf manual for Coq 8.8.0. If you think it is unfortunate, please open a new issue: so far the lack of clear use cases has not permitted to motivate anyone to work on the additional infrastructure that this would require.____
>
>     The problem of the wrong mention on the website had indeed been reported a couple times already and should now be fixed.____
>
>     Thanks,____
>
>     Théo____
>
>     __ __
>
>     Le jeu. 10 mai 2018 à 13:49, Soegtrop, Michael <michael.soegtrop AT intel.com <mailto:michael.soegtrop AT intel.com>> a écrit :____
>
>         Dear Coq Team,____
>
>          ____
>
>         I wonder if there are plans to publish a pdf manual for Coq 8.8.0 and future versions, or if this was dropped in favor of the new documentation format.____
>
>          ____
>
>         A note: this page: https://coq.inria.fr/documentation states that a PDF version can be downloaded from the release page https://github.com/coq/coq/releases/tag/V8.8.0 , but this doesn’t seem to be the case.____
>
>          ____
>
>         Best regards,____
>
>          ____
>
>         Michael____
>
>          ____
>
>         Intel Deutschland GmbH
>         Registered Address: Am Campeon 10 <https://maps.google.com/?q=Am+Campeon+10&entry=gmail&source=g>-12, 85579 Neubiberg, Germany
>         Tel: +49 89 99 8853-0, www.intel.de <http://www.intel.de>
>         Managing Directors: Christin Eisenschmid, Christian Lamprechter
>         Chairperson of the Supervisory Board: Nicole Lau
>         Registered Office: Munich
>         Commercial Register: Amtsgericht Muenchen HRB 186928____
>
>     Intel Deutschland GmbH
>     Registered Address: Am Campeon 10 <https://maps.google.com/?q=Am+Campeon+10&entry=gmail&source=g>-12, 85579 Neubiberg, Germany
>     Tel: +49 89 99 8853-0, www.intel.de <http://www.intel.de>
>     Managing Directors: Christin Eisenschmid, Christian Lamprechter
>     Chairperson of the Supervisory Board: Nicole Lau
>     Registered Office: Munich
>     Commercial Register: Amtsgericht Muenchen HRB 186928
>