diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/README.md | 11 | ||||
| -rw-r--r-- | doc/sphinx/README.rst | 37 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 4 | ||||
| -rw-r--r-- | doc/sphinx/credits-contents.rst (renamed from doc/sphinx/credits.rst) | 0 | ||||
| -rw-r--r-- | doc/sphinx/credits-wrapper.latex.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/credits.html.rst (renamed from doc/sphinx/credits-wrapper.html.rst) | 2 | ||||
| -rw-r--r-- | doc/sphinx/credits.latex.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/index.html.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/index.latex.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 5 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 26 |
11 files changed, 61 insertions, 51 deletions
diff --git a/doc/README.md b/doc/README.md index 1461fa2e2c..3db1261656 100644 --- a/doc/README.md +++ b/doc/README.md @@ -88,8 +88,11 @@ Alternatively, you can use some specific targets: - `make doc-html` to produce all HTML documents -- `make sphinx` - to produce the HTML and PDF versions of the reference manual +- `make refman` + to produce the HTML and PDF versions of the reference manual + +- `make refman-{html,pdf}` + to produce only one format of the reference manual - `make stdlib` to produce all formats of the Coq standard library @@ -103,12 +106,12 @@ to avoid treating Sphinx warnings as errors. Otherwise, Sphinx quits upon detecting the first warning. You can set this on the Sphinx `make` command line or as an environment variable: -- `make sphinx SPHINXWARNERROR=0` +- `make refman SPHINXWARNERROR=0` - ~~~ export SPHINXWARNERROR=0 ⋮ - make sphinx + make refman ~~~ Installation diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index c1f3f7b4d0..4ad952bdfb 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -114,32 +114,23 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica Raised if :n:`@tactic` does not fully solve the goal. -``.. flag::`` :black_nib: A Coq flag (i.e a binary-valued setting). +``.. flag::`` :black_nib: A Coq flag (i.e. a boolean setting). Example:: .. flag:: Nonrecursive Elimination Schemes - This option controls whether types declared with the keywords - :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + Controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of induction principles. -``.. opt::`` :black_nib: A Coq option (with a string or numeric value; use "flag" for binary options) +``.. opt::`` :black_nib: A Coq option (a setting with non-boolean value, e.g. a string or numeric value). Example:: - .. opt:: Printing Width @num - :name: Printing Width + .. opt:: Hyps Limit @num + :name Hyps Limit - This command sets which left-aligned part of the width of the screen is used - for display. At the time of writing this documentation, the default value - is 78. - -``.. table::`` :black_nib: A Coq table (i.e a setting whose value is a set). - Example:: - - .. table:: Search Blacklist @string - :name: Search Blacklist - - This table controls ... + Controls the maximum number of hypotheses displayed in goals after + application of a tactic. ``.. prodn::`` A grammar production. This is useful if you intend to document individual grammar productions. @@ -159,6 +150,14 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica .. prodn:: term += let: @pattern := @term in @term .. prodn:: occ_switch ::= { {? + %| - } {* @num } } +``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values. + Example:: + + .. table:: Search Blacklist @string + :name: Search Blacklist + + Controls ... + ``.. tacn::`` :black_nib: A tactic, or a tactic notation. Example:: @@ -293,7 +292,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo \WTEG{\forall~x:T,U}{\Prop} ``.. preamble::`` A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The + contents of the TeX file are wrapped in a math environment, as MathJax + doesn't process LaTeX definitions otherwise. Usage:: diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index b43d5fb6f0..71f01cbb17 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 = 'The Coq Reference Manual' +project = 'Coq' copyright = '1999-2018, Inria' author = 'The Coq Development Team' @@ -335,7 +335,7 @@ latex_additional_files = [ "_static/coqnotations.sty" ] -latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')] +latex_documents = [('index', 'CoqRefMan.tex', 'The Coq Reference Manual', author, 'manual')] # The name of an image file (relative to this directory) to place at the top of # the title page. diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits-contents.rst index 212f0a65b0..212f0a65b0 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits-contents.rst diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst deleted file mode 100644 index 9f7dd49af8..0000000000 --- a/doc/sphinx/credits-wrapper.latex.rst +++ /dev/null @@ -1,3 +0,0 @@ -.. _credits: - -.. include:: credits.rst diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits.html.rst index 2d35a12dc2..0b2b1c6ad1 100644 --- a/doc/sphinx/credits-wrapper.html.rst +++ b/doc/sphinx/credits.html.rst @@ -4,4 +4,4 @@ Credits ------- -.. include:: credits.rst +.. include:: credits-contents.rst diff --git a/doc/sphinx/credits.latex.rst b/doc/sphinx/credits.latex.rst new file mode 100644 index 0000000000..39101f9d52 --- /dev/null +++ b/doc/sphinx/credits.latex.rst @@ -0,0 +1,3 @@ +.. _credits: + +.. include:: credits-contents.rst diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst index 9d90857061..cf12b57414 100644 --- a/doc/sphinx/index.html.rst +++ b/doc/sphinx/index.html.rst @@ -1,11 +1,8 @@ -========================== - The Coq Reference Manual -========================== - .. _introduction: +========================== Introduction ------------- +========================== .. include:: introduction.rst @@ -28,7 +25,7 @@ Table of contents :caption: Preamble self - credits-wrapper + credits .. toctree:: :caption: The language @@ -89,3 +86,8 @@ 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 index 0f2f7b4897..af757f8746 100644 --- a/doc/sphinx/index.latex.rst +++ b/doc/sphinx/index.latex.rst @@ -7,10 +7,15 @@ Introduction .. include:: introduction.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). + Credits ------- -.. include:: credits-wrapper.rst +.. include:: credits.rst License ------- diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index b8d2f6b6dc..5bb7bf542c 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -35,11 +35,6 @@ 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 diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 7992c10abb..edf4e6ec9d 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -333,14 +333,15 @@ class TacticNotationVariantObject(TacticNotationObject): annotation = "Variant" class OptionObject(NotationObject): - """A Coq option. + """A Coq option (a setting with non-boolean value, e.g. a string or numeric value). Example:: .. opt:: Hyps Limit @num + :name Hyps Limit - This option controls the maximum number of hypotheses displayed in goals after - the application of a tactic. + Controls the maximum number of hypotheses displayed in goals after + application of a tactic. """ subdomain = "opt" index_suffix = "(opt)" @@ -351,14 +352,14 @@ class OptionObject(NotationObject): class FlagObject(NotationObject): - """A Coq flag, i.e. a boolean Option. + """A Coq flag (i.e. a boolean setting). Example:: .. flag:: Nonrecursive Elimination Schemes - This flag controls whether types declared with the keywords - :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + Controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of induction principles. """ subdomain = "flag" @@ -374,9 +375,10 @@ class TableObject(NotationObject): Example:: - .. table:: Search Blacklist + .. table:: Search Blacklist @string + :name: Search Blacklist - This table controls ... + Controls ... """ subdomain = "table" index_suffix = "(table)" @@ -664,7 +666,9 @@ class ExampleDirective(BaseAdmonition): class PreambleDirective(Directive): r"""A reST directive to include a TeX file. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s. + Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The + contents of the TeX file are wrapped in a math environment, as MathJax + doesn't process LaTeX definitions otherwise. Usage:: @@ -691,7 +695,7 @@ class PreambleDirective(Directive): with open(abs_fname, encoding="utf-8") as ltx: latex = ltx.read() - node = make_math_node(latex, env.docname, nowrap=True) + node = make_math_node(latex, env.docname, nowrap=False) node['classes'] = ["math-preamble"] set_source_info(self, node) return [node] @@ -1192,6 +1196,6 @@ def setup(app): # contents of ``env.domaindata['coq']`` change. See # `https://github.com/sphinx-doc/sphinx/issues/4460`. meta = { "version": "0.1", - "env_version": 1, + "env_version": 2, "parallel_read_safe": True } return meta |