From ddc4391be1214ea4d929ba0a8737be4eda6b87ad Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Wed, 16 May 2018 20:07:30 -0400 Subject: [doc] Fix a typo in coqdomain.py --- doc/sphinx/README.rst | 4 ++-- doc/tools/coqrst/coqdomain.py | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 4673107e3d..983f4e665f 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -260,8 +260,8 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo .. inference:: name - newline-separated premisses - ------------------------ + newline-separated premises + -------------------------- conclusion Example:: diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 40554c3ca3..d81355e865 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -632,8 +632,8 @@ class InferenceDirective(Directive): .. inference:: name - newline-separated premisses - ------------------------ + newline-separated premises + -------------------------- conclusion Example:: -- cgit v1.2.3 From 33fbebc97e9bc399511661bfecc54d92f6ad9a8a Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Wed, 16 May 2018 20:11:22 -0400 Subject: [doc] Move the LaTeX preamble to a separate .tex file --- doc/sphinx/README.rst | 10 ++--- doc/sphinx/preamble.rst | 96 +++---------------------------------------- doc/sphinx/preamble.tex | 88 +++++++++++++++++++++++++++++++++++++++ doc/tools/coqrst/coqdomain.py | 58 ++++++++++++++++---------- 4 files changed, 134 insertions(+), 118 deletions(-) create mode 100644 doc/sphinx/preamble.tex diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 983f4e665f..ab4648d577 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -274,14 +274,12 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo ----------------------------- \WTEG{\forall~x:T,U}{\Prop} -``.. preamble::`` A reST directive for hidden math. - Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. +``.. preamble::`` A reST directive to include a TeX file. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. - Example:: - - .. preamble:: + Usage:: - \newcommand{\paren}[#1]{\left(#1\right)} + .. preamble:: preamble.tex Coq roles ========= diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst index 395f558a85..dcbc3322ac 100644 --- a/doc/sphinx/preamble.rst +++ b/doc/sphinx/preamble.rst @@ -1,92 +1,6 @@ -.. preamble:: +.. only:: html - \[ - \newcommand{\alors}{\textsf{then}} - \newcommand{\alter}{\textsf{alter}} - \newcommand{\as}{\kw{as}} - \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} - \newcommand{\bool}{\textsf{bool}} - \newcommand{\case}{\kw{case}} - \newcommand{\conc}{\textsf{conc}} - \newcommand{\cons}{\textsf{cons}} - \newcommand{\consf}{\textsf{consf}} - \newcommand{\conshl}{\textsf{cons\_hl}} - \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} - \newcommand{\emptyf}{\textsf{emptyf}} - \newcommand{\End}{\kw{End}} - \newcommand{\endkw}{\kw{end}} - \newcommand{\EqSt}{\textsf{EqSt}} - \newcommand{\even}{\textsf{even}} - \newcommand{\evenO}{\textsf{even_O}} - \newcommand{\evenS}{\textsf{even_S}} - \newcommand{\false}{\textsf{false}} - \newcommand{\filter}{\textsf{filter}} - \newcommand{\Fix}{\kw{Fix}} - \newcommand{\fix}{\kw{fix}} - \newcommand{\for}{\textsf{for}} - \newcommand{\forest}{\textsf{forest}} - \newcommand{\from}{\textsf{from}} - \newcommand{\Functor}{\kw{Functor}} - \newcommand{\haslength}{\textsf{has\_length}} - \newcommand{\hd}{\textsf{hd}} - \newcommand{\ident}{\textsf{ident}} - \newcommand{\In}{\kw{in}} - \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} - \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} - \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} - \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} - \newcommand{\injective}{\kw{injective}} - \newcommand{\kw}[1]{\textsf{#1}} - \newcommand{\lb}{\lambda} - \newcommand{\length}{\textsf{length}} - \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} - \newcommand{\List}{\textsf{list}} - \newcommand{\lra}{\longrightarrow} - \newcommand{\Match}{\kw{match}} - \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} - \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} - \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} - \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} - \newcommand{\mto}{.\;} - \newcommand{\Nat}{\mathbb{N}} - \newcommand{\nat}{\textsf{nat}} - \newcommand{\Nil}{\textsf{nil}} - \newcommand{\nilhl}{\textsf{nil\_hl}} - \newcommand{\nO}{\textsf{O}} - \newcommand{\node}{\textsf{node}} - \newcommand{\nS}{\textsf{S}} - \newcommand{\odd}{\textsf{odd}} - \newcommand{\oddS}{\textsf{odd_S}} - \newcommand{\ovl}[1]{\overline{#1}} - \newcommand{\Pair}{\textsf{pair}} - \newcommand{\Prod}{\textsf{prod}} - \newcommand{\Prop}{\textsf{Prop}} - \newcommand{\return}{\kw{return}} - \newcommand{\Set}{\textsf{Set}} - \newcommand{\si}{\textsf{if}} - \newcommand{\sinon}{\textsf{else}} - \newcommand{\Sort}{\cal S} - \newcommand{\Str}{\textsf{Stream}} - \newcommand{\Struct}{\kw{Struct}} - \newcommand{\subst}[3]{#1\{#2/#3\}} - \newcommand{\tl}{\textsf{tl}} - \newcommand{\tree}{\textsf{tree}} - \newcommand{\true}{\textsf{true}} - \newcommand{\Type}{\textsf{Type}} - \newcommand{\unfold}{\textsf{unfold}} - \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} - \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} - \newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} - \newcommand{\WFE}[1]{\WF{E}{#1}} - \newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} - \newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} - \newcommand{\with}{\kw{with}} - \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} - \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} - \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} - \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} - \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} - \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} - \newcommand{\zeroone}[1]{[{#1}]} - \newcommand{\zeros}{\textsf{zeros}} - \] + .. This is included once per page in the HTML build, and a single time (in the + document's preamble) in the LaTeX one. + + .. preamble:: /preamble.tex diff --git a/doc/sphinx/preamble.tex b/doc/sphinx/preamble.tex new file mode 100644 index 0000000000..b4fc608e47 --- /dev/null +++ b/doc/sphinx/preamble.tex @@ -0,0 +1,88 @@ +\newcommand{\alors}{\textsf{then}} +\newcommand{\alter}{\textsf{alter}} +\newcommand{\as}{\kw{as}} +\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} +\newcommand{\bool}{\textsf{bool}} +\newcommand{\case}{\kw{case}} +\newcommand{\conc}{\textsf{conc}} +\newcommand{\cons}{\textsf{cons}} +\newcommand{\consf}{\textsf{consf}} +\newcommand{\conshl}{\textsf{cons\_hl}} +\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} +\newcommand{\emptyf}{\textsf{emptyf}} +\newcommand{\End}{\kw{End}} +\newcommand{\kwend}{\kw{end}} +\newcommand{\EqSt}{\textsf{EqSt}} +\newcommand{\even}{\textsf{even}} +\newcommand{\evenO}{\textsf{even}_\textsf{O}} +\newcommand{\evenS}{\textsf{even}_\textsf{S}} +\newcommand{\false}{\textsf{false}} +\newcommand{\filter}{\textsf{filter}} +\newcommand{\Fix}{\kw{Fix}} +\newcommand{\fix}{\kw{fix}} +\newcommand{\for}{\textsf{for}} +\newcommand{\forest}{\textsf{forest}} +\newcommand{\from}{\textsf{from}} +\newcommand{\Functor}{\kw{Functor}} +\newcommand{\haslength}{\textsf{has\_length}} +\newcommand{\hd}{\textsf{hd}} +\newcommand{\ident}{\textsf{ident}} +\newcommand{\In}{\kw{in}} +\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} +\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} +\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} +\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} +\newcommand{\injective}{\kw{injective}} +\newcommand{\kw}[1]{\textsf{#1}} +\newcommand{\lb}{\lambda} +\newcommand{\length}{\textsf{length}} +\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} +\newcommand{\List}{\textsf{list}} +\newcommand{\lra}{\longrightarrow} +\newcommand{\Match}{\kw{match}} +\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} +\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} +\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} +\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} +\newcommand{\mto}{.\;} +\newcommand{\Nat}{\mathbb{N}} +\newcommand{\nat}{\textsf{nat}} +\newcommand{\Nil}{\textsf{nil}} +\newcommand{\nilhl}{\textsf{nil\_hl}} +\newcommand{\nO}{\textsf{O}} +\newcommand{\node}{\textsf{node}} +\newcommand{\nS}{\textsf{S}} +\newcommand{\odd}{\textsf{odd}} +\newcommand{\oddS}{\textsf{odd}_\textsf{S}} +\newcommand{\ovl}[1]{\overline{#1}} +\newcommand{\Pair}{\textsf{pair}} +\newcommand{\Prod}{\textsf{prod}} +\newcommand{\Prop}{\textsf{Prop}} +\newcommand{\return}{\kw{return}} +\newcommand{\Set}{\textsf{Set}} +\newcommand{\si}{\textsf{if}} +\newcommand{\sinon}{\textsf{else}} +\newcommand{\Sort}{\cal S} +\newcommand{\Str}{\textsf{Stream}} +\newcommand{\Struct}{\kw{Struct}} +\newcommand{\subst}[3]{#1\{#2/#3\}} +\newcommand{\tl}{\textsf{tl}} +\newcommand{\tree}{\textsf{tree}} +\newcommand{\true}{\textsf{true}} +\newcommand{\Type}{\textsf{Type}} +\newcommand{\unfold}{\textsf{unfold}} +\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} +\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} +\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} +\newcommand{\WFE}[1]{\WF{E}{#1}} +\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} +\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} +\newcommand{\with}{\kw{with}} +\newcommand{\WS}[3]{#1[] \vdash #2 <: #3} +\newcommand{\WSE}[2]{\WS{E}{#1}{#2}} +\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} +\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} +\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} +\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} +\newcommand{\zeroone}[1]{[{#1}]} +\newcommand{\zeros}{\textsf{zeros}} diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index d81355e865..b3641c152b 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -34,7 +34,7 @@ from sphinx.util.logging import getLogger from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index from sphinx.domains.std import token_xrefs -from sphinx.ext.mathbase import MathDirective, displaymath +from sphinx.ext import mathbase from . import coqdoc from .repl import ansicolors @@ -58,6 +58,15 @@ def make_target(objtype, targetid): """Create a target to an object of type objtype and id targetid""" return "coq:{}.{}".format(objtype, targetid) +def make_math_node(latex, docname, nowrap): + node = mathbase.displaymath() + node['latex'] = latex + node['label'] = None # Otherwise equations are numbered + node['nowrap'] = nowrap + node['docname'] = docname + node['number'] = None + return node + class CoqObject(ObjectDescription): """A generic Coq object for Sphinx; all Coq objects are subclasses of this. @@ -602,24 +611,39 @@ class ExampleDirective(BaseAdmonition): self.options['classes'] = ['admonition', 'note'] return super().run() -class PreambleDirective(MathDirective): - r"""A reST directive for hidden math. +class PreambleDirective(Directive): + r"""A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. - - Example:: + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. - .. preamble:: + Usage:: - \newcommand{\paren}[#1]{\left(#1\right)} + .. preamble:: preamble.tex """ - directive_name = "preamble" + has_content = False + required_arguments = 1 + optional_arguments = 0 + final_argument_whitespace = True + option_spec = {} def run(self): - self.options['nowrap'] = True - [node] = super().run() + document = self.state.document + env = document.settings.env + + if not document.settings.file_insertion_enabled: + msg = 'File insertion disabled' + return [document.reporter.warning(msg, line=self.lineno)] + + rel_fname, abs_fname = env.relfn2path(self.arguments[0]) + env.note_dependency(rel_fname) + + with open(abs_fname, encoding="utf-8") as ltx: + latex = ltx.read() + + node = make_math_node(latex, env.docname, nowrap=True) node['classes'] = ["math-preamble"] + set_source_info(self, node) return [node] class InferenceDirective(Directive): @@ -652,15 +676,6 @@ class InferenceDirective(Directive): final_argument_whitespace = True directive_name = "inference" - def make_math_node(self, latex): - node = displaymath() - node['latex'] = latex - node['label'] = None # Otherwise equations are numbered - node['nowrap'] = False - node['docname'] = self.state.document.settings.env.docname - node['number'] = None - return node - @staticmethod def prepare_latex_operand(op): # TODO: Could use a fancier inference class in LaTeX @@ -680,7 +695,8 @@ class InferenceDirective(Directive): title = self.arguments[0] content = '\n'.join(self.content) latex = self.prepare_latex(content) - math_node = self.make_math_node(latex) + docname = self.state.document.settings.env.docname + math_node = make_math_node(latex, docname, nowrap=False) tid = nodes.make_id(title) target = nodes.target('', '', ids=['inference-' + tid]) -- cgit v1.2.3 From 47bd6c3de6e8e2e8cdaf049ba95934ad4d0af4f7 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Wed, 16 May 2018 20:50:12 -0400 Subject: [doc] Adjust conf.py to allow LaTeX builds --- doc/sphinx/conf.py | 43 +++++++++++++++++++++---------------------- 1 file changed, 21 insertions(+), 22 deletions(-) diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 8127d3df3f..a213791504 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -257,57 +257,56 @@ smartquotes = False ########################### # Set things up for XeTeX # ########################### + latex_elements = { 'babel': '', 'fontenc': '', 'inputenc': '', 'utf8extra': '', 'cmappkg': '', - # https://www.topbug.net/blog/2015/12/10/a-collection-of-issues-about-the-latex-output-in-sphinx-and-the-solutions/ 'papersize': 'letterpaper', 'classoptions': ',openany', # No blank pages 'polyglossia' : '\\usepackage{polyglossia}', - 'unicode-math' : '\\usepackage{unicode-math}', 'microtype' : '\\usepackage{microtype}', - "preamble": r"\usepackage{coqnotations}" + "preamble": r""" + \usepackage{unicode-math} + + % Macro definitions + \input{preamble.tex} + + % Style definitions for notations + \usepackage{coqnotations} + """ } -from sphinx.builders.latex import LaTeXBuilder +latex_engine = "xelatex" ######## # done # ######## -latex_additional_files = ["_static/coqnotations.sty"] +latex_additional_files = [ + "preamble.tex", + "_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 = [ + (master_doc, 'CoqRefMan.tex', 'Coq Documentation', + 'The Coq Development Team', 'manual'), +] # The name of an image file (relative to this directory) to place at the top of # the title page. -#latex_logo = None - -# For "manual" documents, if this is true, then toplevel headings are parts, -# not chapters. -#latex_use_parts = False +latex_logo = "../../ide/coq.png" # If true, show page references after internal links. #latex_show_pagerefs = False # If true, show URL addresses after external links. -#latex_show_urls = False - -# Documents to append as an appendix to all manuals. -#latex_appendices = [] - -# If false, no module index is generated. -#latex_domain_indices = True - +latex_show_urls = 'footnote' # -- Options for manual page output --------------------------------------- -- cgit v1.2.3 From ad7dda30d651f259304a2efdcc84519ae6542bb7 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Tue, 4 Sep 2018 18:11:40 -0400 Subject: [doc] Explain why zebibliography needs to be separate and oddly-named --- doc/sphinx/zebibliography.rst | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/doc/sphinx/zebibliography.rst b/doc/sphinx/zebibliography.rst index 0000caa301..756edd5482 100644 --- a/doc/sphinx/zebibliography.rst +++ b/doc/sphinx/zebibliography.rst @@ -1,8 +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 +============== .. bibliography:: biblio.bib :cited: -- cgit v1.2.3 From 6146def665803be4f37eedee0d81b2f807e1b3f7 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Mon, 13 Aug 2018 17:45:23 -0400 Subject: [doc] Remove an empty '.. bibliography::' in addendum/program --- doc/sphinx/addendum/program.rst | 3 --- 1 file changed, 3 deletions(-) diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index d6895f5fe5..78471700be 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -378,6 +378,3 @@ Frequently Asked Questions using lazy evaluation; #. Mutual recursion on the underlying inductive type isn’t possible anymore, but nested mutual recursion is always possible. - -.. bibliography:: ../biblio.bib - :keyprefix: p- -- cgit v1.2.3 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 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 From b627c7242d71c834e7a06353ced967c43598e344 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 6 Sep 2018 16:42:24 -0400 Subject: [doc] Create a wrapper around the Credits file for the LaTeX build --- .gitignore | 1 + doc/sphinx/credits-wrapper.html.rst | 7 +++++++ doc/sphinx/credits-wrapper.latex.rst | 3 +++ doc/sphinx/credits.rst | 2 -- doc/sphinx/index.html.rst | 2 +- doc/sphinx/index.latex.rst | 2 +- 6 files changed, 13 insertions(+), 4 deletions(-) create mode 100644 doc/sphinx/credits-wrapper.html.rst create mode 100644 doc/sphinx/credits-wrapper.latex.rst diff --git a/.gitignore b/.gitignore index d52898b3a5..582a8f43c7 100644 --- a/.gitignore +++ b/.gitignore @@ -101,6 +101,7 @@ doc/faq/axioms.pdf_t doc/faq/axioms.png doc/sphinx/index.rst doc/sphinx/zebibliography.rst +doc/sphinx/credits-wrapper.rst doc/stdlib/Library.out doc/stdlib/Library.ps doc/stdlib/Library.coqdoc.tex diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits-wrapper.html.rst new file mode 100644 index 0000000000..2d35a12dc2 --- /dev/null +++ b/doc/sphinx/credits-wrapper.html.rst @@ -0,0 +1,7 @@ +.. _credits: + +------- +Credits +------- + +.. include:: credits.rst diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst new file mode 100644 index 0000000000..9f7dd49af8 --- /dev/null +++ b/doc/sphinx/credits-wrapper.latex.rst @@ -0,0 +1,3 @@ +.. _credits: + +.. include:: credits.rst diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index 62851039bf..be6fe5704e 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1,5 +1,3 @@ -.. _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 index b96a01f76d..96ddd27027 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -28,7 +28,7 @@ Table of contents :caption: Preamble self - credits + credits-wrapper .. toctree:: :caption: The language diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst index 13bc1a19e7..0f2f7b4897 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -10,7 +10,7 @@ Introduction Credits ------- -.. include:: credits.rst +.. include:: credits-wrapper.rst License ------- -- cgit v1.2.3 From a63bc54bfd697e76182044a8515818fa8f92e849 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Wed, 16 May 2018 21:24:47 -0400 Subject: [doc] Fix a few LaTeX mistakes --- doc/sphinx/language/cic.rst | 26 +++++++++++++++----------- doc/sphinx/practical-tools/coqide.rst | 2 +- 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index ac0f0f8ea6..13d6e228a6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1010,7 +1010,7 @@ the Type hierarchy. It is possible to declare the same inductive definition in the universe :math:`\Type`. The :g:`exType` inductive definition has type - :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}` + :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT}_{\kw{intro}}` has type :math:`\Type(k)` with :math:`k`_ included by most chapters of the manual. Some useful LaTeX macros are defined in ``_. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file `_. This file is automatically included in all manual pages. Emacs ----- diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index c333d6e9d5..4ca5171166 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -174,7 +174,7 @@ Add either ``undo`` to the first block or ``reset`` to the second block to avoid Abbreviations and macros ------------------------ -Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file `_ included by most chapters of the manual. Some useful LaTeX macros are defined in ``_. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file `_. This file is automatically included in all manual pages. Emacs ----- diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 2cc1f95c08..3e414a714c 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -1,4 +1,3 @@ -.. include:: ../replaces.rst .. _canonicalstructures: Canonical Structures diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index e507a224c6..ad6a06d2b0 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extendedpatternmatching: Extended pattern-matching diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index e3d25cf5cf..4bfa45d54c 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extraction: Extraction of programs in |OCaml| and Haskell diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e0babb6c4e..5eba539e03 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _generalizedrewriting: Generalized rewriting diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 23cbd76eda..5cb0eaf469 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _implicitcoercions: Implicit Coercions diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 0f2d35d044..2cde65dcdc 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _miscellaneousextensions: Miscellaneous extensions diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index 9adeca46fc..e7a8c238ac 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -1,5 +1,3 @@ -.. include:: ../preamble.rst - .. _nsatz_chapter: Nsatz: tactics for proving equalities in integral domains diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 8ee8f52227..eb19d57203 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _asynchronousandparallelproofprocessing: Asynchronous and Parallel Proof Processing diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 78471700be..24247f7bb1 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. this should be just "_program", but refs to it don't work .. _programs: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 8cb86e2267..58617916c0 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -1,11 +1,9 @@ -.. include:: ../replaces.rst .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}` .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}` .. |eq| replace:: `=`:sub:`(by the main correctness theorem)` .. |re| replace:: ``(PEeval`` `v` `ap`\ ``)`` .. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))`` - .. _theringandfieldtacticfamilies: The ring and field tactic families diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index ab4b4a9824..418014809f 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _typeclasses: Type Classes diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7e77dea457..706ce1065c 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _polymorphicuniverses: Polymorphic Universes diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 35c08fd806..8b29d1e9f9 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -36,6 +36,12 @@ sys.path.append(os.path.abspath('../../config/')) import coq_config +# -- Prolog --------------------------------------------------------------- + +# Include substitution definitions in all files +with open("refman-preamble.rst") as s: + rst_prolog = s.read() + # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 797a9a9714..5bb7bf542c 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,6 +1,3 @@ -.. 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. Links to several tutorials can be found at diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 13d6e228a6..c8c3e37efb 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _calculusofinductiveconstructions: diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 9de30e2190..320448d46e 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thecoqlibrary: The |Coq| library diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 0fbe7ac70b..ae96a75a94 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extensionsofgallina: Extensions of |Gallina| diff --git a/doc/sphinx/language/module-system.rst b/doc/sphinx/language/module-system.rst index e6a6736654..15fee91245 100644 --- a/doc/sphinx/language/module-system.rst +++ b/doc/sphinx/language/module-system.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _themodulesystem: The Module System diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 9498f37c7e..343ca9ed7d 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thecoqcommands: The |Coq| commands diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index e8fc29dece..9455228e7d 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _coqintegrateddevelopmentenvironment: |Coq| Integrated Development Environment diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index b9a4d2a7bd..5d300c3d6d 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _utilities: --------------------- diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst deleted file mode 100644 index dcbc3322ac..0000000000 --- a/doc/sphinx/preamble.rst +++ /dev/null @@ -1,6 +0,0 @@ -.. only:: html - - .. This is included once per page in the HTML build, and a single time (in the - document's preamble) in the LaTeX one. - - .. preamble:: /preamble.tex diff --git a/doc/sphinx/preamble.tex b/doc/sphinx/preamble.tex deleted file mode 100644 index b4fc608e47..0000000000 --- a/doc/sphinx/preamble.tex +++ /dev/null @@ -1,88 +0,0 @@ -\newcommand{\alors}{\textsf{then}} -\newcommand{\alter}{\textsf{alter}} -\newcommand{\as}{\kw{as}} -\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} -\newcommand{\bool}{\textsf{bool}} -\newcommand{\case}{\kw{case}} -\newcommand{\conc}{\textsf{conc}} -\newcommand{\cons}{\textsf{cons}} -\newcommand{\consf}{\textsf{consf}} -\newcommand{\conshl}{\textsf{cons\_hl}} -\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} -\newcommand{\emptyf}{\textsf{emptyf}} -\newcommand{\End}{\kw{End}} -\newcommand{\kwend}{\kw{end}} -\newcommand{\EqSt}{\textsf{EqSt}} -\newcommand{\even}{\textsf{even}} -\newcommand{\evenO}{\textsf{even}_\textsf{O}} -\newcommand{\evenS}{\textsf{even}_\textsf{S}} -\newcommand{\false}{\textsf{false}} -\newcommand{\filter}{\textsf{filter}} -\newcommand{\Fix}{\kw{Fix}} -\newcommand{\fix}{\kw{fix}} -\newcommand{\for}{\textsf{for}} -\newcommand{\forest}{\textsf{forest}} -\newcommand{\from}{\textsf{from}} -\newcommand{\Functor}{\kw{Functor}} -\newcommand{\haslength}{\textsf{has\_length}} -\newcommand{\hd}{\textsf{hd}} -\newcommand{\ident}{\textsf{ident}} -\newcommand{\In}{\kw{in}} -\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} -\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} -\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} -\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} -\newcommand{\injective}{\kw{injective}} -\newcommand{\kw}[1]{\textsf{#1}} -\newcommand{\lb}{\lambda} -\newcommand{\length}{\textsf{length}} -\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} -\newcommand{\List}{\textsf{list}} -\newcommand{\lra}{\longrightarrow} -\newcommand{\Match}{\kw{match}} -\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} -\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} -\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} -\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} -\newcommand{\mto}{.\;} -\newcommand{\Nat}{\mathbb{N}} -\newcommand{\nat}{\textsf{nat}} -\newcommand{\Nil}{\textsf{nil}} -\newcommand{\nilhl}{\textsf{nil\_hl}} -\newcommand{\nO}{\textsf{O}} -\newcommand{\node}{\textsf{node}} -\newcommand{\nS}{\textsf{S}} -\newcommand{\odd}{\textsf{odd}} -\newcommand{\oddS}{\textsf{odd}_\textsf{S}} -\newcommand{\ovl}[1]{\overline{#1}} -\newcommand{\Pair}{\textsf{pair}} -\newcommand{\Prod}{\textsf{prod}} -\newcommand{\Prop}{\textsf{Prop}} -\newcommand{\return}{\kw{return}} -\newcommand{\Set}{\textsf{Set}} -\newcommand{\si}{\textsf{if}} -\newcommand{\sinon}{\textsf{else}} -\newcommand{\Sort}{\cal S} -\newcommand{\Str}{\textsf{Stream}} -\newcommand{\Struct}{\kw{Struct}} -\newcommand{\subst}[3]{#1\{#2/#3\}} -\newcommand{\tl}{\textsf{tl}} -\newcommand{\tree}{\textsf{tree}} -\newcommand{\true}{\textsf{true}} -\newcommand{\Type}{\textsf{Type}} -\newcommand{\unfold}{\textsf{unfold}} -\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} -\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} -\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} -\newcommand{\WFE}[1]{\WF{E}{#1}} -\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} -\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} -\newcommand{\with}{\kw{with}} -\newcommand{\WS}[3]{#1[] \vdash #2 <: #3} -\newcommand{\WSE}[2]{\WS{E}{#1}{#2}} -\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} -\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} -\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} -\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} -\newcommand{\zeroone}[1]{[{#1}]} -\newcommand{\zeros}{\textsf{zeros}} diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 1fc267488c..38fdf243fe 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _ltac: The tactic language diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index b1e769c571..53294bf8da 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -1,4 +1,3 @@ -.. include:: ../replaces.rst .. _proofhandling: ------------------- diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 8656e5eb3e..361b6e44a5 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thessreflectprooflanguage: ------------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fb121c82ec..b0b57d00a0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _tactics: Tactics diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 584193b9c6..56df535d85 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _vernacularcommands: Vernacular commands diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst new file mode 100644 index 0000000000..aa581e1ee1 --- /dev/null +++ b/doc/sphinx/refman-preamble.rst @@ -0,0 +1,98 @@ +.. This file is automatically prepended to all other files using the ``rst_prolog`` option. + +.. only:: html + + .. This is included once per page in the HTML build, and a single time (in the + document's preamble) in the LaTeX one. + + .. preamble:: /refman-preamble.sty + +.. Some handy replacements for common items + +.. role:: smallcaps + +.. |A_1| replace:: `A`\ :math:`_{1}` +.. |A_n| replace:: `A`\ :math:`_{n}` +.. |arg_1| replace:: `arg`\ :math:`_{1}` +.. |arg_n| replace:: `arg`\ :math:`_{n}` +.. |bdi| replace:: :math:`\beta\delta\iota` +.. |binder_1| replace:: `binder`\ :math:`_{1}` +.. |binder_n| replace:: `binder`\ :math:`_{n}` +.. |binders_1| replace:: `binders`\ :math:`_{1}` +.. |binders_n| replace:: `binders`\ :math:`_{n}` +.. |C_1| replace:: `C`\ :math:`_{1}` +.. |c_1| replace:: `c`\ :math:`_{1}` +.. |C_2| replace:: `C`\ :math:`_{2}` +.. |c_i| replace:: `c`\ :math:`_{i}` +.. |c_n| replace:: `c`\ :math:`_{n}` +.. |Cic| replace:: :smallcaps:`Cic` +.. |class_1| replace:: `class`\ :math:`_{1}` +.. |class_2| replace:: `class`\ :math:`_{2}` +.. |Coq| replace:: :smallcaps:`Coq` +.. |CoqIDE| replace:: :smallcaps:`CoqIDE` +.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\beta\delta\iota\zeta}}` +.. |Gallina| replace:: :smallcaps:`Gallina` +.. |ident_0| replace:: `ident`\ :math:`_{0}` +.. |ident_1,1| replace:: `ident`\ :math:`_{1,1}` +.. |ident_1,k_1| replace:: `ident`\ :math:`_{1,k_1}`) +.. |ident_1| replace:: `ident`\ :math:`_{1}` +.. |ident_2| replace:: `ident`\ :math:`_{2}` +.. |ident_3| replace:: `ident`\ :math:`_{3}` +.. |ident_i| replace:: `ident`\ :math:`_{i}` +.. |ident_j| replace:: `ident`\ :math:`_{j}` +.. |ident_k| replace:: `ident`\ :math:`_{k}` +.. |ident_n,1| replace:: `ident`\ :math:`_{n,1}` +.. |ident_n,k_n| replace:: `ident`\ :math:`_{n,k_n}` +.. |ident_n| replace:: `ident`\ :math:`_{n}` +.. |Latex| replace:: :smallcaps:`LaTeX` +.. |L_tac| replace:: `L`:sub:`tac` +.. |Ltac| replace:: `L`:sub:`tac` +.. |ML| replace:: :smallcaps:`ML` +.. |mod_0| replace:: `mod`\ :math:`_{0}` +.. |mod_1| replace:: `mod`\ :math:`_{1}` +.. |mod_2| replace:: `mod`\ :math:`_{1}` +.. |mod_n| replace:: `mod`\ :math:`_{n}` +.. |module_0| replace:: `module`\ :math:`_{0}` +.. |module_1| replace:: `module`\ :math:`_{1}` +.. |module_expression_0| replace:: `module_expression`\ :math:`_{0}` +.. |module_expression_1| replace:: `module_expression`\ :math:`_{1}` +.. |module_expression_i| replace:: `module_expression`\ :math:`_{i}` +.. |module_expression_n| replace:: `module_expression`\ :math:`_{n}` +.. |module_n| replace:: `module`\ :math:`_{n}` +.. |module_type_0| replace:: `module_type`\ :math:`_{0}` +.. |module_type_1| replace:: `module_type`\ :math:`_{1}` +.. |module_type_i| replace:: `module_type`\ :math:`_{i}` +.. |module_type_n| replace:: `module_type`\ :math:`_{n}` +.. |N| replace:: ``N`` +.. |nat| replace:: ``nat`` +.. |OCaml| replace:: :smallcaps:`OCaml` +.. |p_1| replace:: `p`\ :math:`_{1}` +.. |p_i| replace:: `p`\ :math:`_{i}` +.. |p_n| replace:: `p`\ :math:`_{n}` +.. |Program| replace:: :strong:`Program` +.. |SSR| replace:: :smallcaps:`SSReflect` +.. |t_1| replace:: `t`\ :math:`_{1}` +.. |t_i| replace:: `t`\ :math:`_{i}` +.. |t_m| replace:: `t`\ :math:`_{m}` +.. |t_n| replace:: `t`\ :math:`_{n}` +.. |f_1| replace:: `f`\ :math:`_{1}` +.. |f_i| replace:: `f`\ :math:`_{i}` +.. |f_m| replace:: `f`\ :math:`_{m}` +.. |f_n| replace:: `f`\ :math:`_{n}` +.. |u_1| replace:: `u`\ :math:`_{1}` +.. |u_i| replace:: `u`\ :math:`_{i}` +.. |u_m| replace:: `u`\ :math:`_{m}` +.. |u_n| replace:: `u`\ :math:`_{n}` +.. |term_0| replace:: `term`\ :math:`_{0}` +.. |term_1| replace:: `term`\ :math:`_{1}` +.. |term_2| replace:: `term`\ :math:`_{2}` +.. |term_n| replace:: `term`\ :math:`_{n}` +.. |type_0| replace:: `type`\ :math:`_{0}` +.. |type_1| replace:: `type`\ :math:`_{1}` +.. |type_2| replace:: `type`\ :math:`_{2}` +.. |type_3| replace:: `type`\ :math:`_{3}` +.. |type_n| replace:: `type`\ :math:`_{n}` +.. |x_1| replace:: `x`\ :math:`_{1}` +.. |x_i| replace:: `x`\ :math:`_{i}` +.. |x_n| replace:: `x`\ :math:`_{n}` +.. |Z| replace:: ``Z`` diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty new file mode 100644 index 0000000000..b4fc608e47 --- /dev/null +++ b/doc/sphinx/refman-preamble.sty @@ -0,0 +1,88 @@ +\newcommand{\alors}{\textsf{then}} +\newcommand{\alter}{\textsf{alter}} +\newcommand{\as}{\kw{as}} +\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} +\newcommand{\bool}{\textsf{bool}} +\newcommand{\case}{\kw{case}} +\newcommand{\conc}{\textsf{conc}} +\newcommand{\cons}{\textsf{cons}} +\newcommand{\consf}{\textsf{consf}} +\newcommand{\conshl}{\textsf{cons\_hl}} +\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} +\newcommand{\emptyf}{\textsf{emptyf}} +\newcommand{\End}{\kw{End}} +\newcommand{\kwend}{\kw{end}} +\newcommand{\EqSt}{\textsf{EqSt}} +\newcommand{\even}{\textsf{even}} +\newcommand{\evenO}{\textsf{even}_\textsf{O}} +\newcommand{\evenS}{\textsf{even}_\textsf{S}} +\newcommand{\false}{\textsf{false}} +\newcommand{\filter}{\textsf{filter}} +\newcommand{\Fix}{\kw{Fix}} +\newcommand{\fix}{\kw{fix}} +\newcommand{\for}{\textsf{for}} +\newcommand{\forest}{\textsf{forest}} +\newcommand{\from}{\textsf{from}} +\newcommand{\Functor}{\kw{Functor}} +\newcommand{\haslength}{\textsf{has\_length}} +\newcommand{\hd}{\textsf{hd}} +\newcommand{\ident}{\textsf{ident}} +\newcommand{\In}{\kw{in}} +\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} +\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} +\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} +\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} +\newcommand{\injective}{\kw{injective}} +\newcommand{\kw}[1]{\textsf{#1}} +\newcommand{\lb}{\lambda} +\newcommand{\length}{\textsf{length}} +\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} +\newcommand{\List}{\textsf{list}} +\newcommand{\lra}{\longrightarrow} +\newcommand{\Match}{\kw{match}} +\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} +\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} +\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} +\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} +\newcommand{\mto}{.\;} +\newcommand{\Nat}{\mathbb{N}} +\newcommand{\nat}{\textsf{nat}} +\newcommand{\Nil}{\textsf{nil}} +\newcommand{\nilhl}{\textsf{nil\_hl}} +\newcommand{\nO}{\textsf{O}} +\newcommand{\node}{\textsf{node}} +\newcommand{\nS}{\textsf{S}} +\newcommand{\odd}{\textsf{odd}} +\newcommand{\oddS}{\textsf{odd}_\textsf{S}} +\newcommand{\ovl}[1]{\overline{#1}} +\newcommand{\Pair}{\textsf{pair}} +\newcommand{\Prod}{\textsf{prod}} +\newcommand{\Prop}{\textsf{Prop}} +\newcommand{\return}{\kw{return}} +\newcommand{\Set}{\textsf{Set}} +\newcommand{\si}{\textsf{if}} +\newcommand{\sinon}{\textsf{else}} +\newcommand{\Sort}{\cal S} +\newcommand{\Str}{\textsf{Stream}} +\newcommand{\Struct}{\kw{Struct}} +\newcommand{\subst}[3]{#1\{#2/#3\}} +\newcommand{\tl}{\textsf{tl}} +\newcommand{\tree}{\textsf{tree}} +\newcommand{\true}{\textsf{true}} +\newcommand{\Type}{\textsf{Type}} +\newcommand{\unfold}{\textsf{unfold}} +\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} +\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} +\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} +\newcommand{\WFE}[1]{\WF{E}{#1}} +\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} +\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} +\newcommand{\with}{\kw{with}} +\newcommand{\WS}[3]{#1[] \vdash #2 <: #3} +\newcommand{\WSE}[2]{\WS{E}{#1}{#2}} +\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} +\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} +\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} +\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} +\newcommand{\zeroone}[1]{[{#1}]} +\newcommand{\zeros}{\textsf{zeros}} diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/replaces.rst deleted file mode 100644 index 28a04f90ce..0000000000 --- a/doc/sphinx/replaces.rst +++ /dev/null @@ -1,89 +0,0 @@ -.. some handy replacements for common items - -.. role:: smallcaps - -.. |A_1| replace:: `A`\ :math:`_{1}` -.. |A_n| replace:: `A`\ :math:`_{n}` -.. |arg_1| replace:: `arg`\ :math:`_{1}` -.. |arg_n| replace:: `arg`\ :math:`_{n}` -.. |bdi| replace:: :math:`\beta\delta\iota` -.. |binder_1| replace:: `binder`\ :math:`_{1}` -.. |binder_n| replace:: `binder`\ :math:`_{n}` -.. |binders_1| replace:: `binders`\ :math:`_{1}` -.. |binders_n| replace:: `binders`\ :math:`_{n}` -.. |C_1| replace:: `C`\ :math:`_{1}` -.. |c_1| replace:: `c`\ :math:`_{1}` -.. |C_2| replace:: `C`\ :math:`_{2}` -.. |c_i| replace:: `c`\ :math:`_{i}` -.. |c_n| replace:: `c`\ :math:`_{n}` -.. |Cic| replace:: :smallcaps:`Cic` -.. |class_1| replace:: `class`\ :math:`_{1}` -.. |class_2| replace:: `class`\ :math:`_{2}` -.. |Coq| replace:: :smallcaps:`Coq` -.. |CoqIDE| replace:: :smallcaps:`CoqIDE` -.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\beta\delta\iota\zeta}}` -.. |Gallina| replace:: :smallcaps:`Gallina` -.. |ident_0| replace:: `ident`\ :math:`_{0}` -.. |ident_1,1| replace:: `ident`\ :math:`_{1,1}` -.. |ident_1,k_1| replace:: `ident`\ :math:`_{1,k_1}`) -.. |ident_1| replace:: `ident`\ :math:`_{1}` -.. |ident_2| replace:: `ident`\ :math:`_{2}` -.. |ident_3| replace:: `ident`\ :math:`_{3}` -.. |ident_i| replace:: `ident`\ :math:`_{i}` -.. |ident_j| replace:: `ident`\ :math:`_{j}` -.. |ident_k| replace:: `ident`\ :math:`_{k}` -.. |ident_n,1| replace:: `ident`\ :math:`_{n,1}` -.. |ident_n,k_n| replace:: `ident`\ :math:`_{n,k_n}` -.. |ident_n| replace:: `ident`\ :math:`_{n}` -.. |Latex| replace:: :smallcaps:`LaTeX` -.. |L_tac| replace:: `L`:sub:`tac` -.. |Ltac| replace:: `L`:sub:`tac` -.. |ML| replace:: :smallcaps:`ML` -.. |mod_0| replace:: `mod`\ :math:`_{0}` -.. |mod_1| replace:: `mod`\ :math:`_{1}` -.. |mod_2| replace:: `mod`\ :math:`_{1}` -.. |mod_n| replace:: `mod`\ :math:`_{n}` -.. |module_0| replace:: `module`\ :math:`_{0}` -.. |module_1| replace:: `module`\ :math:`_{1}` -.. |module_expression_0| replace:: `module_expression`\ :math:`_{0}` -.. |module_expression_1| replace:: `module_expression`\ :math:`_{1}` -.. |module_expression_i| replace:: `module_expression`\ :math:`_{i}` -.. |module_expression_n| replace:: `module_expression`\ :math:`_{n}` -.. |module_n| replace:: `module`\ :math:`_{n}` -.. |module_type_0| replace:: `module_type`\ :math:`_{0}` -.. |module_type_1| replace:: `module_type`\ :math:`_{1}` -.. |module_type_i| replace:: `module_type`\ :math:`_{i}` -.. |module_type_n| replace:: `module_type`\ :math:`_{n}` -.. |N| replace:: ``N`` -.. |nat| replace:: ``nat`` -.. |OCaml| replace:: :smallcaps:`OCaml` -.. |p_1| replace:: `p`\ :math:`_{1}` -.. |p_i| replace:: `p`\ :math:`_{i}` -.. |p_n| replace:: `p`\ :math:`_{n}` -.. |Program| replace:: :strong:`Program` -.. |SSR| replace:: :smallcaps:`SSReflect` -.. |t_1| replace:: `t`\ :math:`_{1}` -.. |t_i| replace:: `t`\ :math:`_{i}` -.. |t_m| replace:: `t`\ :math:`_{m}` -.. |t_n| replace:: `t`\ :math:`_{n}` -.. |f_1| replace:: `f`\ :math:`_{1}` -.. |f_i| replace:: `f`\ :math:`_{i}` -.. |f_m| replace:: `f`\ :math:`_{m}` -.. |f_n| replace:: `f`\ :math:`_{n}` -.. |u_1| replace:: `u`\ :math:`_{1}` -.. |u_i| replace:: `u`\ :math:`_{i}` -.. |u_m| replace:: `u`\ :math:`_{m}` -.. |u_n| replace:: `u`\ :math:`_{n}` -.. |term_0| replace:: `term`\ :math:`_{0}` -.. |term_1| replace:: `term`\ :math:`_{1}` -.. |term_2| replace:: `term`\ :math:`_{2}` -.. |term_n| replace:: `term`\ :math:`_{n}` -.. |type_0| replace:: `type`\ :math:`_{0}` -.. |type_1| replace:: `type`\ :math:`_{1}` -.. |type_2| replace:: `type`\ :math:`_{2}` -.. |type_3| replace:: `type`\ :math:`_{3}` -.. |type_n| replace:: `type`\ :math:`_{n}` -.. |x_1| replace:: `x`\ :math:`_{1}` -.. |x_i| replace:: `x`\ :math:`_{i}` -.. |x_n| replace:: `x`\ :math:`_{n}` -.. |Z| replace:: ``Z`` diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 4c0e85bdd4..0236f19490 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _syntaxextensionsandinterpretationscopes: Syntax extensions and interpretation scopes -- cgit v1.2.3 From d9209353ced1b6ba23cb18e6b4d8e8f9c0c20d92 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 17 May 2018 22:22:10 -0400 Subject: [doc] Fix a typo in the developer guide --- doc/tools/coqrst/coqdomain.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index f62df94e36..3bb805f2dc 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -496,7 +496,7 @@ def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): CoqCodeRole = coq_code_role class CoqtopDirective(Directive): - """A reST directive to describe interactions with Coqtop. + r"""A reST directive to describe interactions with Coqtop. Usage:: -- cgit v1.2.3 From a5586852cca4a8a9b57506fd2ea09438bd5bda2e Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 17 May 2018 22:27:42 -0400 Subject: [doc] Work around https://github.com/sphinx-doc/sphinx/issues/4980 --- doc/tools/coqrst/coqdomain.py | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 3bb805f2dc..86f5622912 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -534,16 +534,17 @@ class CoqtopDirective(Directive): required_arguments = 0 optional_arguments = 1 final_argument_whitespace = True + option_spec = { 'name': directives.unchanged } directive_name = "coqtop" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable # Pygments-based post-processing (we could also set rawsource to '') content = '\n'.join(self.content) - options = self.arguments[0].split() if self.arguments else ['in'] - if 'all' in options: - options.extend(['in', 'out']) - node = nodes.container(content, coqtop_options = list(set(options)), + args = self.arguments[0].split() if self.arguments else ['in'] + if 'all' in args: + args.extend(['in', 'out']) + node = nodes.container(content, coqtop_options = list(set(args)), classes=['coqtop', 'literal-block']) self.add_name(node) return [node] @@ -568,6 +569,7 @@ class CoqdocDirective(Directive): required_arguments = 0 optional_arguments = 0 final_argument_whitespace = True + option_spec = { 'name': directives.unchanged } directive_name = "coqdoc" def run(self): @@ -576,6 +578,7 @@ class CoqdocDirective(Directive): content = '\n'.join(self.content) node = nodes.inline(content, '', *highlight_using_coqdoc(content)) wrapper = nodes.container(content, node, classes=['coqdoc', 'literal-block']) + self.add_name(wrapper) return [wrapper] class ExampleDirective(BaseAdmonition): -- cgit v1.2.3 From 48662f95c63a02d90630941aace96e7b44dcc247 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 17 May 2018 22:28:19 -0400 Subject: [doc] Ensure that merging coqtop blocks preserves anchors --- doc/tools/coqrst/coqdomain.py | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 86f5622912..1ae2a4a19f 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -846,23 +846,28 @@ class CoqtopBlocksTransform(Transform): kept_node['classes'] = [c for c in kept_node['classes'] if c != 'coqtop-hidden'] - def merge_consecutive_coqtop_blocks(self): + @staticmethod + def merge_consecutive_coqtop_blocks(app, doctree, _): """Merge consecutive divs wrapping lists of Coq sentences; keep ‘dl’s separate.""" - for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block): + for node in doctree.traverse(CoqtopBlocksTransform.is_coqtop_block): if node.parent: + rawsources, names = [node.rawsource], set(node['names']) for sibling in node.traverse(include_self=False, descend=False, siblings=True, ascend=False): if CoqtopBlocksTransform.is_coqtop_block(sibling): - self.merge_coqtop_classes(node, sibling) + CoqtopBlocksTransform.merge_coqtop_classes(node, sibling) + rawsources.append(sibling.rawsource) + names.update(sibling['names']) node.extend(sibling.children) node.parent.remove(sibling) sibling.parent = None else: break + node.rawsource = "\n\n".join(rawsources) + node['names'] = list(names) def apply(self): self.add_coqtop_output() - self.merge_consecutive_coqtop_blocks() class CoqSubdomainsIndex(Index): """Index subclass to provide subdomain-specific indices. @@ -1078,7 +1083,6 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: pygments if available. This prevents the LaTeX builder from getting confused. """ - is_html = app.builder.tags.has("html") for node in doctree.traverse(is_coqtop_or_coqdoc_block): if is_html: @@ -1115,6 +1119,7 @@ def setup(app): app.add_transform(CoqtopBlocksTransform) app.connect('doctree-resolved', simplify_source_code_blocks_for_latex) + app.connect('doctree-resolved', CoqtopBlocksTransform.merge_consecutive_coqtop_blocks) # Add extra styles app.add_stylesheet("fonts.css") -- cgit v1.2.3 From 468815006f1c272a6ada7186186f90a6692d2521 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 17 May 2018 22:30:53 -0400 Subject: [doc] Work around https://github.com/sphinx-doc/sphinx/issues/4979 --- doc/sphinx/proof-engine/proof-handling.rst | 7 ++++++- doc/tools/coqrst/coqdomain.py | 11 ++++++++--- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 53294bf8da..3c0577b8e4 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -441,7 +441,12 @@ The following example script illustrates all these features: You tried to apply a tactic but no goals were under focus. Using :n:`@bullet` is mandatory here. -.. exn:: No such goal. Try unfocusing with %{. +.. FIXME: the :noindex: below works around a Sphinx issue. + (https://github.com/sphinx-doc/sphinx/issues/4979) + It should be removed once that issue is fixed. + +.. exn:: No such goal. Try unfocusing with %}. + :noindex: You just finished a goal focused by ``{``, you must unfocus it with ``}``. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 1ae2a4a19f..6317e6e214 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -110,7 +110,9 @@ class CoqObject(ObjectDescription): # Explicit object naming 'name': directives.unchanged, # Silence warnings produced by report_undocumented_coq_objects - 'undocumented': directives.flag + 'undocumented': directives.flag, + # noindex omits this object from its index + 'noindex': directives.flag } def subdomain_data(self): @@ -174,13 +176,16 @@ class CoqObject(ObjectDescription): """Add `name` (pointing to `target`) to the main index.""" assert isinstance(name, str) if not name.startswith("_"): - index_text = name + # remove trailing . , found in commands, but not ... (ellipsis) + trim = name.endswith(".") and not name.endswith("...") + index_text = name[:-1] if trim else name if self.index_suffix: index_text += " " + self.index_suffix self.indexnode['entries'].append(('single', index_text, target, '', None)) def add_target_and_index(self, name, _, signode): - """Attach a link target to `signode` and an index entry for `name`.""" + """Attach a link target to `signode` and an index entry for `name`. + This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified.""" if name: target = self._add_target(signode, name) self._add_index_entry(name, target) -- cgit v1.2.3 From a249f94d00c64157631fe2517d317dd75ebeff88 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 17 May 2018 23:42:01 -0400 Subject: [doc] Add a warning about overusing the `coqtop` directive --- doc/sphinx/README.rst | 33 +++++++++++++++++++++++++++++++++ doc/sphinx/README.template.rst | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 66 insertions(+) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index fbf94fd7da..2884f70477 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -375,6 +375,39 @@ DON'T .. tacv:: assert form as intro_pattern +Using the ``.. coqtop::`` directive for syntax highlighting +----------------------------------------------------------- + +DO + .. code:: + + A tactic of the form: + + .. coqdoc:: + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqdoc:: + + first [ t1 | … | tn ]. + +DONT + .. code:: + + A tactic of the form: + + .. coqtop:: in + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqtop:: in + + first [ t1 | … | tn ]. + Tips and tricks =============== diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 4ca5171166..d1052d48b2 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -153,6 +153,39 @@ DON'T .. tacv:: assert form as intro_pattern +Using the ``.. coqtop::`` directive for syntax highlighting +----------------------------------------------------------- + +DO + .. code:: + + A tactic of the form: + + .. coqdoc:: + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqdoc:: + + first [ t1 | … | tn ]. + +DONT + .. code:: + + A tactic of the form: + + .. coqtop:: in + + do [ t1 | … | tn ]. + + is equivalent to the standard Ltac expression: + + .. coqtop:: in + + first [ t1 | … | tn ]. + Tips and tricks =============== -- cgit v1.2.3 From 196f36e1db08c80c0e2d1de538a4c0fe6bae062b Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 17 May 2018 23:42:51 -0400 Subject: [doc] Mark the dummy index files as orphans (the LaTeX build skips them) Do we really need these? Wouldn't it be better to just add appropriate links to the html template? --- doc/sphinx/coq-cmdindex.rst | 2 ++ doc/sphinx/coq-exnindex.rst | 2 ++ doc/sphinx/coq-optindex.rst | 2 ++ doc/sphinx/coq-tacindex.rst | 2 ++ doc/sphinx/genindex.rst | 2 ++ 5 files changed, 10 insertions(+) diff --git a/doc/sphinx/coq-cmdindex.rst b/doc/sphinx/coq-cmdindex.rst index 7df6cb36c5..fd0b342ae4 100644 --- a/doc/sphinx/coq-cmdindex.rst +++ b/doc/sphinx/coq-cmdindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ----------------- diff --git a/doc/sphinx/coq-exnindex.rst b/doc/sphinx/coq-exnindex.rst index 100c57b085..dbf60bb06c 100644 --- a/doc/sphinx/coq-exnindex.rst +++ b/doc/sphinx/coq-exnindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ---------------------- diff --git a/doc/sphinx/coq-optindex.rst b/doc/sphinx/coq-optindex.rst index f8046a800b..925d4cd185 100644 --- a/doc/sphinx/coq-optindex.rst +++ b/doc/sphinx/coq-optindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ----------------- diff --git a/doc/sphinx/coq-tacindex.rst b/doc/sphinx/coq-tacindex.rst index 588104f465..31b2f7f8cb 100644 --- a/doc/sphinx/coq-tacindex.rst +++ b/doc/sphinx/coq-tacindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ------------- diff --git a/doc/sphinx/genindex.rst b/doc/sphinx/genindex.rst index a991c7f9f8..29f792b3aa 100644 --- a/doc/sphinx/genindex.rst +++ b/doc/sphinx/genindex.rst @@ -1,3 +1,5 @@ +:orphan: + .. hack to get index in TOC ----- -- cgit v1.2.3 From e45bada261c42152e0b835cae7e989a7fccc0fb7 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 00:07:36 -0400 Subject: [doc] Add more common mistakes to the documentation-writing guide --- doc/sphinx/README.rst | 43 ++++++++++++++++++++++++++++++++++++++++++ doc/sphinx/README.template.rst | 43 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 86 insertions(+) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 2884f70477..6d5545ec3c 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -362,6 +362,32 @@ DON'T This is equivalent to ``Axiom`` :token`ident` : :token:`term`. +.. + +DO + .. code:: + + :n:`power_tac @term [@ltac]` + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +DON'T + .. code:: + + power_tac :n:`@term` [:n:`@ltac`] + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +.. + +DO + .. code:: + + :n:`name={*; attr}` + +DON'T + .. code:: + + ``name=``:n:`{*; attr}` + Omitting annotations -------------------- @@ -408,6 +434,23 @@ DONT first [ t1 | … | tn ]. +Overusing plain quotes +---------------------- + +DO + .. code:: + + The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception. + The term :g:`let a = 1 in a a` is ill-typed. + +DON'T + .. code:: + + The ``refine`` tactic can raise the ``Invalid argument`` exception. + The term ``let a = 1 in a a`` is ill-typed. + +Plain quotes produce plain text, without highlighting or cross-references. + Tips and tricks =============== diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index d1052d48b2..73b2e96dcb 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -140,6 +140,32 @@ DON'T This is equivalent to ``Axiom`` :token`ident` : :token:`term`. +.. + +DO + .. code:: + + :n:`power_tac @term [@ltac]` + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +DON'T + .. code:: + + power_tac :n:`@term` [:n:`@ltac`] + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize … + +.. + +DO + .. code:: + + :n:`name={*; attr}` + +DON'T + .. code:: + + ``name=``:n:`{*; attr}` + Omitting annotations -------------------- @@ -186,6 +212,23 @@ DONT first [ t1 | … | tn ]. +Overusing plain quotes +---------------------- + +DO + .. code:: + + The :tacn:`refine` tactic can raise the :exn:`Invalid argument` exception. + The term :g:`let a = 1 in a a` is ill-typed. + +DON'T + .. code:: + + The ``refine`` tactic can raise the ``Invalid argument`` exception. + The term ``let a = 1 in a a`` is ill-typed. + +Plain quotes produce plain text, without highlighting or cross-references. + Tips and tricks =============== -- cgit v1.2.3 From 0b5251ee8a6f69d4b0700991884e68dfdfcf8ad6 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:10:15 -0400 Subject: [doc] Rewrite and document the prodn directive It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place. --- doc/tools/coqrst/coqdomain.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 6317e6e214..2bf9776751 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -149,6 +149,13 @@ class CoqObject(ObjectDescription): msg = MSG.format(name, self.env.doc2path(objects[name][0])) self.state_machine.reporter.warning(msg, line=self.lineno) + def _warn_if_duplicate_name(self, objects, name): + """Check that two objects in the same domain don't have the same name.""" + if name in objects: + MSG = 'Duplicate object: {}; other is at {}' + msg = MSG.format(name, self.env.doc2path(objects[name][0])) + self.state_machine.reporter.warning(msg, line=self.lineno) + def _record_name(self, name, target_id): """Record a name, mapping it to target_id -- cgit v1.2.3 From aaabad040eaf50c6c11823d64a08027c080aa113 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:19:50 -0400 Subject: [doc] Fix more duplicate-label issues in production lists --- doc/sphinx/language/gallina-extensions.rst | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ae96a75a94..27ed176a9b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -20,7 +20,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining .. _record_grammar: - .. productionlist:: `sentence` + .. productionlist:: sentence record : `record_keyword` `record_body` with … with `record_body` record_keyword : Record | Inductive | CoInductive record_body : `ident` [ `binders` ] [: `sort` ] := [ `ident` ] { [ `field` ; … ; `field` ] }. @@ -80,11 +80,13 @@ To build an object of type :n:`@ident`, one should provide the constructor Definition half := mkRat true 1 2 (O_S 1) one_two_irred. Check half. +.. FIXME: move this to the main grammar in the spec chapter + .. _record-named-fields-grammar: .. productionlist:: - term : {| [`field_def` ; … ; `field_def`] |} - field_def : name [binders] := `term` + record_term : {| [`field_def` ; … ; `field_def`] |} + field_def : name [binders] := `record_term` Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have @@ -152,12 +154,14 @@ It can be activated for printing with Set Printing Projections. Check top half. +.. FIXME: move this to the main grammar in the spec chapter + .. _record_projections_grammar: .. productionlist:: terms - term : term `.` ( qualid ) - : | term `.` ( qualid arg … arg ) - : | term `.` ( @`qualid` `term` … `term` ) + projection : projection `.` ( `qualid` ) + : | projection `.` ( `qualid` `arg` … `arg` ) + : | projection `.` ( @`qualid` `term` … `term` ) Syntax of Record projections -- cgit v1.2.3 From 145da17e8312a7963229e36ef7b1448299357117 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:33:12 -0400 Subject: [doc] Get rid of two Sphinx warnings --- doc/sphinx/conf.py | 3 +++ doc/sphinx/refman-preamble.rst | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 8b29d1e9f9..b85cf57a98 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -316,6 +316,9 @@ latex_elements = { % Style tweaks \newcssclass{sigannot}{\textrm{#1:}} + + % Silence 'LaTeX Warning: Command \nobreakspace invalid in math mode' + \everymath{\def\nobreakspace{\ }} """ } diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index aa581e1ee1..c662028773 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -30,7 +30,7 @@ .. |class_2| replace:: `class`\ :math:`_{2}` .. |Coq| replace:: :smallcaps:`Coq` .. |CoqIDE| replace:: :smallcaps:`CoqIDE` -.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\beta\delta\iota\zeta}}` +.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` .. |Gallina| replace:: :smallcaps:`Gallina` .. |ident_0| replace:: `ident`\ :math:`_{0}` .. |ident_1,1| replace:: `ident`\ :math:`_{1,1}` -- cgit v1.2.3 From f39626edcbd56bd7b05aabe8b60e9af72d27bbfd Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:49:13 -0400 Subject: [doc] Fix a few syntax highlighting issues --- doc/sphinx/addendum/generalized-rewriting.rst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 5eba539e03..403b163196 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -123,10 +123,10 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. .. coqtop:: in - forall (A : Type) (S1 S1’ S2 S2’ : list A), - set_eq A S1 S1’ -> - set_eq A S2 S2’ -> - set_eq A (union A S1 S2) (union A S1’ S2’). + forall (A: Type) (S1 S1' S2 S2': list A), + set_eq A S1 S1' -> + set_eq A S2 S2' -> + set_eq A (union A S1 S2) (union A S1' S2'). The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A`` for all ``A``. @@ -448,7 +448,7 @@ various combinations of properties on relations and morphisms are represented as records and instances of theses classes are put in a hint database. For example, the declaration: -.. coqtop:: in +.. coqdoc:: Add Parametric Relation (x1 : T1) ... (xn : Tn) : (A t1 ... tn) (Aeq t′1 ... t′m) [reflexivity proved by refl] @@ -459,7 +459,7 @@ hint database. For example, the declaration: is equivalent to an instance declaration: -.. coqtop:: in +.. coqdoc:: Instance (x1 : T1) ... (xn : Tn) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) := [Equivalence_Reflexive := refl] -- cgit v1.2.3 From fdc5e750f7b87c1d0d1454bae19c00eec9dabbeb Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 01:49:27 -0400 Subject: [doc] Add another common mistake to the documentation-writing guide --- doc/sphinx/README.rst | 32 +++++++++++++++++++++++++++++++- doc/sphinx/README.template.rst | 32 +++++++++++++++++++++++++++++++- 2 files changed, 62 insertions(+), 2 deletions(-) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 6d5545ec3c..369a3a0db8 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -419,7 +419,7 @@ DO first [ t1 | … | tn ]. -DONT +DON'T .. code:: A tactic of the form: @@ -451,6 +451,36 @@ DON'T Plain quotes produce plain text, without highlighting or cross-references. +Overusing the ``example`` directive +----------------------------------- + +DO + .. code:: + + Here is a useful axiom: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + +DO + .. code:: + + .. example:: Using proof-irrelevance + + If you assume the axiom above, … + +DON'T + .. code:: + + Here is a useful axiom: + + .. example:: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + Tips and tricks =============== diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 73b2e96dcb..86914a71df 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -197,7 +197,7 @@ DO first [ t1 | … | tn ]. -DONT +DON'T .. code:: A tactic of the form: @@ -229,6 +229,36 @@ DON'T Plain quotes produce plain text, without highlighting or cross-references. +Overusing the ``example`` directive +----------------------------------- + +DO + .. code:: + + Here is a useful axiom: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + +DO + .. code:: + + .. example:: Using proof-irrelevance + + If you assume the axiom above, … + +DON'T + .. code:: + + Here is a useful axiom: + + .. example:: + + .. coqdoc:: + + Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. + Tips and tricks =============== -- cgit v1.2.3 From 6ae1a2df419db8f44e11f5c5d4bb5e387d290a64 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 02:19:00 -0400 Subject: [doc] Fix some Sphinx LaTeX warnings and silence others --- doc/sphinx/conf.py | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index b85cf57a98..143309fab5 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -166,6 +166,7 @@ primary_domain = 'coq' # The name of the Pygments (syntax highlighting) style to use. pygments_style = 'sphinx' highlight_language = 'text' +suppress_warnings = ["misc.highlighting_failure"] # A list of ignored prefixes for module index sorting. #modindex_common_prefix = [] -- cgit v1.2.3 From a58c64d545bcfe7d24554575f1ac1b80afe78806 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 15:35:22 -0400 Subject: [doc] Change the name that appears on the first page of the PDF manual --- doc/sphinx/conf.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 143309fab5..d820944301 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -106,7 +106,7 @@ def setup(app): master_doc = "index" # General information about the project. -project = 'Coq' +project = 'The Coq Reference Manual' copyright = '1999-2018, Inria' author = 'The Coq Development Team' -- cgit v1.2.3 From 64c64913c18b871088a7da0a37467a337ea673c4 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 19:02:00 -0400 Subject: [doc] Remove frames around code snippets in the LateX build --- doc/sphinx/conf.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index d820944301..bfd13c536b 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -304,8 +304,9 @@ latex_elements = { 'cmappkg': '', 'papersize': 'letterpaper', 'classoptions': ',openany', # No blank pages - 'polyglossia' : '\\usepackage{polyglossia}', - "preamble": r""" + 'polyglossia': '\\usepackage{polyglossia}', + 'sphinxsetup': 'verbatimwithframe=false', + 'preamble': r""" \usepackage{unicode-math} \usepackage{microtype} -- cgit v1.2.3 From 01e56b8ea3a0e3ba08e8f63d545c01be85b580b6 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 18 May 2018 19:02:24 -0400 Subject: [doc] Add sphinx-html, sphinx-latex, and sphinx-pdf targets --- Makefile.doc | 25 ++++++++++++++++--------- doc/README.md | 2 +- 2 files changed, 17 insertions(+), 10 deletions(-) diff --git a/Makefile.doc b/Makefile.doc index 0dcf9daf27..e4b1d5f43c 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -58,17 +58,24 @@ ifndef QUICK SPHINX_DEPS := coq endif -sphinx: $(SPHINX_DEPS) - $(SHOW)'SPHINXBUILD doc/sphinx' - $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/html - @echo - @echo "Build finished. The HTML pages are in $(SPHINXBUILDDIR)/html." +# sphinx-html and sphinx-latex +sphinx-%: $(SPHINX_DEPS) + $(SHOW)'SPHINXBUILD doc/sphinx ($*)' + $(HIDE)$(SPHINXENV) $(SPHINXBUILD) -b $* \ + $(ALLSPHINXOPTS) doc/sphinx $(SPHINXBUILDDIR)/$* + +sphinx-pdf: sphinx-latex + +$(MAKE) -C $(SPHINXBUILDDIR)/latex + +sphinx: + +$(MAKE) sphinx-html + +$(MAKE) sphinx-pdf doc-html:\ - doc/stdlib/html/index.html sphinx + doc/stdlib/html/index.html sphinx-html doc-pdf:\ - doc/stdlib/Library.pdf + doc/stdlib/Library.pdf sphinx-pdf doc-ps:\ doc/stdlib/Library.ps @@ -181,7 +188,7 @@ install-doc-meta: $(MKDIR) $(FULLDOCDIR) $(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc -install-doc-html: install-doc-stdlib-html install-doc-sphinx +install-doc-html: install-doc-stdlib-html install-doc-sphinx-html install-doc-stdlib-html: $(MKDIR) $(FULLDOCDIR)/html/stdlib @@ -192,7 +199,7 @@ install-doc-printable: $(INSTALLLIB) doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf $(INSTALLLIB) doc/stdlib/Library.ps $(FULLDOCDIR)/ps -install-doc-sphinx: +install-doc-sphinx-html: $(MKDIR) $(FULLDOCDIR)/sphinx (for f in `cd doc/sphinx/_build; find . -type f`; do \ $(MKDIR) $$(dirname $(FULLDOCDIR)/sphinx/$$f);\ diff --git a/doc/README.md b/doc/README.md index 47507de52d..6cfa94b3dc 100644 --- a/doc/README.md +++ b/doc/README.md @@ -80,7 +80,7 @@ Alternatively, you can use some specific targets: to produce all HTML documents - `make sphinx` - to produce the HTML version of the reference manual + to produce the HTML and PDF versions of the reference manual - `make stdlib` to produce all formats of the Coq standard library -- cgit v1.2.3 From 81e55a33d518aa70cef62af3cdf3d6a013960ac6 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Mon, 13 Aug 2018 17:44:36 -0400 Subject: [doc] Move a citation back into the introduction Alternatively, we could duplicate the citation text in both index files. --- doc/sphinx/index.html.rst | 5 ----- doc/sphinx/introduction.rst | 5 +++++ 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index 96ddd27027..9d90857061 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -89,8 +89,3 @@ 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/introduction.rst b/doc/sphinx/introduction.rst index 5bb7bf542c..b8d2f6b6dc 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -35,6 +35,11 @@ are processed from a file. The `coqtop` read-eval-print-loop can also be used directly, for debugging purposes. + .. [#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). + - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact -- cgit v1.2.3 From f3476766cbdfb685b59058a974456348d5365265 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Tue, 14 Aug 2018 17:55:33 -0400 Subject: [doc] Skip unneeded copies in copy_formatspecific_files --- doc/sphinx/conf.py | 28 +++++++++++++--------------- 1 file changed, 13 insertions(+), 15 deletions(-) diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index bfd13c536b..c4f2fb11f3 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -24,6 +24,7 @@ import sys import os +from shutil import copyfile # Increase recursion limit for sphinx sys.setrecursionlimit(1500) @@ -72,31 +73,28 @@ source_suffix = '.rst' # The encoding of source files. #source_encoding = 'utf-8-sig' -import logging -from glob import glob -from shutil import copyfile - # Add extra cases here to support more formats SUPPORTED_FORMATS = ["html", "latex"] -def current_format(app): - for fmt in SUPPORTED_FORMATS: - if app.tags.has(fmt): - 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 readbin(fname): + try: + with open(fname, mode="rb") as f: + return f.read() + except FileNotFoundError: + return None def copy_formatspecific_files(app): - ext = ".{}.rst".format(current_format(app)) + ext = ".{}.rst".format(app.builder.name) 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) + if readbin(src) == readbin(dst): + app.info("Skipping {}: {} is up to date".format(src, dst)) + else: + app.info("Copying {} to {}".format(src, dst)) + copyfile(src, dst) def setup(app): app.connect('builder-inited', copy_formatspecific_files) -- cgit v1.2.3 From 3eebeb6d39340a6e9feabce567f688df0e7270a6 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Wed, 5 Sep 2018 17:24:50 -0400 Subject: [doc] Remove unneeded backslashes in biblio.bib --- doc/sphinx/biblio.bib | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index c74d8f540c..aa8537c92d 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -121,7 +121,7 @@ s}, volume = {7998}, editor = {Sandrine Blazy and Christine Paulin and David Pichardie }, series = {LNCS }, - doi = {10.1007/978-3-642-39634-2\_5 }, + doi = {10.1007/978-3-642-39634-2_5}, year = {2013}, } @@ -136,7 +136,7 @@ s}, pages = {85--95}, month = {November}, year = {2000}, - url = {http://www.lirmm.fr/\%7Edelahaye/papers/ltac\%20(LPAR\%2700).pdf} + url = {http://www.lirmm.fr/%7Edelahaye/papers/ltac%20(LPAR%2700).pdf} } @Article{Dyc92, -- cgit v1.2.3 From 31ac5a2ec8eb71b0bf31c7a5d046f9a9bc366f2e Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Wed, 12 Sep 2018 19:20:32 -0400 Subject: [doc] Replace app.info (deprecated in Sphinx 8.0) with logger.info --- doc/sphinx/conf.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index c4f2fb11f3..b43d5fb6f0 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -25,6 +25,7 @@ import sys import os from shutil import copyfile +import sphinx # Increase recursion limit for sphinx sys.setrecursionlimit(1500) @@ -90,10 +91,11 @@ def copy_formatspecific_files(app): if fname.endswith(ext): src = os.path.join(app.srcdir, fname) dst = os.path.join(app.srcdir, fname[:-len(ext)] + ".rst") + logger = sphinx.util.logging.getLogger(__name__) if readbin(src) == readbin(dst): - app.info("Skipping {}: {} is up to date".format(src, dst)) + logger.info("Skipping {}: {} is up to date".format(src, dst)) else: - app.info("Copying {} to {}".format(src, dst)) + logger.info("Copying {} to {}".format(src, dst)) copyfile(src, dst) def setup(app): -- cgit v1.2.3 From 9320056b8572bc8ac0514a5f72885cbd0d228e87 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 12 Sep 2018 10:40:23 +0200 Subject: Update minimum required dependency versions of Sphinx doc. The minimum required versions of the Sphinx-related (and ANTLR) Python packages for Coq 8.10 were chosen as the lower bound between what is currently in Debian Buster and in NixOS 18.09 Jellyfish (in practice the lower bound was always met by NixOS 18.09 Jellyfish). These minimum required versions were documented. In the docker image used by GitLab CI, we install these Python packages through pip as this allows us to pin them to these specific versions. In Travis, we let them unspecified to always test the latest versions. Finally, we also add the new dependencies of the Sphinx PDF manual. --- .gitlab-ci.yml | 2 +- default.nix | 16 ++-------------- dev/ci/docker/bionic_coq/Dockerfile | 18 ++++++++++++------ doc/README.md | 33 +++++++++++++++++++++------------ 4 files changed, 36 insertions(+), 33 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 0115ac9eff..27d7fbf243 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-09-05-V1" + CACHEKEY: "bionic_coq-V2018-09-20-V2" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/default.nix b/default.nix index 6f759f41d1..88992a30a3 100644 --- a/default.nix +++ b/default.nix @@ -23,8 +23,8 @@ { pkgs ? (import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/4477cf04b6779a537cdb5f0bd3dd30e75aeb4a3b.tar.gz"; - sha256 = "1i39wsfwkvj9yryj8di3jibpdg3b3j86ych7s9rb6z79k08yaaxc"; + url = "https://github.com/NixOS/nixpkgs/archive/947ae71dcec680b5075ece14e38eae64831b9819.tar.gz"; + sha256 = "15nryymfch4fzxk6nacli4gw4cyicpdjwzai5v3bc0azaslww2x5"; }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true @@ -38,18 +38,6 @@ with pkgs; with stdenv.lib; -let dune = - overrideDerivation jbuilder (o: { - name = "dune-1.1.1"; - src = fetchFromGitHub { - owner = "ocaml"; - repo = "dune"; - rev = "1.1.1"; - sha256 = "0v2pnxpmqsvrvidpwxvbsypzhqfdnjs5crjp9y61qi8nyj8d75zw"; - }; - }); -in - stdenv.mkDerivation rec { name = "coq"; diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8b26294d8f..9fad274bf4 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-09-05-V1" +# CACHEKEY: "bionic_coq-V2018-09-20-V2" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -7,13 +7,19 @@ LABEL maintainer="e@x80.org" ENV DEBIAN_FRONTEND="noninteractive" RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ + # Dependencies of the image, the test-suite and external projects m4 automake autoconf time wget rsync git gcc-multilib opam \ + # Dependencies of lablgtk (for CoqIDE) libgtk2.0-dev libgtksourceview2.0-dev \ - texlive-latex-extra texlive-fonts-recommended texlive-science tipa \ - python3-sphinx python3-pexpect python3-sphinx-rtd-theme python3-bs4 python3-sphinxcontrib.bibtex \ - python3-setuptools python3-wheel python3-pip - -RUN pip3 install antlr4-python3-runtime + # Dependencies of stdlib and sphinx doc + texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ + xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \ + # Dependencies of source-doc and coq-makefile + texlive-science tipa + +# More dependencies of the sphinx doc +RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \ + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # Basic OPAM setup ENV NJOBS="2" \ diff --git a/doc/README.md b/doc/README.md index 6cfa94b3dc..cb3427e010 100644 --- a/doc/README.md +++ b/doc/README.md @@ -28,18 +28,18 @@ To produce the complete documentation in HTML, you will need Coq dependencies listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based reference manual requires Python 3, and the following Python packages: - sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime pexpect sphinxcontrib-bibtex + - sphinx >= 1.7.8 + - sphinx_rtd_theme >= 0.2.5b2 + - beautifulsoup4 >= 4.0.6 + - antlr4-python3-runtime >= 4.7.1 + - pexpect >= 4.2.1 + - sphinxcontrib-bibtex >= 0.4.0 -You can install them using `pip3 install` or using your distribution's package -manager. E.g. under recent Debian-based operating systems (Debian 10 "Buster", -Ubuntu 18.04, ...) you can use: +To install them, you should first install pip and setuptools (for instance, +with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run: - apt install python3-sphinx python3-pexpect python3-sphinx-rtd-theme \ - python3-bs4 python3-sphinxcontrib.bibtex python3-pip - -Then, install the missing Python3 Antlr4 package: - - pip3 install antlr4-python3-runtime + pip3 install sphinx sphinx_rtd_theme beautifulsoup4 antlr4-python3-runtime \ + 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 @@ -54,10 +54,19 @@ additional tools are required: - pdflatex - dvips - makeindex + - xelatex + - latexmk + - xindy + +All of them are part of the TexLive distribution. E.g. on Debian / Ubuntu, +install them with: + + apt install texlive-full -Install them using your package manager. E.g. on Debian / Ubuntu: +Or if you want to use less disk space: - apt install texlive-latex-extra texlive-fonts-recommended + apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \ + latexmk xindy Compilation ----------- -- cgit v1.2.3 From d54ed424bf0c73f6341cdb22130739011af4a356 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 19 Sep 2018 13:45:01 +0200 Subject: Fix race condition. --- Makefile.doc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.doc b/Makefile.doc index e4b1d5f43c..788e4e61e7 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -67,7 +67,7 @@ sphinx-%: $(SPHINX_DEPS) sphinx-pdf: sphinx-latex +$(MAKE) -C $(SPHINXBUILDDIR)/latex -sphinx: +sphinx: $(SPHINX_DEPS) +$(MAKE) sphinx-html +$(MAKE) sphinx-pdf -- cgit v1.2.3 From 5b01a356f1905af64353a5b60ec377df316d183a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 19 Sep 2018 13:55:48 +0200 Subject: Mention PDF doc in CHANGES. --- CHANGES | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGES b/CHANGES index 1bf0e0edd4..453d82758a 100644 --- a/CHANGES +++ b/CHANGES @@ -215,6 +215,10 @@ Notations Changes from 8.8.1 to 8.8.2 =========================== +Documentation + +- A PDF version of the reference manual is available once again. + Tools - The coq-makefile targets `print-pretty-timed`, `print-pretty-timed-diff`, -- cgit v1.2.3 From 968a72b6bc481916a67a2825d1fc245a2bb0071e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 20 Sep 2018 15:58:33 +0200 Subject: Stop building LaTeX doc in Travis (keep HTML). The LaTeX doc is already tested in GitLab CI and finding the right dependencies in this older version of Ubuntu is a hurdle. --- .travis.yml | 21 ++++++--------------- 1 file changed, 6 insertions(+), 15 deletions(-) diff --git a/.travis.yml b/.travis.yml index dd28410bec..766c76c29c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -105,8 +105,8 @@ matrix: # Full Coq test-suite with two compilers - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" - - EXTRA_CONF="-coqide opt -with-doc yes" + - TEST_TARGET="doc-html test-suite" + - EXTRA_CONF="-coqide opt" - EXTRA_OPAM="${LABLGTK} ounit" before_install: &sphinx-install - sudo pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex @@ -119,26 +119,17 @@ matrix: - aspcud - libgtk2.0-dev - libgtksourceview2.0-dev - - texlive-latex-base - - texlive-latex-recommended - - texlive-latex-extra - - texlive-math-extra - - texlive-fonts-recommended - - texlive-fonts-extra - - latex-xcolor - - ghostscript - - tipa - python3 - python3-pip - python3-setuptools - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" + - TEST_TARGET="doc-html test-suite" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-coqide opt -with-doc yes" + - EXTRA_CONF="-coqide opt" - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install addons: @@ -150,11 +141,11 @@ matrix: # Full test-suite with flambda - if: NOT (type = pull_request) env: - - TEST_TARGET="test-suite" + - TEST_TARGET="doc-html test-suite" - COMPILER="${COMPILER_BE}+flambda" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" + - EXTRA_CONF="-coqide opt -flambda-opts -O3" - EXTRA_OPAM="${LABLGTK_BE} ounit" before_install: *sphinx-install addons: -- cgit v1.2.3