diff options
33 files changed, 1002 insertions, 483 deletions
diff --git a/.travis.yml b/.travis.yml index 44d24eaa2..890ee6d7c 100644 --- a/.travis.yml +++ b/.travis.yml @@ -93,39 +93,24 @@ matrix: - TEST_TARGET="ci-equations" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-geocoq" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-fcsl-pcm" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-fiat-crypto" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-fiat-parsers" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-flocq" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-formal-topology" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-hott" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-iris-lambda-rust" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-ltac2" - if: NOT (type = pull_request) env: - TEST_TARGET="ci-math-classes" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-math-comp" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-mtac2" - if: NOT (type = pull_request) env: @@ -133,12 +118,6 @@ matrix: - if: NOT (type = pull_request) env: - TEST_TARGET="ci-sf" - - if: NOT (type = pull_request) - env: - - TEST_TARGET="ci-unimath" - - if: NOT (type = pull_request) - env: - - TEST_TARGET="ci-vst" - env: - TEST_TARGET="lint" diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index b7faea13e..5c882ee85 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -11,6 +11,8 @@ ######################################################################## : "${mathcomp_CI_BRANCH:=master}" : "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}" +: "${oddorder_CI_BRANCH:=master}" +: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order.git}" ######################################################################## # UniMath diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 2a14ed352..f867fd189 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -71,11 +71,6 @@ git_checkout() echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) } -checkout_mathcomp() -{ - git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}" -} - make() { # +x: add x only if defined @@ -93,7 +88,8 @@ install_ssreflect() { echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - checkout_mathcomp "${mathcomp_CI_DIR}" + git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" + ( cd "${mathcomp_CI_DIR}/mathcomp" && \ sed -i.bak '/ssrtest/d' Make && \ sed -i.bak '/odd_order/d' Make && \ diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index 845addb4c..f8d811bef 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -6,6 +6,9 @@ ci_dir="$(dirname "$0")" fiat_crypto_CI_DIR="${CI_BUILD_DIR}/fiat-crypto" git_checkout "${fiat_crypto_CI_BRANCH}" "${fiat_crypto_CI_GITURL}" "${fiat_crypto_CI_DIR}" + ( cd "${fiat_crypto_CI_DIR}" && git submodule update --init --recursive ) -( cd "${fiat_crypto_CI_DIR}" && make lite lite-display ) +fiat_crypto_CI_TARGETS="lite lite-display" + +( cd "${fiat_crypto_CI_DIR}" && make ${fiat_crypto_CI_TARGETS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index bd1d88993..920272bcf 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -7,6 +7,4 @@ GeoCoq_CI_DIR="${CI_BUILD_DIR}/GeoCoq" git_checkout "${GeoCoq_CI_BRANCH}" "${GeoCoq_CI_GITURL}" "${GeoCoq_CI_DIR}" -( cd "${GeoCoq_CI_DIR}" && \ - ./configure-ci.sh && \ - make ) +( cd "${GeoCoq_CI_DIR}" && ./configure.sh && make ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index 8c6b910bb..20328baf2 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -5,11 +5,10 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" +oddorder_CI_DIR="${CI_BUILD_DIR}/odd-order" -checkout_mathcomp "${mathcomp_CI_DIR}" +git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}" +git_checkout "${oddorder_CI_BRANCH}" "${oddorder_CI_GITURL}" "${oddorder_CI_DIR}" -# odd_order takes too much time for travis. -( cd "${mathcomp_CI_DIR}/mathcomp" && \ - sed -i.bak '/PFsection/d' Make && \ - sed -i.bak '/stripped_odd_order_theorem/d' Make && \ - make Makefile.coq && make -f Makefile.coq all ) +( cd "${mathcomp_CI_DIR}/mathcomp" && make && make install ) +( cd "${oddorder_CI_DIR}/" && make ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh index 62a949f59..aa20fe1ff 100755 --- a/dev/ci/ci-unimath.sh +++ b/dev/ci/ci-unimath.sh @@ -7,7 +7,4 @@ UniMath_CI_DIR="${CI_BUILD_DIR}/UniMath" git_checkout "${UniMath_CI_BRANCH}" "${UniMath_CI_GITURL}" "${UniMath_CI_DIR}" -( cd "${UniMath_CI_DIR}" && \ - sed -i.bak '/Folds/d' Makefile && \ - sed -i.bak '/HomologicalAlgebra/d' Makefile && \ - make BUILD_COQ=no ) +( cd "${UniMath_CI_DIR}" && make BUILD_COQ=no ) diff --git a/dev/ci/ci-vst.sh b/dev/ci/ci-vst.sh index 79001c547..7a097eaab 100755 --- a/dev/ci/ci-vst.sh +++ b/dev/ci/ci-vst.sh @@ -5,9 +5,6 @@ ci_dir="$(dirname "$0")" VST_CI_DIR="${CI_BUILD_DIR}/VST" -# opam install -j ${NJOBS} -y menhir git_checkout "${VST_CI_BRANCH}" "${VST_CI_GITURL}" "${VST_CI_DIR}" -# We have to omit progs as otherwise we timeout on Travis; on Gitlab -# we will be able to just use `make` -( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true -o progs ) +( cd "${VST_CI_DIR}" && make IGNORECOQVERSION=true ) diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 9dd12087a..70a9756e5 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -23,7 +23,7 @@ ;; If you load this file from a git repository, checking out an old ;; commit will make it disappear and cause errors for your Emacs -;; startup. To ignore those errors use (require 'coqdev nil t). If you +;; startup. To ignore those errors use (require 'coqdev nil t). If you ;; check out a malicious commit Emacs startup would allow it to run ;; arbitrary code, to avoid this you can copy coqdev.el to any ;; location and adjust the load path accordingly (of course if you run @@ -115,5 +115,36 @@ This does not enable `bug-reference-mode'." (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s")))) (add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode) +(defun coqdev-sphinx-quote-coq-refman-region (left right &optional offset beg end) + "Add LEFT and RIGHT around the BEG..END. +Leave the point after RIGHT. BEG and END default to the bounds +of the current region. Leave point OFFSET characters after the +left quote (if OFFSET is nil, leave the point after the right +quote)." + (unless beg + (if (region-active-p) + (setq beg (region-beginning) end (region-end)) + (setq beg (point) end nil))) + (save-excursion + (goto-char (or end beg)) + (insert right)) + (save-excursion + (goto-char beg) + (insert left)) + (if (and end (not offset)) ;; Second test handles the ::`` case + (goto-char (+ end (length left) (length right))) + (goto-char (+ beg (or offset (length left)))))) + +(defun coqdev-sphinx-rst-coq-action () + "Insert a Sphinx role template or quote the current region." + (interactive) + (pcase (read-char "Command [gntm:`]?") + (?g (coqdev-sphinx-quote-coq-refman-region ":g:`" "`")) + (?n (coqdev-sphinx-quote-coq-refman-region ":n:`" "`")) + (?t (coqdev-sphinx-quote-coq-refman-region ":token:`" "`")) + (?m (coqdev-sphinx-quote-coq-refman-region ":math:`" "`")) + (?: (coqdev-sphinx-quote-coq-refman-region "::`" "`" 1)) + (?` (coqdev-sphinx-quote-coq-refman-region "``" "``")))) + (provide 'coqdev) ;;; coqdev ends here diff --git a/doc/sphinx/MIGRATING b/doc/sphinx/MIGRATING deleted file mode 100644 index fa6fe1537..000000000 --- a/doc/sphinx/MIGRATING +++ /dev/null @@ -1,238 +0,0 @@ -How to migrate the Coq Reference Manual to Sphinx -================================================= - -# Install Python3 packages (requires Python 3, python3-pip, python3-setuptools) - - * pip3 install bs4 sphinx sphinx_rtd_theme pexpect antlr4-python3-runtime sphinxcontrib-bibtex - -# You may want to do this under a virtualenv, particularly if you end up with issues finding sphinxcontrib.bibtex. http://docs.python-guide.org/en/latest/dev/virtualenvs/ - - * pip3 install virtualenv - * virtualenv coqsphinxing # you may want to use -p to specify the python version - * source coqsphinxing/bin/activate # activate the virtual environment - -# After activating the virtual environment you can run the above pip3 command to install sphinx. You will have to activate the virtual environment before building the docs in your session. - -# Add this Elisp code to .emacs, if you're using emacs (recommended): - - (defun sphinx/quote-coq-refman-region (left right &optional beg end count) - (unless beg - (if (region-active-p) - (setq beg (region-beginning) end (region-end)) - (setq beg (point) end nil))) - (unless count - (setq count 1)) - (save-excursion - (goto-char (or end beg)) - (dotimes (_ count) (insert right))) - (save-excursion - (goto-char beg) - (dotimes (_ count) (insert left))) - (if (and end (characterp left)) ;; Second test handles the ::`` case - (goto-char (+ (* 2 count) end)) - (goto-char (+ count beg)))) - - (defun sphinx/coqtop (beg end) - (interactive (list (region-beginning) (region-end))) - (replace-regexp "^Coq < " " " nil beg end) - (indent-rigidly beg end -3) - (goto-char beg) - (insert ".. coqtop:: all\n\n")) - - (defun sphinx/rst-coq-action () - (interactive) - (pcase (read-char "Command?") - (?g (sphinx/quote-coq-refman-region ":g:`" "`")) - (?n (sphinx/quote-coq-refman-region ":n:`" "`")) - (?t (sphinx/quote-coq-refman-region ":token:`" "`")) - (?m (sphinx/quote-coq-refman-region ":math:`" "`")) - (?: (sphinx/quote-coq-refman-region "::`" "`")) - (?` (sphinx/quote-coq-refman-region "``" "``")) - (?c (sphinx/coqtop (region-beginning) (region-end))))) - - (global-set-key (kbd "<f12>") #'sphinx/rst-coq-action) - - With this code installed, you can hit "F12" followed by an appropriate key to do quick markup of text - (this will make more sense once you've started editing the text). - -# Fork the Coq repo, if needed: - - https://github.com/coq/coq - -# Clone the repo to your work machine - -# Add Maxime Dénès's repo as a remote: - - git remote add sphinx https://github.com/maximedenes/coq.git - - (or choose a name other than "sphinx") - - Verify with: - - git remote -v - -# Fetch from the remote - - git fetch sphinx - -# Checkout the sphinx-doc branch - - git checkout sphinx-doc - - You should pull from the repo from time to time to keep your local copy up-to-date: - - git pull sphinx sphinx-doc - - You may want to create a new branch to do your work in. - -# Choose a Reference Manual chapter to work on at - - https://docs.google.com/document/d/1Yo7dV4OI0AY9Di-lsEQ3UTmn5ygGLlhxjym7cTCMCWU - -# For each chapter, raw ReStructuredText (the Sphinx format), created by the "html2rest" utility, - is available in the directory porting/raw-rst/ - - Elsewhere, depending on the chapter, there should be an almost-empty template file already created, - which is in the location where the final version should go - -# Manually edit the .rst file, place it in the correct location - - There are small examples in sphinx/porting/, a larger example in language/gallina-extensions.rst - - (N.B.: the migration is a work-in-progress, your suggestions are welcome) - - Find the chapter you're working on from the online manual at https://coq.inria.fr/distrib/current/refman/. - At the top of the file, after the chapter heading, add: - - :Source: https://coq.inria.fr/distrib/current/refman/the-chapter-file.html - :Converted by: Your Name - - N.B.: These source and converted-by annotations should help for the migration phase. Later on, - those annotations will be removed, and contributors will be mentioned in the Coq credits. - - Remove chapter numbers - - Replace section, subsection numbers with reference labels: - - .. _some-reference-label: - - Place the label before the section or subsection, followed by a blank line. - - Note the leading underscore. Use :ref:`some_reference-label` to refer to such a label; note the leading underscore is omitted. - Many cross-references may be to other chapters. If the required label exists, use it. Otherwise, use a dummy reference of the form - `TODO-n.n.n-mnemonic` we can fixup later. Example: - - :ref:`TODO-1.3.2-definitions` - - We can grep for those TODOs, and the existing subsection number makes it easy to find in the exisyting manual. - - For the particular case of references to chapters, we can use a -convention for the cross-reference name, so no TODO is needed. - - :ref:`thegallinaspecificationlanguage` - -That is, the chapter label is the chapter title, all in lower-case, -with no spaces or punctuation. For chapters with subtitles marked with -a ":", like those for Omega and Nsatz, use just the chapter part -preceding the ":". These labels should already be in the -placeholder .rst files for each chapter. - - - You can also label other items, like grammars, with the same syntax. To refer to such labels, not involving a - section or subsection, use the syntax - - :ref:`Some link text <label-name>` - - Yes, the angle-brackets are needed here! - - For bibliographic references (those in biblio.bib), use :cite:`thecitation`. - - Grammars will get mangled by the translation. Look for "productionlist" in the examples, also see - http://www.sphinx-doc.org/en/stable/markup/para.html. - - For Coq examples that appear, look at the "coqtop" syntax in porting/tricky-bits.rst. The Sphinx - script will run coqtop on those examples, and can show the output (or not). - - The file replaces.rst contains replacement definitions for some items that are clumsy to write out otherwise. - Use - - .. include:: replaces.rst - - to gain access to those definitions in your file (you might need a path prefix). Some especially-important - replacements are |Cic|, |Coq|, |CoqIDE|, and |Gallina|, which display those names in small-caps. Please use them, - so that they're rendered consistently. - - Similarly, there are some LaTeX macros in preamble.rst that can be useful. - - Conventions: - - - Keywords and other literal text is double-backquoted (e.g. ``Module``, ``Section``, ``(``, ``,``). - - - Metavariables are single-backquotes (e.g. `term`, `ident`) - - - Use the cmd directive for Vernacular commands, like: - - .. cmd:: Set Printing All. - - Within this directive, prefix metavariables (ident, term) with @: - - .. cmd:: Add Printing Let @ident. - - There's also the "cmdv" directive for variants of a command. - - - Use the "exn" and "warn" directives for errors and warnings: - - .. exn:: Something's not right. - .. warn:: You shouldn't do that. - - - Use the "example" directive for examples - - - Use the "g" role for inline Gallina, like :g:`fun x => x` - - - Use code blocks for blocks of Gallina. You can use a double-colon at the end of a line:: - - your code here - - which prints a single colon, or put the double-colon on a newline. - -:: - - your other code here - -# Making changes to the text - - The goal of the migration is simply to change the storage format from LaTeX to ReStructuredText. The goal is not - to make any organizational or other substantive changes to the text. If you do notice nits (misspellings, wrong - verb tense, and so on), please do change them. For example, the programming language that Coq is written in is these days - called "OCaml", and there are mentions of the older name "Objective Caml" in the reference manual that should be changed. - -# Build, view the manual - - In the root directory of your local repo, run "make sphinx". You can view the result in a browser by loading the HTML file - associated with your chapter, which will be contained in the directory doc/sphinx/_build/html/ beneath the repo root directory. - Make any changes you need until there are no build warnings and the output is perfect. :-) - -# Creating pull requests - - When your changes are done, commit them, push to your fork: - - git commit -m "useful commit message" file - git push origin sphinx-doc - - (or push to another branch, if you've created one). Then go to your GitHub - fork and create a pull request against Maxime's sphinx-doc - branch. If your commit is recent, you should see a link on your - fork's code page to do that. Otherwise, you may need to go to your - branch on GitHub to do that. - -# Issues/Questions/Suggestions - - As the migration proceeds, if you have technical issues, have a more general question, or want to suggest something, please contact: - - Paul Steckler <steck@stecksoft.com> - Maxime Dénès <maxime.denes@inria.fr> - -# Issues - - Should the stuff in replaces.rst go in preamble.rst? - In LaTeX, some of the grammars add productions to existing nonterminals, like term ++= ... . How to indicate that? diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst new file mode 100644 index 000000000..5f2f21f2b --- /dev/null +++ b/doc/sphinx/README.rst @@ -0,0 +1,325 @@ +============================= + Documenting Coq with Sphinx +============================= + +.. + README.rst is auto-generated from README.template.rst and the coqrst docs; + use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + +Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. + +In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* — a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc. —, some custom *directives*, and a few custom *roles*. Finally, this manual uses a small DSL to describe tactic invocations and commands. + +Coq objects +=========== + +Our Coq domain define multiple `objects`_. Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object). The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise:: + + .. tacv:: simpl @pattern at {+ @num} + :name: simpl_at + + This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + matching :n:`@pattern` in the current goal. + + .. exn:: Too few occurrences + +Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```. + +Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a ``:name:`` option, as shown above. + +- Options, errors, warnings have their name set to their signature, with ``...`` replacing all notation bits. For example, the auto-generated name of ``.. exn:: @qualid is not a module`` is ``... is not a module``, and a link to it would take the form ``:exn:`... is not a module```. +- Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. +- Vernac variants, tactic notations, and tactic variants do not have a default name. + +Notations +--------- + +The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_): + +``@…`` + A placeholder (``@ident``, ``@num``, ``@tactic``\ …) + +``{? …}`` + an optional block + +``{* …}``, ``{+ …}`` + an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces + +``{*, …}``, ``{+, …}`` + an optional or mandatory repeatable block, with repetitions separated by commas + +``%|``, ``%{``, … + an escaped character (rendered without the leading ``%``) + +.. + FIXME document the new subscript support + +As an exercise, what do the following patterns mean? + +.. code:: + + pattern {+, @term {? at {+ @num}}} + generalize {+, @term at {+ @num} as @ident} + fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)} + +Objects +------- + +Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL): + +``.. cmd::`` :black_nib: A Coq command. + Example:: + + .. cmd:: Infix "@symbol" := @term ({+, @modifier}). + + This command is equivalent to :n:`…`. + +``.. cmdv::`` :black_nib: A variant of a Coq command. + Example:: + + .. cmd:: Axiom @ident : @term. + + This command links :token:`term` to the name :token:`term` as its specification in + the global context. The fact asserted by :token:`term` is thus assumed as a + postulate. + + .. cmdv:: Parameter @ident : @term. + + This is equivalent to :n:`Axiom @ident : @term`. + +``.. exn::`` :black_nib: An error raised by a Coq command or tactic. + This commonly appears nested in the ``.. tacn::`` that raises the + exception. + + Example:: + + .. tacv:: assert @form by @tactic + + This tactic applies :n:`@tactic` to solve the subgoals generated by + ``assert``. + + .. exn:: Proof is not complete + + Raised if :n:`@tactic` does not fully solve the goal. + +``.. opt::`` :black_nib: A Coq option. + Example:: + + .. opt:: Nonrecursive Elimination Schemes + + This option controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + induction principles. + +``.. prodn::`` :black_nib: Grammar productions. + This is useful if you intend to document individual grammar productions. + Otherwise, use Sphinx's `production lists + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. + +``.. tacn::`` :black_nib: A tactic, or a tactic notation. + Example:: + + .. tacn:: do @num @expr + + :token:`expr` is evaluated to ``v`` which must be a tactic value. … + +``.. tacv::`` :black_nib: A variant of a tactic. + Example:: + + .. tacn:: fail + + This is the always-failing tactic: it does not solve any goal. It is + useful for defining other tacticals since it can be caught by + :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching + tacticals. … + + .. tacv:: fail @natural + + The number is the failure level. If no level is specified, it + defaults to 0. … + +``.. thm::`` A theorem. + Example:: + + .. thm:: Bound on the ceiling function + + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. + +``.. warn::`` :black_nib: An warning raised by a Coq command or tactic.. + Do not mistake this for ``.. warning::``; this directive is for warning + messages produced by Coq. + + + Example:: + + .. warn:: Ambiguous path + + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored. + +Coq directives +============== + +In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives: + +``.. coqtop::`` A reST directive to describe interactions with Coqtop. + Usage:: + + .. coqtop:: options… + + Coq code to send to coqtop + + Example:: + + .. coqtop:: in reset undo + + Print nat. + Definition a := 1. + + Here is a list of permissible options: + + - Display options + + - ``all``: Display input and output + - ``in``: Display only input + - ``out``: Display only output + - ``none``: Display neither (useful for setup commands) + + - Behavior options + + - ``reset``: Send a ``Reset Initial`` command before running this block + - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after + running all the commands in this block + + ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks + of the same document (``coqrst`` creates a single ``coqtop`` process per + reST source file). Use the ``reset`` option to reset Coq's state. + +``.. coqdoc::`` A reST directive to display Coqtop-formatted source code. + Usage:: + + .. coqdoc:: + + Coq code to highlight + + Example:: + + .. coqdoc:: + + Definition test := 1. + +``.. example::`` A reST directive for examples. + This behaves like a generic admonition; see + http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition + for more details. + + Example:: + + .. example:: Adding a hint to a database + + The following adds ``plus_comm`` to the ``plu`` database: + + .. coqdoc:: + + Hint Resolve plus_comm : plu. + +``.. inference::`` A reST directive to format inference rules. + This also serves as a small illustration of the way to create new Sphinx + directives. + + Usage:: + + .. inference:: name + + newline-separated premisses + ------------------------ + conclusion + + Example:: + + .. inference:: Prod-Pro + + \WTEG{T}{s} + s \in \Sort + \WTE{\Gamma::(x:T)}{U}{\Prop} + ----------------------------- + \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. + + Example:: + + .. preamble:: + + \newcommand{\paren}[#1]{\left(#1\right)} + +Coq roles +========= + +In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles: + +``:g:`` Coq code. + Use this for Gallina and Ltac snippets:: + + :g:`apply plus_comm; reflexivity` + :g:`Set Printing All.` + :g:`forall (x: t), P(x)` + +``:n:`` Any text using the notation syntax (``@id``, ``{+, …}``, etc.). + Use this to explain tactic equivalences. For example, you might write + this:: + + :n:`generalize @term as @ident` is just like :n:`generalize @term`, but + it names the introduced hypothesis :token:`ident`. + + Note that this example also uses ``:token:``. That's because ``ident`` is + defined in the the Coq manual as a grammar production, and ``:token:`` + creates a link to that. When referring to a placeholder that happens to be + a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```. + +``:production:`` A grammar production not included in a ``productionlist`` directive. + Useful to informally introduce a production, as part of running text. + + Example:: + + :production:`string` indicates a quoted string. + + You're not likely to use this role very commonly; instead, use a + `production list + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_ + and reference its tokens using ``:token:`…```. + +Tips and tricks +=============== + +Nested lemmas +------------- + +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: + + .. coqtop:: all + + Lemma l1: 1 + 1 = 2. + + .. coqtop:: all + + Lemma l2: 2 + 2 <> 1. + +Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. + +Abbreviations and macros +------------------------ + +Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_. + +Emacs +----- + +The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function. + +Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``:: + + (with-eval-after-load 'rst + (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action)) diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst new file mode 100644 index 000000000..203251abf --- /dev/null +++ b/doc/sphinx/README.template.rst @@ -0,0 +1,117 @@ +============================= + Documenting Coq with Sphinx +============================= + +.. + README.rst is auto-generated from README.template.rst and the coqrst docs; + use ``doc/tools/coqrst/regen_readme.py`` to rebuild it. + +Coq's reference manual is written in `reStructuredText <http://www.sphinx-doc.org/en/master/usage/restructuredtext/basics.html>`_ (“reST”), and compiled with `Sphinx <http://www.sphinx-doc.org/en/master/>`_. + +In addition to standard reST directives (a directive is similar to a LaTeX environment) and roles (a role is similar to a LaTeX command), the ``coqrst`` plugin loaded by the documentation uses a custom *Coq domain* — a set of Coq-specific directives that define *objects* like tactics, commands (vernacs), warnings, etc. —, some custom *directives*, and a few custom *roles*. Finally, this manual uses a small DSL to describe tactic invocations and commands. + +Coq objects +=========== + +Our Coq domain define multiple `objects`_. Each object has a *signature* (think *type signature*), followed by an optional body (a description of that object). The following example defines two objects: a variant of the ``simpl`` tactic, and an error that it may raise:: + + .. tacv:: simpl @pattern at {+ @num} + :name: simpl_at + + This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms + matching :n:`@pattern` in the current goal. + + .. exn:: Too few occurrences + +Objects are automatically collected into indices, and can be linked to using the role version of the object's directive. For example, you could link to the tactic variant above using ``:tacv:`simpl_at```, and to its exception using ``:exn:`Too few occurrences```. + +Names (link targets) are auto-generated for most simple objects, though they can always be overwritten using a ``:name:`` option, as shown above. + +- Options, errors, warnings have their name set to their signature, with ``...`` replacing all notation bits. For example, the auto-generated name of ``.. exn:: @qualid is not a module`` is ``... is not a module``, and a link to it would take the form ``:exn:`... is not a module```. +- Vernacs (commands) have their name set to the first word of their signature. For example, the auto-generated name of ``Axiom @ident : @term`` is ``Axiom``, and a link to it would take the form ``:cmd:`Axiom```. +- Vernac variants, tactic notations, and tactic variants do not have a default name. + +Notations +--------- + +The signatures of most objects can be written using a succinct DSL for Coq notations (think regular expressions written with a Lispy syntax). A typical signature might look like ``Hint Extern @num {? @pattern} => @tactic``, which means that the ``Hint Extern`` command takes a number (``num``), followed by an optional pattern, and a mandatory tactic. The language has the following constructs (the full grammar is in `TacticNotations.g </doc/tools/coqrst/notations/TacticNotations.g>`_): + +``@…`` + A placeholder (``@ident``, ``@num``, ``@tactic``\ …) + +``{? …}`` + an optional block + +``{* …}``, ``{+ …}`` + an optional (``*``) or mandatory (``+``) block that can be repeated, with repetitions separated by spaces + +``{*, …}``, ``{+, …}`` + an optional or mandatory repeatable block, with repetitions separated by commas + +``%|``, ``%{``, … + an escaped character (rendered without the leading ``%``) + +.. + FIXME document the new subscript support + +As an exercise, what do the following patterns mean? + +.. code:: + + pattern {+, @term {? at {+ @num}}} + generalize {+, @term at {+ @num} as @ident} + fix @ident @num with {+ (@ident {+ @binder} {? {struct @ident'}} : @type)} + +Objects +------- + +Here is the list of all objects of the Coq domain (The symbol :black_nib: indicates an object whose signature can be written using the notations DSL): + +[OBJECTS] + +Coq directives +============== + +In addition to the objects above, the ``coqrst`` Sphinx plugin defines the following directives: + +[DIRECTIVES] + +Coq roles +========= + +In addition to the objects and directives above, the ``coqrst`` Sphinx plugin defines the following roles: + +[ROLES] + +Tips and tricks +=============== + +Nested lemmas +------------- + +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: + + .. coqtop:: all + + Lemma l1: 1 + 1 = 2. + + .. coqtop:: all + + Lemma l2: 2 + 2 <> 1. + +Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. + +Abbreviations and macros +------------------------ + +Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file </doc/sphinx/replaces.rst>`_ included by most chapters of the manual. Some useful LaTeX macros are defined in `</doc/sphinx/preamble.rst>`_. + +Emacs +----- + +The ``dev/tools/coqdev.el`` folder contains a convenient Emacs function to quickly insert Sphinx roles and quotes. It takes a single character (one of ``gntm:```), and inserts one of ``:g:``, ``:n:``, ``:t:``, or an arbitrary role, or double quotes. You can also select a region of text, and wrap it in single or double backticks using that function. + +Use the following snippet to bind it to :kbd:`F12` in ``rst-mode``:: + + (with-eval-after-load 'rst + (define-key rst-mode-map (kbd "<f12>") #'coqdev-sphinx-rst-coq-action)) diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 152f4f655..09faa0676 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -140,29 +140,29 @@ Declaration of Coercions .. warn:: Ambiguous path. - When the coercion `qualid` is added to the inheritance graph, non - valid coercion paths are ignored; they are signaled by a warning - displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored; they are signaled by a warning + displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`. .. cmdv:: Local Coercion @qualid : @class >-> @class - Declares the construction denoted by `qualid` as a coercion local to - the current section. + Declares the construction denoted by `qualid` as a coercion local to + the current section. .. cmdv:: Coercion @ident := @term - This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. .. cmdv:: Coercion @ident := @term : @type - This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Definition`` `ident` : `type` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. .. cmdv:: Local Coercion @ident := @term - This defines `ident` just like ``Let`` `ident` ``:=`` `term`, - and then declares `ident` as a coercion between it source and its target. + This defines `ident` just like ``Let`` `ident` ``:=`` `term`, + and then declares `ident` as a coercion between it source and its target. Assumptions can be declared as coercions at declaration time. This extends the grammar of assumptions from diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index f887a5fee..0e9c23b9b 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -150,9 +150,10 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin .. _ceil_thm: -**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then +.. thm:: Bound on the ceiling function - :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil` + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. For instance, from 2 x = 1 we can deduce diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 80ea8a116..b6c35d8fa 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -11,7 +11,7 @@ Program derivation |Coq| comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations of program refinements. To use the Derive extension it must first be -required with ``Require Coq.Derive.Derive``. When the extension is loaded, +required with ``Require Coq.derive.Derive``. When the extension is loaded, it provides the following command: .. cmd:: Derive @ident SuchThat @term As @ident diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 23bc9a2e4..1f7dd9d68 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -96,11 +96,13 @@ language = None # directories to ignore when looking for source files. # This patterns also effect to html_static_path and html_extra_path exclude_patterns = [ - '_build', - 'Thumbs.db', - '.DS_Store', - 'introduction.rst', - 'credits.rst' + '_build', + 'Thumbs.db', + '.DS_Store', + 'introduction.rst', + 'credits.rst', + 'README.rst', + 'README.template.rst' ] # The reST default role (used for this markup: `text`) to use for all diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index aa41f8058..4dcd7deb1 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -553,8 +553,8 @@ has type :token:`type`. .. cmd:: Axiom @ident : @term - This command links *term* to the name *ident* as its specification in - the global context. The fact asserted by *term* is thus assumed as a + This command links :token:`term` to the name :token:`ident` as its specification in + the global context. The fact asserted by :token:`term` is thus assumed as a postulate. .. exn:: @ident already exists. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 83dddab4f..ad1f0caa6 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -55,15 +55,20 @@ Customization at launch time By resource file ~~~~~~~~~~~~~~~~~~~~~~~ -When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file -``$XDG_CONFIG_HOME/coq/coqrc.xxx`` is loaded, where ``$XDG_CONFIG_HOME`` +When |Coq| is launched, with either ``coqtop`` or ``coqc``, the +resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will +be implicitly prepended to any document read by Coq, whether it is an +interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME`` is the configuration directory of the user (by default its home -directory ``/.config`` and ``xxx`` is the version number (e.g. 8.8). If +directory ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is -searched. You can also specify an arbitrary name for the resource file +searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched, +and, if still not found, the file ``~/.coqrc``. If the latter is also +absent, no resource file is loaded. +You can also specify an arbitrary name for the resource file (see option ``-init-file`` below). -This file may contain, for instance, ``Add LoadPath`` commands to add +The resource file may contain, for instance, ``Add LoadPath`` commands to add directories to the load path of |Coq|. It is possible to skip the loading of the resource file with the option ``-q``. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 892ddbc16..6d0b27728 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -542,23 +542,23 @@ Controlling the effect of proof editing commands .. opt:: Hyps Limit @num -This option controls the maximum number of hypotheses displayed in goals -after the application of a tactic. All the hypotheses remain usable -in the proof development. -When unset, it goes back to the default mode which is to print all -available hypotheses. + This option controls the maximum number of hypotheses displayed in goals + after the application of a tactic. All the hypotheses remain usable + in the proof development. + When unset, it goes back to the default mode which is to print all + available hypotheses. .. opt:: Automatic Introduction -This option controls the way binders are handled -in assertion commands such as ``Theorem ident [binders] : form``. When the -option is on, which is the default, binders are automatically put in -the local context of the goal to prove. + This option controls the way binders are handled + in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the + option is on, which is the default, binders are automatically put in + the local context of the goal to prove. -When the option is off, binders are discharged on the statement to be -proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) -has to be used to move the assumptions to the local context. + When the option is off, binders are discharged on the statement to be + proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) + has to be used to move the assumptions to the local context. Controlling memory usage @@ -570,13 +570,13 @@ to force |Coq| to optimize some of its internal data structures. .. cmd:: Optimize Proof -This command forces |Coq| to shrink the data structure used to represent -the ongoing proof. + This command forces |Coq| to shrink the data structure used to represent + the ongoing proof. .. cmd:: Optimize Heap -This command forces the |OCaml| runtime to perform a heap compaction. -This is in general an expensive operation. -See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ -There is also an analogous tactic :tacn:`optimize_heap`. + This command forces the |OCaml| runtime to perform a heap compaction. + This is in general an expensive operation. + See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ + There is also an analogous tactic :tacn:`optimize_heap`. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0318bddde..3835524f0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -653,7 +653,7 @@ be applied or the goal is not head-reducible. This repeats ``intro`` until it meets the head-constant. It never reduces head-constants and it never fails. -.. tac:: intro @ident +.. tacn:: intro @ident This applies ``intro`` but forces :n:`@ident` to be the name of the introduced hypothesis. @@ -904,15 +904,15 @@ quantification or an implication. .. tacn:: revert {+ @ident} :name: revert -This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses -(possibly defined) to the goal, if this respects dependencies. This tactic is -the inverse of :tacn:`intro`. + This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses + (possibly defined) to the goal, if this respects dependencies. This tactic is + the inverse of :tacn:`intro`. .. exn:: No such hypothesis. .. exn:: @ident is used in the hypothesis @ident. -.. tac:: revert dependent @ident +.. tacn:: revert dependent @ident This moves to the goal the hypothesis :n:`@ident` and all the hypotheses that depend on it. @@ -1122,7 +1122,7 @@ Controlling the proof flow This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by Coq. -.. tacv:: assert form by tactic +.. tacv:: assert @form by @tactic This tactic behaves like :n:`assert` but applies tactic to solve the subgoals generated by assert. @@ -1130,7 +1130,7 @@ Controlling the proof flow .. exn:: Proof is not complete. :name: Proof is not complete. (assert) -.. tacv:: assert form as intro_pattern +.. tacv:: assert @form as @intro_pattern If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`), the hypothesis is named after this introduction pattern (in particular, if @@ -1139,7 +1139,7 @@ Controlling the proof flow introduction pattern, the tactic behaves like :n:`assert form` followed by the action done by this introduction pattern. -.. tacv:: assert form as intro_pattern by tactic +.. tacv:: assert @form as @intro_pattern by @tactic This combines the two previous variants of :n:`assert`. @@ -1192,9 +1192,9 @@ Controlling the proof flow This behaves like :n:`enough form` using :n:`intro_pattern` to name or destruct the new hypothesis. -.. tacv:: enough (@ident : form) by tactic -.. tacv:: enough form by tactic -.. tacv:: enough form as intro_pattern by tactic +.. tacv:: enough (@ident : @form) by @tactic +.. tacv:: enough @form by @tactic +.. tacv:: enough @form as @intro_pattern by @tactic This behaves as above but with :n:`tactic` expected to solve the initial goal after the extra assumption :n:`form` is added and possibly destructed. If the @@ -3240,7 +3240,9 @@ the processing of the rewriting rules. The rewriting rule bases are built with the ``Hint Rewrite vernacular`` command. -.. warn:: This tactic may loop if you build non terminating rewriting systems. +.. warning:: + + This tactic may loop if you build non terminating rewriting systems. .. tacv:: autorewrite with {+ @ident} using @tactic @@ -3444,7 +3446,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Declares each :n:`@ident` as a transparent or opaque constant. - .. cmdv:: Hint Extern @num {? @pattern} => tactic + .. cmdv:: Hint Extern @num {? @pattern} => @tactic :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 682553c31..838926d65 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -106,15 +106,15 @@ Automatic declaration of schemes .. opt:: Elimination Schemes -It is possible to deactivate the automatic declaration of the -induction principles when defining a new inductive type with the -``Unset Elimination Schemes`` command. It may be reactivated at any time with -``Set Elimination Schemes``. + It is possible to deactivate the automatic declaration of the + induction principles when defining a new inductive type with the + ``Unset Elimination Schemes`` command. It may be reactivated at any time with + ``Set Elimination Schemes``. .. opt:: Nonrecursive Elimination Schemes -This option controls whether types declared with the keywords :cmd:`Variant` and -:cmd:`Record` get an automatic declaration of the induction principles. + This option controls whether types declared with the keywords :cmd:`Variant` and + :cmd:`Record` get an automatic declaration of the induction principles. .. opt:: Case Analysis Schemes @@ -125,8 +125,8 @@ This option controls whether types declared with the keywords :cmd:`Variant` and .. opt:: Decidable Equality Schemes -These flags control the automatic declaration of those Boolean equalities (see -the second variant of ``Scheme``). + These flags control the automatic declaration of those Boolean equalities (see + the second variant of ``Scheme``). .. warning:: diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index d464f75bb..a004959eb 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -32,8 +32,9 @@ COQDOC_OPTIONS = ['--body-only', '--no-glob', '--no-index', '--no-externals', COQDOC_SYMBOLS = ["->", "<-", "<->", "=>", "<=", ">=", "<>", "~", "/\\", "\\/", "|-", "*", "forall", "exists"] COQDOC_HEADER = "".join("(** remove printing {} *)".format(s) for s in COQDOC_SYMBOLS) -def coqdoc(coq_code, coqdoc_bin = os.path.join(os.getenv("COQBIN"),"coqdoc")): +def coqdoc(coq_code, coqdoc_bin=None): """Get the output of coqdoc on coq_code.""" + coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc") fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") try: os.write(fd, COQDOC_HEADER.encode("utf-8")) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 21093bd90..606d725bf 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -1,3 +1,4 @@ +# -*- coding: utf-8 -*- ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## ## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## @@ -57,30 +58,37 @@ def make_target(objtype, targetid): return "coq:{}.{}".format(objtype, targetid) class CoqObject(ObjectDescription): - """A generic Coq object; all Coq objects are subclasses of this. + """A generic Coq object for Sphinx; all Coq objects are subclasses of this. The fields and methods to override are listed at the top of this class' implementation. Each object supports the :name: option, which gives an explicit name to link to. - See the documentation of CoqDomain for high-level information. + See the comments and docstrings in CoqObject for more information. """ - # The semantic domain in which this object lives. + # The semantic domain in which this object lives (eg. “tac”, “cmd”, “chm”…). # It matches exactly one of the roles used for cross-referencing. - subdomain = None + subdomain = None # type: str - # The suffix to use in indices for objects of this type - index_suffix = None + # The suffix to use in indices for objects of this type (eg. “(tac)”) + index_suffix = None # type: str # The annotation to add to headers of objects of this type - annotation = None + # (eg. “Command”, “Theorem”) + annotation = None # type: str def _name_from_signature(self, signature): # pylint: disable=no-self-use, unused-argument """Convert a signature into a name to link to. + ‘Signature’ is Sphinx parlance for an object's header (think “type + signature”); for example, the signature of the simplest form of the + ``exact`` tactic is ``exact @id``. + Returns None by default, in which case no name will be automatically - generated. + generated. This is a convenient way to automatically generate names + (link targets) without having to write explicit names everywhere. + """ return None @@ -100,7 +108,7 @@ class CoqObject(ObjectDescription): def handle_signature(self, signature, signode): """Prefix signature with the proper annotation, then render it using - _render_signature. + ``_render_signature`` (for example, add “Command” in front of commands). :returns: the name given to the resulting node, if any """ @@ -110,11 +118,6 @@ class CoqObject(ObjectDescription): self._render_signature(signature, signode) return self.options.get("name") or self._name_from_signature(signature) - @property - def _index_suffix(self): - if self.index_suffix: - return " " + self.index_suffix - def _record_name(self, name, target_id): """Record a name, mapping it to target_id @@ -141,12 +144,14 @@ class CoqObject(ObjectDescription): return targetid def _add_index_entry(self, name, target): - """Add name (with target) to the main index.""" - index_text = name + self._index_suffix + """Add `name` (pointing to `target`) to the main index.""" + index_text = 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): - """Create a target and an index entry for name""" + """Attach a link target to `signode` and an index entry for `name`.""" if name: target = self._add_target(signode, name) # remove trailing . , found in commands, but not ... (ellipsis) @@ -156,31 +161,44 @@ class CoqObject(ObjectDescription): return target class PlainObject(CoqObject): - """A base class for objects whose signatures should be rendered literaly.""" + """A base class for objects whose signatures should be rendered literally.""" def _render_signature(self, signature, signode): signode += addnodes.desc_name(signature, signature) class NotationObject(CoqObject): - """A base class for objects whose signatures should be rendered as nested boxes.""" + """A base class for objects whose signatures should be rendered as nested boxes. + + Objects that inherit from this class can use the notation grammar (“{+ …}”, + “@…”, etc.) in their signature. + """ def _render_signature(self, signature, signode): position = self.state_machine.get_source_and_line(self.lineno) tacn_node = parse_notation(signature, *position) signode += addnodes.desc_name(signature, '', tacn_node) -class TacticObject(PlainObject): - """An object to represent Coq tactics""" - subdomain = "tac" - index_suffix = "(tac)" - annotation = None - class GallinaObject(PlainObject): - """An object to represent Coq theorems""" + r"""A theorem. + + Example:: + + .. thm:: Bound on the ceiling function + + Let :math:`p` be an integer and :math:`c` a rational constant. Then + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`. + """ subdomain = "thm" index_suffix = "(thm)" annotation = "Theorem" class VernacObject(NotationObject): - """An object to represent Coq commands""" + """A Coq command. + + Example:: + + .. cmd:: Infix "@symbol" := @term ({+, @modifier}). + + This command is equivalent to :n:`…`. + """ subdomain = "cmd" index_suffix = "(cmd)" annotation = "Command" @@ -191,7 +209,20 @@ class VernacObject(NotationObject): return m.group(0).strip() class VernacVariantObject(VernacObject): - """An object to represent variants of Coq commands""" + """A variant of a Coq command. + + Example:: + + .. cmd:: Axiom @ident : @term. + + This command links :token:`term` to the name :token:`term` as its specification in + the global context. The fact asserted by :token:`term` is thus assumed as a + postulate. + + .. cmdv:: Parameter @ident : @term. + + This is equivalent to :n:`Axiom @ident : @term`. + """ index_suffix = "(cmdv)" annotation = "Variant" @@ -199,18 +230,49 @@ class VernacVariantObject(VernacObject): return None class TacticNotationObject(NotationObject): - """An object to represent Coq tactic notations""" + """A tactic, or a tactic notation. + + Example:: + + .. tacn:: do @num @expr + + :token:`expr` is evaluated to ``v`` which must be a tactic value. … + """ subdomain = "tacn" index_suffix = "(tacn)" annotation = None class TacticNotationVariantObject(TacticNotationObject): - """An object to represent variants of Coq tactic notations""" + """A variant of a tactic. + + Example:: + + .. tacn:: fail + + This is the always-failing tactic: it does not solve any goal. It is + useful for defining other tacticals since it can be caught by + :tacn:`try`, :tacn:`repeat`, :tacn:`match goal`, or the branching + tacticals. … + + .. tacv:: fail @natural + + The number is the failure level. If no level is specified, it + defaults to 0. … + """ index_suffix = "(tacnv)" annotation = "Variant" class OptionObject(NotationObject): - """An object to represent Coq options""" + """A Coq option. + + Example:: + + .. opt:: Nonrecursive Elimination Schemes + + This option controls whether types declared with the keywords + :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the + induction principles. + """ subdomain = "opt" index_suffix = "(opt)" annotation = "Option" @@ -219,7 +281,13 @@ class OptionObject(NotationObject): return stringify_with_ellipses(signature) class ProductionObject(NotationObject): - """An object to represent grammar productions""" + """Grammar productions. + + This is useful if you intend to document individual grammar productions. + Otherwise, use Sphinx's `production lists + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. + """ + # FIXME (CPC): I have no idea what this does :/ Someone should add an example. subdomain = "prodn" index_suffix = None annotation = None @@ -258,7 +326,22 @@ class ProductionObject(NotationObject): return [idx, node] class ExceptionObject(NotationObject): - """An object to represent Coq errors.""" + """An error raised by a Coq command or tactic. + + This commonly appears nested in the ``.. tacn::`` that raises the + exception. + + Example:: + + .. tacv:: assert @form by @tactic + + This tactic applies :n:`@tactic` to solve the subgoals generated by + ``assert``. + + .. exn:: Proof is not complete + + Raised if :n:`@tactic` does not fully solve the goal. + """ subdomain = "exn" index_suffix = "(err)" annotation = "Error" @@ -269,7 +352,19 @@ class ExceptionObject(NotationObject): return stringify_with_ellipses(signature) class WarningObject(NotationObject): - """An object to represent Coq warnings.""" + """An warning raised by a Coq command or tactic.. + + Do not mistake this for ``.. warning::``; this directive is for warning + messages produced by Coq. + + + Example:: + + .. warn:: Ambiguous path + + When the coercion :token:`qualid` is added to the inheritance graph, non + valid coercion paths are ignored. + """ subdomain = "warn" index_suffix = "(warn)" annotation = "Warning" @@ -280,14 +375,33 @@ class WarningObject(NotationObject): def NotationRole(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=unused-argument, dangerous-default-value - """And inline role for notations""" + """Any text using the notation syntax (``@id``, ``{+, …}``, etc.). + + Use this to explain tactic equivalences. For example, you might write + this:: + + :n:`generalize @term as @ident` is just like :n:`generalize @term`, but + it names the introduced hypothesis :token:`ident`. + + Note that this example also uses ``:token:``. That's because ``ident`` is + defined in the the Coq manual as a grammar production, and ``:token:`` + creates a link to that. When referring to a placeholder that happens to be + a grammar production, ``:token:`…``` is typically preferable to ``:n:`@…```. + """ notation = utils.unescape(text, 1) position = inliner.reporter.get_source_and_line(lineno) return [nodes.literal(rawtext, '', parse_notation(notation, *position, rawtext=rawtext))], [] def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): #pylint: disable=dangerous-default-value - """And inline role for Coq source code""" + """Coq code. + + Use this for Gallina and Ltac snippets:: + + :g:`apply plus_comm; reflexivity` + :g:`Set Printing All.` + :g:`forall (x: t), P(x)` + """ options['language'] = 'Coq' return code_role(role, rawtext, text, lineno, inliner, options, content) ## Too heavy: @@ -300,15 +414,14 @@ def coq_code_role(role, rawtext, text, lineno, inliner, options={}, content=[]): # node = nodes.literal(rawtext, '', *highlight_using_coqdoc(code), classes=classes) # return [node], [] -# TODO pass different languages? -LtacRole = GallinaRole = VernacRole = coq_code_role +CoqCodeRole = coq_code_role class CoqtopDirective(Directive): """A reST directive to describe interactions with Coqtop. Usage:: - .. coqtop:: (options)+ + .. coqtop:: options… Coq code to send to coqtop @@ -321,20 +434,28 @@ class CoqtopDirective(Directive): Here is a list of permissible options: - Display - - ‘all’: Display input and output - - ‘in’: Display only input - - ‘out’: Display only output - - ‘none’: Display neither (useful for setup commands) - Behaviour - - ‘reset’: Send a `Reset Initial` command before running this block - - ‘undo’: Send an `Undo n` (n=number of sentences) command after running - all the commands in this block + - Display options + + - ``all``: Display input and output + - ``in``: Display only input + - ``out``: Display only output + - ``none``: Display neither (useful for setup commands) + + - Behavior options + + - ``reset``: Send a ``Reset Initial`` command before running this block + - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after + running all the commands in this block + + ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks + of the same document (``coqrst`` creates a single ``coqtop`` process per + reST source file). Use the ``reset`` option to reset Coq's state. """ has_content = True required_arguments = 0 optional_arguments = 1 final_argument_whitespace = True + directive_name = "coqtop" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -349,12 +470,26 @@ class CoqtopDirective(Directive): return [node] class CoqdocDirective(Directive): - """A reST directive to display Coqtop-formatted source code""" + """A reST directive to display Coqtop-formatted source code. + + Usage:: + + .. coqdoc:: + + Coq code to highlight + + Example:: + + .. coqdoc:: + + Definition test := 1. + """ # TODO implement this as a Pygments highlighter? has_content = True required_arguments = 0 optional_arguments = 0 final_argument_whitespace = True + directive_name = "coqdoc" def run(self): # Uses a ‘container’ instead of a ‘literal_block’ to disable @@ -365,8 +500,24 @@ class CoqdocDirective(Directive): return [wrapper] class ExampleDirective(BaseAdmonition): - """A reST directive for examples""" + """A reST directive for examples. + + This behaves like a generic admonition; see + http://docutils.sourceforge.net/docs/ref/rst/directives.html#generic-admonition + for more details. + + Example:: + + .. example:: Adding a hint to a database + + The following adds ``plus_comm`` to the ``plu`` database: + + .. coqdoc:: + + Hint Resolve plus_comm : plu. + """ node_class = nodes.admonition + directive_name = "example" def run(self): # ‘BaseAdmonition’ checks whether ‘node_class’ is ‘nodes.admonition’, @@ -380,8 +531,17 @@ class ExampleDirective(BaseAdmonition): class PreambleDirective(MathDirective): r"""A reST directive for hidden math. - Mostly useful to let MathJax know about `\def`s and `\newcommand`s + Mostly useful to let MathJax know about `\def`\ s and `\newcommand`\ s. + + Example:: + + .. preamble:: + + \newcommand{\paren}[#1]{\left(#1\right)} """ + + directive_name = "preamble" + def run(self): self.options['nowrap'] = True [node] = super().run() @@ -389,14 +549,17 @@ class PreambleDirective(MathDirective): return [node] class InferenceDirective(Directive): - r"""A small example of what directives let you do in Sphinx. + r"""A reST directive to format inference rules. + + This also serves as a small illustration of the way to create new Sphinx + directives. Usage:: .. inference:: name - \n-separated premisses - ---------------------- + newline-separated premisses + ------------------------ conclusion Example:: @@ -413,6 +576,7 @@ class InferenceDirective(Directive): optional_arguments = 0 has_content = True final_argument_whitespace = True + directive_name = "inference" def make_math_node(self, latex): node = displaymath() @@ -613,7 +777,7 @@ class CoqSubdomainsIndex(Index): Just as in the original manual, we want to have separate indices for each Coq subdomain (tactics, commands, options, etc)""" - name, localname, shortname, subdomains = None, None, None, None # Must be overwritten + name, localname, shortname, subdomains = None, None, None, [] # Must be overwritten def generate(self, docnames=None): content = defaultdict(list) @@ -635,7 +799,7 @@ class CoqVernacIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "cmdindex", "Command Index", "commands", ["cmd"] class CoqTacticIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tac", "tacn"] + name, localname, shortname, subdomains = "tacindex", "Tactic Index", "tactics", ["tacn"] class CoqOptionIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "optindex", "Option Index", "options", ["opt"] @@ -665,10 +829,18 @@ class IndexXRefRole(XRefRole): return title, target def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, content=[]): - """An inline role to declare grammar productions that are not in fact included - in a `productionlist` directive. + """A grammar production not included in a ``productionlist`` directive. - Useful to informally introduce a production, as part of running text + Useful to informally introduce a production, as part of running text. + + Example:: + + :production:`string` indicates a quoted string. + + You're not likely to use this role very commonly; instead, use a + `production list + <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_ + and reference its tokens using ``:token:`…```. """ #pylint: disable=dangerous-default-value, unused-argument env = inliner.document.settings.env @@ -681,6 +853,8 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte env.domaindata['std']['objects']['token', text] = env.docname, targetid return [node], [] +GrammarProductionRole.role_name = "production" + class CoqDomain(Domain): """A domain to document Coq code. @@ -703,7 +877,6 @@ class CoqDomain(Domain): # ObjType (= directive type) → (Local name, *xref-roles) 'cmd': ObjType('cmd', 'cmd'), 'cmdv': ObjType('cmdv', 'cmd'), - 'tac': ObjType('tac', 'tac'), 'tacn': ObjType('tacn', 'tacn'), 'tacv': ObjType('tacv', 'tacn'), 'opt': ObjType('opt', 'opt'), @@ -720,7 +893,6 @@ class CoqDomain(Domain): # the same role. 'cmd': VernacObject, 'cmdv': VernacVariantObject, - 'tac': TacticObject, 'tacn': TacticNotationObject, 'tacv': TacticNotationVariantObject, 'opt': OptionObject, @@ -733,7 +905,6 @@ class CoqDomain(Domain): roles = { # Each of these roles lives in a different semantic “subdomain” 'cmd': XRefRole(warn_dangling=True), - 'tac': XRefRole(warn_dangling=True), 'tacn': XRefRole(warn_dangling=True), 'opt': XRefRole(warn_dangling=True), 'thm': XRefRole(warn_dangling=True), @@ -743,12 +914,8 @@ class CoqDomain(Domain): # This one is special 'index': IndexXRefRole(), # These are used for highlighting - 'notation': NotationRole, - 'gallina': GallinaRole, - 'ltac': LtacRole, 'n': NotationRole, - 'g': GallinaRole, - 'l': LtacRole, #FIXME unused? + 'g': CoqCodeRole } indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex] @@ -759,7 +926,6 @@ class CoqDomain(Domain): # others, such as “version” 'objects' : { # subdomain → name → docname, objtype, targetid 'cmd': {}, - 'tac': {}, 'tacn': {}, 'opt': {}, 'thm': {}, @@ -829,11 +995,18 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: for node in doctree.traverse(is_coqtop_or_coqdoc_block): if is_html: node.rawsource = '' # Prevent pygments from kicking in + elif 'coqtop-hidden' in node['classes']: + node.parent.remove(node) else: - if 'coqtop-hidden' in node['classes']: - node.parent.remove(node) - else: - node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq")) + node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq")) + +COQ_ADDITIONAL_DIRECTIVES = [CoqtopDirective, + CoqdocDirective, + ExampleDirective, + InferenceDirective, + PreambleDirective] + +COQ_ADDITIONAL_ROLES = [GrammarProductionRole] def setup(app): """Register the Coq domain""" @@ -845,12 +1018,13 @@ def setup(app): # Add domain, directives, and roles app.add_domain(CoqDomain) - app.add_role("production", GrammarProductionRole) - app.add_directive("coqtop", CoqtopDirective) - app.add_directive("coqdoc", CoqdocDirective) - app.add_directive("example", ExampleDirective) - app.add_directive("inference", InferenceDirective) - app.add_directive("preamble", PreambleDirective) + + for role in COQ_ADDITIONAL_ROLES: + app.add_role(role.role_name, role) + + for directive in COQ_ADDITIONAL_DIRECTIVES: + app.add_directive(directive.directive_name, directive) + app.add_transform(CoqtopBlocksTransform) app.connect('doctree-resolved', simplify_source_code_blocks_for_latex) diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py new file mode 100755 index 000000000..e56882a52 --- /dev/null +++ b/doc/tools/coqrst/regen_readme.py @@ -0,0 +1,58 @@ +#!/usr/bin/env python3 +# -*- coding: utf-8 -*- + +"""Rebuild sphinx/README.rst from sphinx/README.template.rst.""" + +import re +from os import sys, path + +SCRIPT_DIR = path.dirname(path.abspath(__file__)) +if __name__ == "__main__" and __package__ is None: + sys.path.append(path.dirname(SCRIPT_DIR)) + +import sphinx +from coqrst import coqdomain + +README_ROLES_MARKER = "[ROLES]" +README_OBJECTS_MARKER = "[OBJECTS]" +README_DIRECTIVES_MARKER = "[DIRECTIVES]" + +FIRST_LINE_BLANKS = re.compile("^(.*)\n *\n") +def format_docstring(template, obj, *strs): + docstring = obj.__doc__.strip() + strs = strs + (FIRST_LINE_BLANKS.sub(r"\1\n", docstring),) + return template.format(*strs) + +SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/") +README_PATH = path.join(SPHINX_DIR, "README.rst") +README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst") + +def notation_symbol(d): + return " :black_nib:" if issubclass(d, coqdomain.NotationObject) else "" + +def regen_readme(): + objects_docs = [format_docstring("``.. {}::``{} {}", obj, objname, notation_symbol(obj)) + for objname, obj in sorted(coqdomain.CoqDomain.directives.items())] + + roles = ([(name, cls) + for name, cls in sorted(coqdomain.CoqDomain.roles.items()) + if not isinstance(cls, (sphinx.roles.XRefRole, coqdomain.IndexXRefRole))] + + [(fn.role_name, fn) + for fn in coqdomain.COQ_ADDITIONAL_ROLES]) + roles_docs = [format_docstring("``:{}:`` {}", role, name) + for (name, role) in roles] + + directives_docs = [format_docstring("``.. {}::`` {}", d, d.directive_name) + for d in coqdomain.COQ_ADDITIONAL_DIRECTIVES] + + with open(README_TEMPLATE_PATH, encoding="utf-8") as readme: + contents = readme.read() + + with open(README_PATH, mode="w", encoding="utf-8") as readme: + readme.write(contents + .replace(README_ROLES_MARKER, "\n\n".join(roles_docs)) + .replace(README_OBJECTS_MARKER, "\n\n".join(objects_docs)) + .replace(README_DIRECTIVES_MARKER, "\n\n".join(directives_docs))) + +if __name__ == '__main__': + regen_readme() diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index efb5cb550..aeadce4c4 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -41,7 +41,9 @@ class CoqTop: the ansicolors module) :param args: Additional arugments to coqtop. """ - self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN'),"coqtop") + self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop") + if not pexpect.utils.which(self.coqtop_bin): + raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin)) self.args = (args or []) + ["-boot", "-color", "on"] * color self.coqtop = None diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index d5feafbf9..be2b05da8 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -18,6 +18,7 @@ #include <caml/misc.h> #include <caml/mlvalues.h> #include <caml/fail.h> +#include <caml/alloc.h> #include <caml/memory.h> #include "coq_instruct.h" #include "coq_fix_code.h" @@ -78,38 +79,41 @@ void * coq_stat_alloc (asize_t sz) } value coq_makeaccu (value i) { - code_t q; - code_t res = coq_stat_alloc(2 * sizeof(opcode_t)); - q = res; + CAMLparam1(i); + CAMLlocal1(res); + code_t q = coq_stat_alloc(2 * sizeof(opcode_t)); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = q; *q++ = VALINSTR(MAKEACCU); *q = (opcode_t)Int_val(i); - return (value)res; + CAMLreturn(res); } value coq_pushpop (value i) { - code_t res; - int n; - n = Int_val(i); + CAMLparam1(i); + CAMLlocal1(res); + code_t q; + res = caml_alloc_small(1, Abstract_tag); + int n = Int_val(i); if (n == 0) { - res = coq_stat_alloc(sizeof(opcode_t)); - *res = VALINSTR(STOP); - return (value)res; + q = coq_stat_alloc(sizeof(opcode_t)); + Code_val(res) = q; + *q = VALINSTR(STOP); + CAMLreturn(res); } else { - code_t q; - res = coq_stat_alloc(3 * sizeof(opcode_t)); - q = res; + q = coq_stat_alloc(3 * sizeof(opcode_t)); + Code_val(res) = q; *q++ = VALINSTR(POP); *q++ = (opcode_t)n; *q = VALINSTR(STOP); - return (value)res; + CAMLreturn(res); } } value coq_is_accumulate_code(value code){ - code_t q; + code_t q = Code_val(code); int res; - q = (code_t)code; res = Is_instruction(q,ACCUMULATE); return Val_bool(res); } @@ -132,11 +136,14 @@ value coq_is_accumulate_code(value code){ #define COPY32(dst,src) (*dst=*src) #endif /* ARCH_BIG_ENDIAN */ -value coq_tcode_of_code (value code, value size) { - code_t p, q, res; - asize_t len = (asize_t) Long_val(size); - res = coq_stat_alloc(len); - q = res; +value coq_tcode_of_code (value code) { + CAMLparam1 (code); + CAMLlocal1 (res); + code_t p, q; + asize_t len = (asize_t) caml_string_length(code); + res = caml_alloc_small(1, Abstract_tag); + q = coq_stat_alloc(len); + Code_val(res) = q; len /= sizeof(opcode_t); for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) { opcode_t instr; @@ -166,5 +173,5 @@ value coq_tcode_of_code (value code, value size) { for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; }; } } - return (value)res; + CAMLreturn(res); } diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h index 5c85389dd..638d6b5ab 100644 --- a/kernel/byterun/coq_fix_code.h +++ b/kernel/byterun/coq_fix_code.h @@ -26,7 +26,7 @@ void init_arity(); #define Is_instruction(pc,instr) (*pc == VALINSTR(instr)) -value coq_tcode_of_code(value code, value len); +value coq_tcode_of_code(value code); value coq_makeaccu (value i); value coq_pushpop (value i); value coq_is_accumulate_code(value code); diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index cfeb0a9ee..8ac1ecc79 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -16,6 +16,7 @@ #include <stdio.h> #include <signal.h> #include <stdint.h> +#include <caml/memory.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -629,7 +630,7 @@ value coq_interprete print_instr("CLOSUREREC"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ - Alloc_small(accu, nfuncs, 0); + Alloc_small(accu, nfuncs, Abstract_tag); for(i = 0; i < nfuncs; i++) { Field(accu,i) = (value)(pc+pc[i]); } @@ -665,7 +666,7 @@ value coq_interprete print_instr("CLOSURECOFIX"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ - Alloc_small(accu, nfunc, 0); + Alloc_small(accu, nfunc, Abstract_tag); for(i = 0; i < nfunc; i++) { Field(accu,i) = (value)(pc+pc[i]); } @@ -1071,12 +1072,22 @@ value coq_interprete } } *--sp = accu; - /* We create the switch zipper */ - Alloc_small(accu, 5, Default_tag); - Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; - Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; - Field(accu, 4) = coq_env; - sp++;sp[0] = accu; + /* Create bytecode wrappers */ + Alloc_small(accu, 1, Abstract_tag); + Code_val(accu) = typlbl; + *--sp = accu; + Alloc_small(accu, 1, Abstract_tag); + Code_val(accu) = swlbl; + *--sp = accu; + /* We create the switch zipper */ + Alloc_small(accu, 5, Default_tag); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; + Field(accu, 2) = sp[3]; + Field(accu, 3) = sp[2]; + Field(accu, 4) = coq_env; + sp += 3; + sp[0] = accu; /* We create the atom */ Alloc_small(accu, 2, ATOM_SWITCH_TAG); Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; @@ -1476,7 +1487,8 @@ value coq_interprete #endif } -value coq_push_ra(value tcode) { +value coq_push_ra(value code) { + code_t tcode = Code_val(code); print_instr("push_ra"); coq_sp -= 3; coq_sp[0] = (value) tcode; @@ -1516,8 +1528,10 @@ value coq_push_vstack(value stk, value max_stack_size) { } value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) { + // Registering the other arguments w.r.t. the OCaml GC is done by coq_interprete + CAMLparam1(tcode); print_instr("coq_interprete"); - return coq_interprete((code_t)tcode, a, t, g, e, Long_val(ea)); + CAMLreturn (coq_interprete(Code_val(tcode), a, t, g, e, Long_val(ea))); print_instr("end coq_interprete"); } diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index b2917a55e..542a05fd2 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -10,6 +10,8 @@ #include <stdio.h> #include <string.h> +#include <caml/alloc.h> +#include <caml/address_class.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -46,7 +48,11 @@ value coq_static_alloc(value size) /* ML */ value accumulate_code(value unit) /* ML */ { - return (value) accumulate; + CAMLparam1(unit); + CAMLlocal1(res); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = accumulate; + CAMLreturn(res); } static void (*coq_prev_scan_roots_hook) (scanning_action); @@ -56,6 +62,10 @@ static void coq_scan_roots(scanning_action action) register value * i; /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { +#ifdef NO_NAKED_POINTERS + /* The VM stack may contain C-allocated bytecode */ + if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue; +#endif (*action) (*i, i); }; /* Hook */ @@ -94,8 +104,12 @@ value init_coq_vm(value unit) /* ML */ /* Initialing the interpreter */ init_coq_interpreter(); - /* Some predefined pointer code */ - accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t)); + /* Some predefined pointer code. + * It is typically contained in accumlator blocks whose tag is 0 and thus + * scanned by the GC, so make it look like an OCaml block. */ + value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); + Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ + accumulate = (code_t) Val_hp(accu_block); *accumulate = VALINSTR(ACCUMULATE); /* Initialize GC */ diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index 528babebf..e05f3fb82 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -9,6 +9,7 @@ /***********************************************************************/ #include <stdio.h> +#include <caml/memory.h> #include "coq_fix_code.h" #include "coq_instruct.h" #include "coq_memory.h" @@ -58,10 +59,36 @@ value coq_offset_closure(value v, value offset){ return (value)&Field(v, Int_val(offset)); } +value coq_set_bytecode_field(value v, value i, value code) { + // No write barrier because the bytecode does not live on the OCaml heap + Field(v, Long_val(i)) = (value) Code_val(code); + return Val_unit; +} + value coq_offset_tcode(value code,value offset){ - return((value)((code_t)code + Int_val(offset))); + CAMLparam1(code); + CAMLlocal1(res); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = Code_val(code) + Int_val(offset); + CAMLreturn(res); } -value coq_int_tcode(value code, value offset) { +value coq_int_tcode(value pc, value offset) { + code_t code = Code_val(pc); return Val_int(*((code_t) code + Int_val(offset))); } + +value coq_tcode_array(value tcodes) { + CAMLparam1(tcodes); + CAMLlocal2(res, tmp); + int i; + /* Assumes that the vector of types is small. This was implicit in the + previous code which was building the type array using Alloc_small. */ + res = caml_alloc_small(Wosize_val(tcodes), Default_tag); + for (i = 0; i < Wosize_val(tcodes); i++) { + tmp = caml_alloc_small(1, Abstract_tag); + Code_val(tmp) = (code_t) Field(tcodes, i); + Store_field(res, i, tmp); + } + CAMLreturn(res); +} diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 14f4f27c0..cea09c510 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -20,7 +20,7 @@ open Mod_subst type emitcodes = String.t -external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code" +external tcode_of_code : Bytes.t -> Vmvalues.tcode = "coq_tcode_of_code" (* Relocation information *) type reloc_info = @@ -82,7 +82,7 @@ let patch buff pl f = (** Order seems important here? *) let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in let buff = patch_int buff reloc in - tcode_of_code buff (Bytes.length buff) + tcode_of_code buff (* Buffering of bytecode *) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 6a41efac2..7a703e653 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -59,14 +59,17 @@ let vm_global (v : values array) = (Obj.magic v : vm_global) (*******************************************) type tcode +(** A block whose first field is a C-allocated VM bytecode, encoded as char*. + This is compatible with the representation of the Coq VM closures. *) + +type tcode_array external mkAccuCode : int -> tcode = "coq_makeaccu" external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode" -let tcode_of_obj v = ((Obj.obj v):tcode) -let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) -let fix_code v = fun_code v -let cofix_upd_code v = fun_code v +let fun_code v = (Obj.magic v : tcode) +let fix_code = fun_code +let cofix_upd_code = fun_code type vswitch = { @@ -255,6 +258,7 @@ external kind_of_closure : Obj.t -> int = "coq_kind_of_closure" external is_accumulate : tcode -> bool = "coq_is_accumulate_code" external int_tcode : tcode -> int -> int = "coq_int_tcode" external accumulate : unit -> tcode = "accumulate_code" +external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field" let accumulate = accumulate () let whd_val : values -> whd = @@ -284,7 +288,7 @@ let whd_val : values -> whd = let obj_of_atom : atom -> Obj.t = fun a -> let res = Obj.new_block accu_tag 2 in - Obj.set_field res 0 (Obj.repr accumulate); + set_bytecode_field res 0 accumulate; Obj.set_field res 1 (Obj.repr a); res @@ -370,17 +374,20 @@ external closure_arity : vfun -> int = "coq_closure_arity" external offset : Obj.t -> int = "coq_offset" external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure" external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure" +external tcode_array : tcode_array -> tcode array = "coq_tcode_array" let first o = (offset_closure o (offset o)) let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix) let last o = (Obj.field o (Obj.size o - 1)) -let fix_types (v:vfix) = (Obj.magic (last (Obj.repr v)) : tcode array) -let cofix_types (v:vcofix) = (Obj.magic (last (Obj.repr v)) : tcode array) +let fix_types (v:vfix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array) +let cofix_types (v:vcofix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array) let current_fix vf = - (offset (Obj.repr vf) / 2) -let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i)) +let unsafe_fb_code fb i = + let off = (2 * i) * (Sys.word_size / 8) in + Obj.obj (Obj.add_offset (Obj.repr fb) (Int32.of_int off)) let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1 @@ -442,13 +449,12 @@ let relaccu_code i = let mk_fix_body k ndef fb = let e = Obj.dup (Obj.repr fb) in for i = 0 to ndef - 1 do - Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i))) + set_bytecode_field e (2 * i) (relaccu_code (k + i)) done; let fix_body i = - let jump_grabrec c = offset_tcode c 2 in - let c = jump_grabrec (unsafe_fb_code fb i) in + let c = offset_tcode (unsafe_fb_code fb i) 2 in let res = Obj.new_block Obj.closure_tag 2 in - Obj.set_field res 0 (Obj.repr c); + set_bytecode_field res 0 c; Obj.set_field res 1 (offset_closure e (2*i)); ((Obj.obj res) : vfun) in Array.init ndef fix_body @@ -486,7 +492,7 @@ let mk_cofix_body apply_varray k ndef vcf = Obj.set_field e 0 c; let atom = Obj.new_block cofix_tag 1 in let self = Obj.new_block accu_tag 2 in - Obj.set_field self 0 (Obj.repr accumulate); + set_bytecode_field self 0 accumulate; Obj.set_field self 1 (Obj.repr atom); apply_varray (Obj.obj e) [|Obj.obj self|] in Array.init ndef cofix_body diff --git a/man/coqtop.1 b/man/coqtop.1 index b1fbb3262..084adfe45 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -110,7 +110,7 @@ print Coq version and exit .TP .B \-q -skip loading of rcfile +skip loading of rcfile (resource file) if any .TP .BI \-init\-file \ filename |