1 files changed, 91 insertions, 0 deletions
diff --git a/doc/README.md b/doc/README.md
new file mode 100644
index 000000000..c47f9f48a
--- /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