The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

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
>