coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Where is downloadable Coq documentation?

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Where is downloadable Coq documentation?
Date: Sun, 24 Dec 2017 09:48:02 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-io0-f169.google.com
Ironport-phdr: 9a23:Tipe3RIsxje5TCnhY9mcpTZWNBhigK39O0sv0rFitYgRLvTxwZ3uMQTl6Ol3ixeRBMOHs6sC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffxhEiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhyUJNzA5/m/ZidF+grxHrx+6vRNz35TZbZuJOPZifK7Qe84RS2pbXsZWUixMGoyzYJESAOoAOOZTsoryqEEKrRu/GwmjHv7kxzhWhn73x6I61+UhER/c0wE7A90OtWnUoM/rO6gPTOC41a/FxijNYfNR3Dfy8onIchY5rPGNW7Jwa8vRxlM1GwPLlFWcsYPlPzKJ1uQNrmiU9PBsWv6oi24irQx6vzuhxt80h4XXmo4YzkrI+CZ5zYovO9G0VkB2bcS5HJZRsyyXMZZ9TNk4TGFyoik6z6ULuZ6lcygOz5Qq3xvfZOaGc4iM+x7jVeGRLSthiHJrZb6yhhK//VKvyu37Ucm031JKoTRfntbQsXAN0gTf6smBSvRj4keswSiD2xzX5+1eIk05lbDXJ4A/zrM+jJYfrEXOEyvulEXzlqCWd0Ek+uay6+TgZ7XrvoGcOJVphQH/N6QigM2+Dv48MggPQWiU4/+x1bP98k3iXLVGlOE5kqzEsJzAO8sUu7O5DxdP0ok/8xa/Eyum0NMAkHYbK1JFYQuLgJTtO1HTO//1Fuy/glSpkDdz3f/KJLzhApPXLnjCirjtZ7h961QPgDY0mNtY/tdfDqwLCPP1QE748tLCXTEjNAnh/e/rCdA15IoaWHyGSvuHIqrWsEGBzukqPq+BaJJD62W1EOQs+/O71SxxolQaZ6T8hZY=

There is also a related bug https://github.com/coq/coq/issues/4855 (about HTML docs).

CMU ECE PhD candidate

Mobile/WhatsApp: +1(510)220-1060

On Sun, Dec 24, 2017 at 8:22 AM, Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

That's an overlook on my part when publishing the 8.7.1 release. Now fixed.

It should be possible to generate a PDF of the standard library documentation as well, although it is not something that was done until now. As for an HTML version of the documentation you can cache, I'm not sure exactly what you mean or how to achieve this.

Ideally, I suppose the documentation should just be shipped with all Coq packages.

Cheers,
Théo

Le dim. 24 déc. 2017 à 15:41, Ramsdell, John D. <ramsdell AT mitre.org> a écrit :
There are times I use Coq without an Internet connection.
Where do I obtain a PDF of the reference manual? It's not
on the release page as suggested by https://coq.inria.fr/documentation.

It also be nice to a PDF of the standard library, and if it's not too much
trouble, HTML versions of the documentation I can cache locally.

John

[Coq-Club] Where is downloadable Coq documentation?, Ramsdell, John D., 12/24/2017
- Re: [Coq-Club] Where is downloadable Coq documentation?, Théo Zimmermann, 12/24/2017
  - Re: [Coq-Club] Where is downloadable Coq documentation?, Vadim Zaliva, 12/24/2017