From ce078ca30d79455cc2a7055f9e989f7b83a5cd56 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 22 Jun 2018 09:06:57 +0200 Subject: Improve doc/README.md. - Fix the Markdown. - Add link to latest build of the refman for the master branch. - Clarify what are the dependencies of the HTML doc. [ci skip] --- doc/README.md | 76 ++++++++++++++++++++++++++++++++++------------------------- 1 file changed, 44 insertions(+), 32 deletions(-) (limited to 'doc') diff --git a/doc/README.md b/doc/README.md index c47f9f48a..416726e1b 100644 --- a/doc/README.md +++ b/doc/README.md @@ -1,13 +1,20 @@ - The Coq documentation - ===================== +The Coq documentation +===================== The Coq documentation includes - A Reference Manual - A document presenting the Coq standard library +The documentation of the latest released version is available on the Coq +web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). + +Additionnally, you can view the documentation for the current master version at +. + The reference manual is written is reStructuredText and compiled -using Sphinx (see `doc/sphinx/README.rst`) to learn more. +using Sphinx (see [`sphinx/README.rst`](/doc/sphinx/README.rst)) +to learn more about the format that is used. The documentation for the standard library is generated from the `.v` source files using coqdoc. @@ -15,12 +22,8 @@ the `.v` source files using coqdoc. Prerequisite ------------ -To produce all the documents, the following tools are needed: +To produce the complete documentation in HTML, the following tools are required: - - latex (latex2e) - - pdflatex - - dvips - - makeindex - Python 3 - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/) - sphinx_rtd_theme @@ -28,56 +31,64 @@ To produce all the documents, the following tools are needed: - beautifulsoup4 - Antlr4 runtime for Python 3 +To produce the documentation in PDF and PostScript formats the following +additional tools are required: + + - latex (latex2e) + - pdflatex + - dvips + - makeindex Under recent Debian based operating systems (Debian 10 "Buster", Ubuntu 18.04, ...) a working set of packages for compiling the documentation for Coq is: - texlive-latex-extra texlive-fonts-recommended python3-sphinx - python3-pexpect python3-sphinx-rtd-theme python3-bs4 - python3-sphinxcontrib.bibtex python3-pip + texlive-latex-extra texlive-fonts-recommended + python3-sphinx python3-pexpect python3-sphinx-rtd-theme + python3-bs4 python3-sphinxcontrib.bibtex python3-pip Then, install the Python3 Antlr4 package: - pip3 install antlr4-python3-runtime + pip3 install antlr4-python3-runtime Nix users should get the correct development environment to build the -HTML documentation from Coq's `default.nix`. [Note Nix setup doesn't -include the LaTeX packages needed to build the full documentation.] +HTML documentation from Coq's [`default.nix`](/default.nix) (note this +doesn't include the LaTeX packages needed to build the full documentation). -If you are in an older/different distribution you can install the -Python packages required to build the user manual using python3-pip: +If you are in an older / different distribution / operating system, you can +install the Python packages required to build the reference manual using +python3-pip: - pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex + pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex Compilation ----------- To produce all documentation about Coq, just run: - ./configure (if you hadn't already) - make doc + ./configure # (if you hadn't already) + make doc Alternatively, you can use some specific targets: - make doc-ps - to produce all PostScript documents +- `make doc-ps` + to produce all PostScript documents - make doc-pdf - to produce all PDF documents +- `make doc-pdf` + to produce all PDF documents - make doc-html - to produce all html documents +- `make doc-html` + to produce all HTML documents - make sphinx - to produce the HTML version of the reference manual +- `make sphinx` + to produce the HTML version of the reference manual - make stdlib - to produce all formats of the Coq standard library +- `make stdlib` + to produce all formats of the Coq standard library -Also note the "-with-doc yes" option of ./configure to enable the +Also note the `-with-doc yes` option of `./configure` to enable the build of the documentation as part of the default make target. @@ -86,6 +97,7 @@ Installation To install all produced documents, do: - make DOCDIR=/some/directory/for/documentation install-doc + make DOCDIR=/some/directory/for/documentation install-doc -DOCDIR defaults to /usr/share/doc/coq +`DOCDIR` defaults to `/usr/share/doc/coq` or whatever value was specificied +through the `-docdir` option of `./configure`. -- cgit v1.2.3