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]

1 files changed, 44 insertions, 32 deletions

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
+<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 `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`.