[doc] Create a separate index file for the LaTeX build

See https://github.com/sphinx-doc/sphinx/issues/4977 for context.

7 files changed, 134 insertions, 36 deletions

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index a213791504..7b742c680e 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -66,8 +66,30 @@ source_suffix = '.rst'
 # The encoding of source files.
 #source_encoding = 'utf-8-sig'
 
+from shutil import copyfile
+
+SUPPORTED_FORMATS = { fmt: os.path.abspath("index-{}.rst".format(fmt))
+                      for fmt in ["html", "latex"] }
+MASTER_DOC = os.path.abspath("index.rst")
+
+# Add extra cases here to support more formats
+def copy_master_doc(app):
+    for fmt, rst_path in SUPPORTED_FORMATS.items():
+        if app.tags.has(fmt):
+            copyfile(rst_path, MASTER_DOC)
+            break
+    else:
+        MSG = """Unexpected builder; expected one of {!r}.
+Add support for this new builder in `copy_master_doc` in conf.py."""
+        from sphinx.errors import ConfigError
+        raise ConfigError(MSG.format(list(SUPPORTED_FORMATS.keys())))
+
+def setup(app):
+    app.connect('builder-inited', copy_master_doc)
+
 # The master toctree document.
-master_doc = 'index'
+# We create this file in `copy_master_doc` above.
+master_doc = "index"
 
 # General information about the project.
 project = 'Coq'
@@ -104,6 +126,8 @@ exclude_patterns = [
     'Thumbs.db',
     '.DS_Store',
     'introduction.rst',
+    'index-*.rst', # One of these gets copied to index.rst in `copy_master_doc`
+    'refman-preamble.rst',
     'README.rst',
     'README.template.rst'
 ]
