From dc4fc036cd361fe0d2943039e75570cf08a90868 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Wed, 16 May 2018 21:22:01 -0400 Subject: [doc] Create a separate index file for the LaTeX build See https://github.com/sphinx-doc/sphinx/issues/4977 for context. --- .gitignore | 1 + doc/sphinx/conf.py | 42 +++++++++++++------ doc/sphinx/credits.rst | 7 ---- doc/sphinx/index-html.rst | 96 +++++++++++++++++++++++++++++++++++++++++++ doc/sphinx/index-latex.rst | 81 ++++++++++++++++++++++++++++++++++++ doc/sphinx/index.rst | 91 ---------------------------------------- doc/sphinx/introduction.rst | 7 +--- doc/sphinx/license.rst | 4 ++ doc/tools/coqrst/coqdomain.py | 2 +- 9 files changed, 215 insertions(+), 116 deletions(-) create mode 100644 doc/sphinx/index-html.rst create mode 100644 doc/sphinx/index-latex.rst delete mode 100644 doc/sphinx/index.rst create mode 100644 doc/sphinx/license.rst diff --git a/.gitignore b/.gitignore index 8fc3c802ad..8c5d8bcc16 100644 --- a/.gitignore +++ b/.gitignore @@ -99,6 +99,7 @@ doc/faq/axioms.eps doc/faq/axioms.eps_t doc/faq/axioms.pdf_t doc/faq/axioms.png +doc/sphinx/index.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 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-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..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/index.rst b/doc/sphinx/index.rst deleted file mode 100644 index baf2e0d981..0000000000 --- a/doc/sphinx/index.rst +++ /dev/null @@ -1,91 +0,0 @@ -.. include:: preamble.rst -.. include:: replaces.rst - -.. 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 - -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. - -.. [#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/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 -- cgit v1.2.3