From 7eced434fb9ceafc2d6e248aa5e49bbd6cd2e1fa Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Mon, 13 Aug 2018 18:27:20 -0400 Subject: [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 --- .gitignore | 1 + doc/sphinx/conf.py | 39 ++++++++------- doc/sphinx/index-html.rst | 96 ------------------------------------- doc/sphinx/index-latex.rst | 81 ------------------------------- doc/sphinx/index.html.rst | 96 +++++++++++++++++++++++++++++++++++++ doc/sphinx/index.latex.rst | 81 +++++++++++++++++++++++++++++++ doc/sphinx/zebibliography.html.rst | 17 +++++++ doc/sphinx/zebibliography.latex.rst | 6 +++ doc/sphinx/zebibliography.rst | 17 ------- 9 files changed, 224 insertions(+), 210 deletions(-) delete mode 100644 doc/sphinx/index-html.rst delete mode 100644 doc/sphinx/index-latex.rst create mode 100644 doc/sphinx/index.html.rst create mode 100644 doc/sphinx/index.latex.rst create mode 100644 doc/sphinx/zebibliography.html.rst create mode 100644 doc/sphinx/zebibliography.latex.rst delete mode 100644 doc/sphinx/zebibliography.rst diff --git a/.gitignore b/.gitignore index 8c5d8bcc16..d52898b3a5 100644 --- a/.gitignore +++ b/.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 diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 7b742c680e..96cff735f5 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -66,26 +66,34 @@ source_suffix = '.rst' # 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 @@ 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' -] +] + ["*.{}.rst".format(fmt) for fmt in SUPPORTED_FORMATS] # The reST default role (used for this markup: `text`) to use for all # documents. diff --git a/doc/sphinx/index-html.rst b/doc/sphinx/index-html.rst deleted file mode 100644 index b96a01f76d..0000000000 --- a/doc/sphinx/index-html.rst +++ /dev/null @@ -1,96 +0,0 @@ -========================== - The Coq Reference Manual -========================== - -.. _introduction: - -Introduction ------------- - -.. include:: introduction.rst - -Table of contents ------------------ - -.. toctree:: - :caption: Indexes - - genindex - coq-cmdindex - coq-tacindex - coq-optindex - coq-exnindex - -.. No entries yet - * :index:`thmindex` - -.. toctree:: - :caption: Preamble - - self - credits - -.. toctree:: - :caption: The language - - language/gallina-specification-language - language/gallina-extensions - language/coq-library - language/cic - language/module-system - -.. toctree:: - :caption: The proof engine - - proof-engine/vernacular-commands - proof-engine/proof-handling - proof-engine/tactics - proof-engine/ltac - proof-engine/detailed-tactic-examples - proof-engine/ssreflect-proof-language - -.. toctree:: - :caption: User extensions - - user-extensions/syntax-extensions - user-extensions/proof-schemes - -.. toctree:: - :caption: Practical tools - - practical-tools/coq-commands - practical-tools/utilities - practical-tools/coqide - -.. toctree:: - :caption: Addendum - - 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 - -.. toctree:: - :caption: Reference - - zebibliography - -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). diff --git a/doc/sphinx/index-latex.rst b/doc/sphinx/index-latex.rst deleted file mode 100644 index e139b22a48..0000000000 --- a/doc/sphinx/index-latex.rst +++ /dev/null @@ -1,81 +0,0 @@ -========================== - 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/index.html.rst b/doc/sphinx/index.html.rst new file mode 100644 index 0000000000..b96a01f76d --- /dev/null +++ b/doc/sphinx/index.html.rst @@ -0,0 +1,96 @@ +========================== + The Coq Reference Manual +========================== + +.. _introduction: + +Introduction +------------ + +.. include:: introduction.rst + +Table of contents +----------------- + +.. toctree:: + :caption: Indexes + + genindex + coq-cmdindex + coq-tacindex + coq-optindex + coq-exnindex + +.. No entries yet + * :index:`thmindex` + +.. toctree:: + :caption: Preamble + + self + credits + +.. toctree:: + :caption: The language + + language/gallina-specification-language + language/gallina-extensions + language/coq-library + language/cic + language/module-system + +.. toctree:: + :caption: The proof engine + + proof-engine/vernacular-commands + proof-engine/proof-handling + proof-engine/tactics + proof-engine/ltac + proof-engine/detailed-tactic-examples + proof-engine/ssreflect-proof-language + +.. toctree:: + :caption: User extensions + + user-extensions/syntax-extensions + user-extensions/proof-schemes + +.. toctree:: + :caption: Practical tools + + practical-tools/coq-commands + practical-tools/utilities + practical-tools/coqide + +.. toctree:: + :caption: Addendum + + 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 + +.. toctree:: + :caption: Reference + + zebibliography + +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). diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst new file mode 100644 index 0000000000..13bc1a19e7 --- /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 + +.. toctree:: + zebibliography diff --git a/doc/sphinx/zebibliography.html.rst b/doc/sphinx/zebibliography.html.rst new file mode 100644 index 0000000000..756edd5482 --- /dev/null +++ b/doc/sphinx/zebibliography.html.rst @@ -0,0 +1,17 @@ +.. There are multiple issues with sphinxcontrib-bibtex that we have to work around: + - The list of cited entries is computed right after encountering + `.. bibliography`, so the file containing that command has to come last + alphabetically: + https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#unresolved-citations-across-documents + - `.. bibliography::` puts the bibliography on its own page with its own + title in LaTeX, but includes it inline without a title in HTML: + https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends + +.. _bibliography: + +============== + Bibliography +============== + +.. bibliography:: biblio.bib + :cited: diff --git a/doc/sphinx/zebibliography.latex.rst b/doc/sphinx/zebibliography.latex.rst new file mode 100644 index 0000000000..2c0396f1c9 --- /dev/null +++ b/doc/sphinx/zebibliography.latex.rst @@ -0,0 +1,6 @@ +.. See zebibliography.html.rst for details + +.. _bibliography: + +.. bibliography:: biblio.bib + :cited: diff --git a/doc/sphinx/zebibliography.rst b/doc/sphinx/zebibliography.rst deleted file mode 100644 index 756edd5482..0000000000 --- a/doc/sphinx/zebibliography.rst +++ /dev/null @@ -1,17 +0,0 @@ -.. There are multiple issues with sphinxcontrib-bibtex that we have to work around: - - The list of cited entries is computed right after encountering - `.. bibliography`, so the file containing that command has to come last - alphabetically: - https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#unresolved-citations-across-documents - - `.. bibliography::` puts the bibliography on its own page with its own - title in LaTeX, but includes it inline without a title in HTML: - https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends - -.. _bibliography: - -============== - Bibliography -============== - -.. bibliography:: biblio.bib - :cited: -- cgit v1.2.3