@@ -267,12 +291,12 @@ latex_elements = {
     'papersize': 'letterpaper',
     'classoptions': ',openany', # No blank pages
     'polyglossia' : '\\usepackage{polyglossia}',
-    'microtype' : '\\usepackage{microtype}',
     "preamble": r"""
                  \usepackage{unicode-math}
+                 \usepackage{microtype}
 
                  % Macro definitions
-                 \input{preamble.tex}
+                 \usepackage{refman-preamble}
 
                  % Style definitions for notations
                  \usepackage{coqnotations}
@@ -286,21 +310,15 @@ latex_engine = "xelatex"
 ########
 
 latex_additional_files = [
-    "preamble.tex",
+    "refman-preamble.sty",
     "_static/coqnotations.sty"
 ]
 
-# Grouping the document tree into LaTeX files. List of tuples
-# (source start file, target name, title,
-#  author, documentclass [howto, manual, or own class]).
-latex_documents = [
-   (master_doc, 'CoqRefMan.tex', 'Coq Documentation',
-    'The Coq Development Team', 'manual'),
-]
+latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')]
 
 # The name of an image file (relative to this directory) to place at the top of
 # the title page.
-latex_logo = "../../ide/coq.png"
+# latex_logo = "../../ide/coq.png"
 
 # If true, show page references after internal links.
 #latex_show_pagerefs = False
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index be0b5d5f12..62851039bf 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1,12 +1,5 @@
-.. include:: preamble.rst
-.. include:: replaces.rst
-
 .. _credits:
 
--------------------------------------------
-Credits
--------------------------------------------
-
 Coq is a proof assistant for higher-order logic, allowing the
 development of computer programs consistent with their formal
 specification. It is the result of about ten years of research of the
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index-html.rst
index baf2e0d981..b96a01f76d 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index-html.rst
@@ -1,11 +1,16 @@
-.. include:: preamble.rst
-.. include:: replaces.rst
+==========================
+ The Coq Reference Manual
+==========================
+
+.. _introduction:
+
+Introduction
+------------
 
 .. include:: introduction.rst
 
-------------------
 Table of contents
-------------------
+-----------------
 
 .. toctree::
    :caption: Indexes
@@ -80,12 +85,12 @@ Table of contents
 
    zebibliography
 
-This material (the Coq Reference Manual) may be distributed only subject to the
-terms and conditions set forth in the Open Publication License, v1.0 or later
-(the latest version is presently available at
-http://www.opencontent.org/openpub). Options A and B are not elected.
+License
+-------
+
+.. include:: license.rst
 
 .. [#PG] Proof-General is available at https://proofgeneral.github.io/.
-         Optionally, you can enhance it with the minor mode
-         Company-Coq :cite:`Pit16`
-         (see https://github.com/cpitclaudel/company-coq).
+   Optionally, you can enhance it with the minor mode
+   Company-Coq :cite:`Pit16`
+   (see https://github.com/cpitclaudel/company-coq).
diff --git a/doc/sphinx/index-latex.rst b/doc/sphinx/index-latex.rst
new file mode 100644
index 0000000000..e139b22a48
--- /dev/null
+++ b/doc/sphinx/index-latex.rst
@@ -0,0 +1,81 @@
+==========================
+ The Coq Reference Manual
+==========================
+
+Introduction
+------------
+
+.. include:: introduction.rst
+
+Credits
+-------
+
+.. include:: credits.rst
+
+License
+-------
+
+.. include:: license.rst
+
+The language
+------------
+
+.. toctree::
+
+   language/gallina-specification-language
+   language/gallina-extensions
+   language/coq-library
+   language/cic
+   language/module-system
+
+The proof engine
+----------------
+
+.. toctree::
+
+   proof-engine/vernacular-commands
+   proof-engine/proof-handling
+   proof-engine/tactics
+   proof-engine/ltac
+   proof-engine/detailed-tactic-examples
+   proof-engine/ssreflect-proof-language
+
+User extensions
+---------------
+
+.. toctree::
+
+   user-extensions/syntax-extensions
+   user-extensions/proof-schemes
+
+Practical tools
+---------------
+
+.. toctree::
+
+   practical-tools/coq-commands
+   practical-tools/utilities
+   practical-tools/coqide
+
+Addendum
+--------
+
+.. toctree::
+
+   addendum/extended-pattern-matching
+   addendum/implicit-coercions
+   addendum/canonical-structures
+   addendum/type-classes
+   addendum/omega
+   addendum/micromega
+   addendum/extraction
+   addendum/program
+   addendum/ring
+   addendum/nsatz
+   addendum/generalized-rewriting
+   addendum/parallel-proof-processing
+   addendum/miscellaneous-extensions
+   addendum/universe-polymorphism
+
+..  No need for an explicit bibliography entry in the toc: it gets picked up
+    from ``zebibliography.rst``.
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index b57e4b209c..797a9a9714 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -1,8 +1,5 @@
-.. _introduction:
-
-------------------------
-Introduction
-------------------------
+.. include:: preamble.rst
+.. include:: replaces.rst
 
 This document is the Reference Manual of the |Coq| proof assistant.
 To start using Coq, it is advised to first read a tutorial.
diff --git a/doc/sphinx/license.rst b/doc/sphinx/license.rst
new file mode 100644
index 0000000000..232b04211c
--- /dev/null
+++ b/doc/sphinx/license.rst
@@ -0,0 +1,4 @@
+This material (the Coq Reference Manual) may be distributed only subject to the
+terms and conditions set forth in the Open Publication License, v1.0 or later
+(the latest version is presently available at
+http://www.opencontent.org/openpub). Options A and B are not elected.
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index b3641c152b..5834ddaa4f 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -620,12 +620,12 @@ class PreambleDirective(Directive):
 
        .. preamble:: preamble.tex
     """
-
     has_content = False
     required_arguments = 1
     optional_arguments = 0
     final_argument_whitespace = True
     option_spec = {}
+    directive_name = "preamble"
 
     def run(self):
         document = self.state.document