Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.

5 files changed, 111 insertions, 100 deletions

diff --git a/INSTALL.doc b/INSTALL.doc
deleted file mode 100644
index 13e6440d0..000000000
--- 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 0903abdd4..df4ca8e40 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/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 508dcf5fb..a59afb8f6 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
 }
 
diff --git a/doc/LICENSE b/doc/LICENSE
index c9f574afb..3789d9104 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
@@ -18,7 +18,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. 
 
diff --git a/doc/README.md b/doc/README.md
new file mode 100644
index 000000000..6c6e1f01f
--- /dev/null
+++ b/doc/README.md
@@ -0,0 +1,102 @@
+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
+<https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=documentation>.
+
+The reference manual is written is reStructuredText and compiled
+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.
+
+Dependencies
+------------
+
+### HTML documentation
+
+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:
+
+    sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex
+
+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:
+
+    apt install python3-sphinx python3-pexpect python3-sphinx-rtd-theme \
+                python3-bs4 python3-sphinxcontrib.bibtex python3-pip
+
+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
+doesn't include the LaTeX packages needed to build the full documentation).
+
+### 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:
+
+    apt install texlive-latex-extra texlive-fonts-recommended
+
+Compilation
+-----------
+
+To produce all documentation about Coq in all formats, 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 install-doc
+
+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.