aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/README.md12
-rw-r--r--doc/sphinx/changes.rst10
-rwxr-xr-xdoc/sphinx/conf.py12
-rw-r--r--doc/sphinx/dune2
4 files changed, 23 insertions, 13 deletions
diff --git a/doc/README.md b/doc/README.md
index 8e1bc85c49..99d285320d 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -28,9 +28,10 @@ Dependencies
To produce the complete documentation in HTML, you will need Coq dependencies
listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based
-reference manual requires Python 3, and the following Python packages:
+reference manual requires Python 3, and the following Python packages
+(note the version constraints on Sphinx):
- - sphinx >= 2.3.1
+ - sphinx >= 2.3.1 & < 3.0.0
- sphinx_rtd_theme >= 0.4.3
- beautifulsoup4 >= 4.0.6
- antlr4-python3-runtime >= 4.7.1
@@ -40,8 +41,8 @@ reference manual requires Python 3, and the following Python packages:
To install them, you should first install pip and setuptools (for instance,
with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run:
- pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime \
- pexpect sphinxcontrib-bibtex
+ pip3 install sphinx==2.3.1 sphinx_rtd_theme beautifulsoup4 \
+ antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex
Nix users should get the correct development environment to build the
HTML documentation from Coq's [`default.nix`](../default.nix) (note this
@@ -58,7 +59,6 @@ additional tools are required:
- makeindex
- xelatex
- latexmk
- - xindy
All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu,
install them with:
@@ -68,7 +68,7 @@ install them with:
Or if you want to use less disk space:
apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \
- latexmk xindy fonts-freefont-otf
+ latexmk fonts-freefont-otf
Compilation
-----------
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 6242833cda..0f2fce522a 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -980,8 +980,14 @@ Infrastructure and dependencies
- **Changed:**
Minimal versions of dependencies for building the reference manual:
- now requires Sphinx 2.3.1+, sphinx_rtd_theme 0.4.3+ and
- sphinxcontrib-bibtex 0.4.2+
+ now requires Sphinx >= 2.3.1 & < 3.0.0, sphinx_rtd_theme 0.4.3+ and
+ sphinxcontrib-bibtex 0.4.2+.
+
+ .. warning::
+
+ The reference manual is known not to build properly with
+ Sphinx 3.
+
(`#12224 <https://github.com/coq/coq/pull/12224>`_,
by Jim Fehrle and Théo Zimmermann).
- **Removed:**
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index fabf7a519f..99762c7a0e 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -214,11 +214,12 @@ html_context = {
'conf_py_path': '/doc/sphinx/',
# Versions and downloads listed in the versions menu (see _templates/versions.html)
'versions': [
- ("master", "https://coq.github.io/doc/master/refman/"),
+ ("dev", "https://coq.github.io/doc/master/refman/"),
("stable", "https://coq.inria.fr/distrib/current/refman/"),
- ("v8.11", "https://coq.github.io/doc/v8.11/refman/"),
- ("v8.10", "https://coq.github.io/doc/v8.10/refman/"),
- ("v8.9", "https://coq.github.io/doc/v8.9/refman/"),
+ ("v8.12", "https://coq.github.io/doc/v8.12/refman/"),
+ ("8.11", "https://coq.inria.fr/distrib/V8.11.2/refman/"),
+ ("8.10", "https://coq.inria.fr/distrib/V8.10.2/refman/"),
+ ("8.9", "https://coq.inria.fr/distrib/V8.9.1/refman/"),
("8.8", "https://coq.inria.fr/distrib/V8.8.2/refman/"),
("8.7", "https://coq.inria.fr/distrib/V8.7.2/refman/"),
("8.6", "https://coq.inria.fr/distrib/V8.6.1/refman/"),
@@ -356,6 +357,9 @@ latex_elements = {
latex_engine = "xelatex"
+# Cf. https://github.com/sphinx-doc/sphinx/issues/7015
+latex_use_xindy = False
+
########
# done #
########
diff --git a/doc/sphinx/dune b/doc/sphinx/dune
index b788fbbeed..31f28635fe 100644
--- a/doc/sphinx/dune
+++ b/doc/sphinx/dune
@@ -1,4 +1,4 @@
-(dirs :standard _static)
+(dirs :standard _static _templates)
(rule
(targets README.gen.rst)