From 1844f4f31276227d6a4d512f1220e83373ea9498 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 22 Jun 2018 09:06:52 +0200 Subject: Move INSTALL.doc into doc/README.md. This will avoid in particular this ambiguous file extension. [ci skip] --- INSTALL.doc | 91 ----------------------------------------------------------- README.md | 4 ++- doc/README.md | 91 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 94 insertions(+), 92 deletions(-) delete mode 100644 INSTALL.doc create mode 100644 doc/README.md diff --git a/INSTALL.doc b/INSTALL.doc deleted file mode 100644 index 13e6440d01..0000000000 --- a/INSTALL.doc +++ /dev/null @@ -1,91 +0,0 @@ - The Coq documentation - ===================== - -The Coq documentation includes - -- A Reference Manual -- A document presenting the Coq standard library - -The reference manual is written is reStructuredText and compiled -using Sphinx (see `doc/sphinx/README.rst`) to learn more. - -The documentation for the standard library is generated from -the `.v` source files using coqdoc. - -Prerequisite ------------- - -To produce all the documents, the following tools are needed: - - - latex (latex2e) - - pdflatex - - dvips - - makeindex - - Python 3 - - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/) - - sphinx_rtd_theme - - pexpect - - beautifulsoup4 - - Antlr4 runtime for Python 3 - - -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 - -Then, install the Python3 Antlr4 package: - - 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.] - -If you are in an older/different distribution you can install the -Python packages required to build the user manual using python3-pip: - - 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 - - -Alternatively, you can use some specific targets: - - make doc-ps - to produce all PostScript documents - - make doc-pdf - to produce all PDF documents - - make doc-html - to produce all html documents - - make sphinx - to produce the HTML version of the reference manual - - make stdlib - to produce all formats of the Coq standard library - - -Also note the "-with-doc yes" option of ./configure to enable the -build of the documentation as part of the default make target. - - -Installation ------------- - -To install all produced documents, do: - - make DOCDIR=/some/directory/for/documentation install-doc - -DOCDIR defaults to /usr/share/doc/coq diff --git a/README.md b/README.md index 0903abdd41..df4ca8e407 100644 --- a/README.md +++ b/README.md @@ -18,7 +18,9 @@ or refer to the [`INSTALL` file](INSTALL) for the procedure to install from sour ## Documentation -The sources of the documentation can be found in directory [`doc`](doc). The +The sources of the documentation can be found in directory [`doc`](doc). +See [`doc/README.md`](/doc/README.md) to learn more about the documentation, +in particular how to build it. The documentation of the last released version is available on the Coq web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). See also [Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki), diff --git a/doc/README.md b/doc/README.md new file mode 100644 index 0000000000..c47f9f48a3 --- /dev/null +++ b/doc/README.md @@ -0,0 +1,91 @@ + The Coq documentation + ===================== + +The Coq documentation includes + +- A Reference Manual +- A document presenting the Coq standard library + +The reference manual is written is reStructuredText and compiled +using Sphinx (see `doc/sphinx/README.rst`) to learn more. + +The documentation for the standard library is generated from +the `.v` source files using coqdoc. + +Prerequisite +------------ + +To produce all the documents, the following tools are needed: + + - latex (latex2e) + - pdflatex + - dvips + - makeindex + - Python 3 + - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/) + - sphinx_rtd_theme + - pexpect + - beautifulsoup4 + - Antlr4 runtime for Python 3 + + +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 + +Then, install the Python3 Antlr4 package: + + 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.] + +If you are in an older/different distribution you can install the +Python packages required to build the user manual using python3-pip: + + 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 + + +Alternatively, you can use some specific targets: + + make doc-ps + to produce all PostScript documents + + make doc-pdf + to produce all PDF documents + + make doc-html + to produce all html documents + + make sphinx + to produce the HTML version of the reference manual + + make stdlib + to produce all formats of the Coq standard library + + +Also note the "-with-doc yes" option of ./configure to enable the +build of the documentation as part of the default make target. + + +Installation +------------ + +To install all produced documents, do: + + make DOCDIR=/some/directory/for/documentation install-doc + +DOCDIR defaults to /usr/share/doc/coq -- cgit v1.2.3 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(-) diff --git a/doc/README.md b/doc/README.md index c47f9f48a3..416726e1ba 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 From ec9d8095ba74cc0549fe1eca950466742c43e74f Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 22 Jun 2018 09:06:57 +0200 Subject: Fix copyright dates in doc/LICENSE. [ci skip] --- doc/LICENSE | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/LICENSE b/doc/LICENSE index c223a4e16c..dcd8c49537 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -2,7 +2,7 @@ The Coq Reference Manual is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the LaTeX and BibTeX sources, the embedded png files, and the PostScript, PDF and html outputs) are -copyright (c) INRIA 1999-2006, with the exception of the Ubuntu font +copyright (c) INRIA 1999-2018, with the exception of the Ubuntu font file UbuntuMono-B.ttf, which is Copyright 2010,2011 Canonical Ltd and licensed under the Ubuntu font license, version 1.0 @@ -27,7 +27,7 @@ The Coq Standard Library is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the Coq vernacular source files and the PostScript, PDF and html outputs) are copyright (c) INRIA -1999-2006. The material connected to the Standard Library is +1999-2018. The material connected to the Standard Library is distributed under the terms of the Lesser General Public License version 2.1 or later. -- cgit v1.2.3 From 37e8149db7bfa2e7d7fe571b92752f6589101852 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 22 Jun 2018 09:06:57 +0200 Subject: Clarify further doc/README.md following Jim's comments. Relative links. Cf. #7800. --- doc/README.md | 63 +++++++++++++++++++++++++++++------------------------------ 1 file changed, 31 insertions(+), 32 deletions(-) diff --git a/doc/README.md b/doc/README.md index 416726e1ba..6c6e1f01fb 100644 --- a/doc/README.md +++ b/doc/README.md @@ -13,58 +13,56 @@ Additionnally, you can view the documentation for the current master version at . The reference manual is written is reStructuredText and compiled -using Sphinx (see [`sphinx/README.rst`](/doc/sphinx/README.rst)) +using Sphinx. See [`sphinx/README.rst`](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. -Prerequisite +Dependencies ------------ -To produce the complete documentation in HTML, the following tools are required: +### HTML documentation - - Python 3 - - Sphinx 1.6.5 (http://www.sphinx-doc.org/en/stable/) - - sphinx_rtd_theme - - pexpect - - beautifulsoup4 - - Antlr4 runtime for Python 3 +To produce the complete documentation in HTML, you will need Coq dependencies +listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based +reference manual requires Python 3, and the following Python packages: -To produce the documentation in PDF and PostScript formats the following -additional tools are required: + sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex - - 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: +You can install them using `pip3 install` or using your distribution's package +manager. E.g. under recent Debian-based operating systems (Debian 10 "Buster", +Ubuntu 18.04, ...) you can use: - texlive-latex-extra texlive-fonts-recommended - python3-sphinx python3-pexpect python3-sphinx-rtd-theme - python3-bs4 python3-sphinxcontrib.bibtex python3-pip + apt install python3-sphinx python3-pexpect python3-sphinx-rtd-theme \ + python3-bs4 python3-sphinxcontrib.bibtex python3-pip -Then, install the Python3 Antlr4 package: +Then, install the missing Python3 Antlr4 package: pip3 install antlr4-python3-runtime Nix users should get the correct development environment to build the -HTML documentation from Coq's [`default.nix`](/default.nix) (note this +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 / operating system, you can -install the Python packages required to build the reference manual using -python3-pip: +### Other formats + +To produce the documentation in PDF and PostScript formats, the following +additional tools are required: + + - latex (latex2e) + - pdflatex + - dvips + - makeindex + +Install them using your package manager. E.g. on Debian / Ubuntu: - pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex + apt install texlive-latex-extra texlive-fonts-recommended Compilation ----------- -To produce all documentation about Coq, just run: +To produce all documentation about Coq in all formats, just run: ./configure # (if you hadn't already) make doc @@ -97,7 +95,8 @@ Installation To install all produced documents, do: - make DOCDIR=/some/directory/for/documentation install-doc + make install-doc -`DOCDIR` defaults to `/usr/share/doc/coq` or whatever value was specificied -through the `-docdir` option of `./configure`. +This will install the documentation in `/usr/share/doc/coq` unless you +specify another value through the `-docdir` option of `./configure` or the +`DOCDIR` environment variable. -- cgit v1.2.3 From b89904c3831f1ddc02efb2998c71dcaa0df1d286 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 22 Jun 2018 09:06:58 +0200 Subject: Fix Windows install script following removal of INSTALL.ide and move of INSTALL.doc. --- dev/build/windows/makecoq_mingw.sh | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index 508dcf5fb0..a59afb8f66 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1128,14 +1128,12 @@ function copy_coq_license { install -D doc/LICENSE "$PREFIXCOQ/license_readme/coq/LicenseDoc.txt" install -D LICENSE "$PREFIXCOQ/license_readme/coq/License.txt" install -D plugins/micromega/LICENSE.sos "$PREFIXCOQ/license_readme/coq/LicenseMicromega.txt" - install -D README "$PREFIXCOQ/license_readme/coq/ReadMe.txt" || true - install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" || true - install -D README.win "$PREFIXCOQ/license_readme/coq/ReadMeWindows.txt" || true - install -D README.doc "$PREFIXCOQ/license_readme/coq/ReadMeDoc.txt" || true + # FIXME: this is not the micromega license + # It only applies to code that was copied into one single file! + install -D README.md "$PREFIXCOQ/license_readme/coq/ReadMe.md" install -D CHANGES "$PREFIXCOQ/license_readme/coq/Changes.txt" install -D INSTALL "$PREFIXCOQ/license_readme/coq/Install.txt" - install -D INSTALL.doc "$PREFIXCOQ/license_readme/coq/InstallDoc.txt" - install -D INSTALL.ide "$PREFIXCOQ/license_readme/coq/InstallIde.txt" + install -D doc/README.md "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" fi } -- cgit v1.2.3