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

`.. bibliography::` puts the bibliography on its own page with its own title in
LaTeX, but includes it inline without a title in HTML [1], so we need to
maintain two separate copies of zebibliography.rst

[1] https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends

Author: cpitclaudel

.gitignore

@@ -100,6 +100,7 @@ doc/faq/axioms.eps_t
 doc/faq/axioms.pdf_t
 doc/faq/axioms.png
 doc/sphinx/index.rst
+doc/sphinx/zebibliography.rst
 doc/stdlib/Library.out
 doc/stdlib/Library.ps
 doc/stdlib/Library.coqdoc.tex

doc/sphinx/conf.py

@@ -66,26 +66,34 @@
 # The encoding of source files.
 #source_encoding = 'utf-8-sig'
 
+import logging
+from glob import glob
 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():
+
+SUPPORTED_FORMATS = ["html", "latex"]
+
+def current_format(app):
+    for fmt in SUPPORTED_FORMATS:
         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())))
+            return fmt
+    MSG = """Unexpected builder ({}); expected one of {!r}.
+Add support for this new builder in `copy_formatspecific_files` in conf.py."""
+    from sphinx.errors import ConfigError
+    raise ConfigError(MSG.format(list(app.tags.tags.keys()), SUPPORTED_FORMATS))
+
+def copy_formatspecific_files(app):
+    ext = ".{}.rst".format(current_format(app))
+    for fname in sorted(os.listdir(app.srcdir)):
+        if fname.endswith(ext):
+            src = os.path.join(app.srcdir, fname)
+            dst = os.path.join(app.srcdir, fname[:-len(ext)] + ".rst")
+            app.info("Copying {} to {}".format(src, dst))
+            copyfile(src, dst)
 
 def setup(app):
-    app.connect('builder-inited', copy_master_doc)
+    app.connect('builder-inited', copy_formatspecific_files)
 
 # The master toctree document.
 # We create this file in `copy_master_doc` above.
@@ -126,11 +134,10 @@ def setup(app):
     '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'
-]
+] + ["*.{}.rst".format(fmt) for fmt in SUPPORTED_FORMATS]
 
 # The reST default role (used for this markup: `text`) to use for all
 # documents.

doc/sphinx/index-html.rst renamed to doc/sphinx/index.html.rst

@@ -77,5 +77,5 @@ Addendum
    addendum/miscellaneous-extensions
    addendum/universe-polymorphism
 
-..  No need for an explicit bibliography entry in the toc: it gets picked up
-    from ``zebibliography.rst``.
+.. toctree::
+   zebibliography

doc/sphinx/index-latex.rst renamed to doc/sphinx/index.latex.rst

@@ -0,0 +1,6 @@
+.. See zebibliography.html.rst for details
+
+.. _bibliography:
+
+.. bibliography:: biblio.bib
+   :cited: