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

2 files changed, 104 insertions, 2 deletions

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.