diff options
Diffstat (limited to 'doc')
18 files changed, 262 insertions, 46 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 4ad952bdfb..01240a062c 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -219,6 +219,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo Print nat. Definition a := 1. + The blank line after the directive is required. If you begin a proof, + include an ``Abort`` afterwards to reset coqtop for the next example. + Here is a list of permissible options: - Display options diff --git a/doc/sphinx/_static/diffs-coqide-compacted.png b/doc/sphinx/_static/diffs-coqide-compacted.png Binary files differnew file mode 100644 index 0000000000..b64ffeb269 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-compacted.png diff --git a/doc/sphinx/_static/diffs-coqide-multigoal.png b/doc/sphinx/_static/diffs-coqide-multigoal.png Binary files differnew file mode 100644 index 0000000000..4020279267 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-multigoal.png diff --git a/doc/sphinx/_static/diffs-coqide-on.png b/doc/sphinx/_static/diffs-coqide-on.png Binary files differnew file mode 100644 index 0000000000..f270397ea3 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-on.png diff --git a/doc/sphinx/_static/diffs-coqide-removed.png b/doc/sphinx/_static/diffs-coqide-removed.png Binary files differnew file mode 100644 index 0000000000..8f2e71fdc8 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqide-removed.png diff --git a/doc/sphinx/_static/diffs-coqtop-compacted.png b/doc/sphinx/_static/diffs-coqtop-compacted.png Binary files differnew file mode 100644 index 0000000000..b37f0a6771 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-compacted.png diff --git a/doc/sphinx/_static/diffs-coqtop-multigoal.png b/doc/sphinx/_static/diffs-coqtop-multigoal.png Binary files differnew file mode 100644 index 0000000000..cfedde02ac --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-multigoal.png diff --git a/doc/sphinx/_static/diffs-coqtop-on.png b/doc/sphinx/_static/diffs-coqtop-on.png Binary files differnew file mode 100644 index 0000000000..bdfcf0af1a --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-on.png diff --git a/doc/sphinx/_static/diffs-coqtop-on3.png b/doc/sphinx/_static/diffs-coqtop-on3.png Binary files differnew file mode 100644 index 0000000000..63ff869432 --- /dev/null +++ b/doc/sphinx/_static/diffs-coqtop-on3.png diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index aa8537c92d..d9eaa2c6c6 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -294,6 +294,17 @@ s}, year = {1994} } +@Article{Myers, + author = {Eugene Myers}, + title = {An {O(ND)} difference algorithm and its variations}, + journal = {Algorithmica}, + volume = {1}, + number = {2}, + year = {1986}, + bibsource = {https://link.springer.com/article/10.1007\%2FBF01840446}, + url = {http://www.xmailserver.org/diff2.pdf} +} + @InProceedings{Parent95b, author = {C. Parent}, booktitle = {{Mathematics of Program Construction'95}}, diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 636144e0c8..9dae7fd102 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -606,7 +606,7 @@ for several ways of defining a function *and other useful related objects*, namely: an induction principle that reflects the recursive structure of the function (see :tacn:`function induction`) and its fixpoint equality. The meaning of this declaration is to define a function ident, -similarly to ``Fixpoint`. Like in ``Fixpoint``, the decreasing argument must +similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must be given (unless the function is not recursive), but it might not necessarily be *structurally* decreasing. The point of the {} annotation is to name the decreasing argument *and* to describe which kind of diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 343ca9ed7d..de9e327740 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -85,6 +85,8 @@ Some |Coq| commands call other |Coq| commands. In this case, they look for the commands in directory specified by ``$COQBIN``. If this variable is not set, they look for the commands in the executable path. +.. _COQ_COLORS: + The ``$COQ_COLORS`` environment variable can be used to specify the set of colors used by ``coqtop`` to highlight its output. It uses the same syntax as the ``$LS_COLORS`` variable from GNU’s ls, that is, a colon-separated @@ -93,6 +95,15 @@ list of assignments of the form :n:`name={*; attr}` where ANSI escape code. The list of highlight tags can be retrieved with the ``-list-tags`` command-line option of ``coqtop``. +The string uses ANSI escape codes to represent attributes. For example: + + ``export COQ_COLORS=”diff.added=4;48;2;0;0;240:diff.removed=41”`` + +sets the highlights for added text in diffs to underlined (the 4) with a background RGB +color (0, 0, 240) and for removed text in diffs to a red background. +Note that if you specify ``COQ_COLORS``, the predefined attributes are ignored. + + .. _command-line-options: By command line options @@ -164,9 +175,13 @@ and ``coqtop``, unless stated otherwise: :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or categories (see Section :ref:`controlling-display`). -:-color (on|off|auto): Enable or not the coloring of output of `coqtop`. - Default is auto, meaning that `coqtop` dynamically decides, depending on - whether the output channel supports ANSI escape sequences. +:-color (on|off|auto): *Coqtop only*. Enable or disable color output. + Default is auto, meaning color is shown only if + the output channel supports ANSI escape sequences. +:-diffs (on|off|removed): *Coqtop only*. Controls highlighting of differences + between proof steps. ``on`` highlights added tokens, ``removed`` highlights both added and + removed tokens. Requires that ``–color`` is enabled. (see Section + :ref:`showing_diffs`). :-beautify: Pretty-print each command to *file.beautified* when compiling *file.v*, in order to get old-fashioned syntax/definitions/notations. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5d300c3d6d..19995520bb 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -21,16 +21,16 @@ The most basic custom toplevel is built using: % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ -package coq.toplevel \ - toplevel/coqtop\_bin.ml -o my\_toplevel.native + topbin/coqtop_bin.ml -o my_toplevel.native -For example, to statically link |L_tac|, you can just do: +For example, to statically link |Ltac|, you can just do: :: % ocamlfind ocamlopt -thread -rectypes -linkall -linkpkg \ - -package coq.toplevel -package coq.ltac \ - toplevel/coqtop\_bin.ml -o my\_toplevel.native + -package coq.toplevel,coq.plugins.ltac \ + topbin/coqtop_bin.ml -o my_toplevel.native and similarly for other plugins. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 4b1b7719c5..46851050ac 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -495,6 +495,10 @@ Requesting information eexists ?[n]. Show n. + .. coqtop:: none + + Abort. + .. cmdv:: Show Script :name: Show Script @@ -581,6 +585,164 @@ Requesting information fixpoint and cofixpoint is violated at some time of the construction of the proof without having to wait the completion of the proof. +.. _showing_diffs: + +Showing differences between proof steps +--------------------------------------- + + +Coq can automatically highlight the differences between successive proof steps. +For example, the following screenshots of CoqIDE and coqtop show the application +of the same :tacn:`intros` tactic. The tactic creates two new hypotheses, highlighted in green. +The conclusion is entirely in pale green because although it’s changed, no tokens were added +to it. The second screenshot uses the "removed" option, so it shows the conclusion a +second time with the old text, with deletions marked in red. Also, since the hypotheses are +new, no line of old text is shown for them. + +.. comment screenshot produced with: + Inductive ev : nat -> Prop := + | ev_0 : ev 0 + | ev_SS : forall n : nat, ev n -> ev (S (S n)). + + Fixpoint double (n:nat) := + match n with + | O => O + | S n' => S (S (double n')) + end. + + Goal forall n, ev n -> exists k, n = double k. + intros n E. + +.. + + .. image:: ../_static/diffs-coqide-on.png + :alt: |CoqIDE| with Set Diffs on + +.. + + .. image:: ../_static/diffs-coqide-removed.png + :alt: |CoqIDE| with Set Diffs removed + +.. + + .. image:: ../_static/diffs-coqtop-on3.png + :alt: coqtop with Set Diffs on + +How to enable diffs +``````````````````` + +.. opt:: Diffs %( "on" %| "off" %| "removed" %) + + .. This ref doesn't work: :opt:`Set Diffs %( "on" %| "off" %| "removed" %)` + + The “on” option highlights added tokens in green, while the “removed” option + additionally reprints items with removed tokens in red. Unchanged tokens in + modified items are shown with pale green or red. (Colors are user-configurable.) + +For coqtop, showing diffs can be enabled when starting coqtop with the +``-diffs on|off|removed`` command-line option or with the ``Set Diffs`` +command within Coq. You will need to provide the ``-color on|auto`` command-line option when +you start coqtop in either case. + +Colors for coqtop can be configured by setting the ``COQ_COLORS`` environment +variable. See section :ref:`customization-by-environment-variables`. Diffs +use the tags ``diff.added``, ``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg``. + +In CoqIDE, diffs should be enabled from the ``View`` menu. Don’t use the ``Set Diffs`` +command in CoqIDE. You can change the background colors shown for diffs from the +``Edit | Preferences | Tags`` panel by changing the settings for the ``diff.added``, +``diff.added.bg``, ``diff.removed`` and ``diff.removed.bg`` tags. This panel also +lets you control other attributes of the highlights, such as the foreground +color, bold, italic, underline and strikeout. + +Note: As of this writing (August 2018), Proof General will need minor changes +to be able to show diffs correctly. We hope it will support this feature soon. +See https://github.com/ProofGeneral/PG/issues/381 for the current status. + +How diffs are calculated +```````````````````````` + +Diffs are calculated as follows: + +1. Select the old proof state to compare to, which is the proof state before + the last tactic that changed the proof. Changes that only affect the view + of the proof, such as ``all: swap 1 2``, are ignored. + +2. For each goal in the new proof state, determine what old goal to compare + it to—the one it is derived from or is the same as. Match the hypotheses by + name (order is ignored), handling compacted items specially. + +3. For each hypothesis and conclusion (the “items”) in each goal, pass + them as strings to the lexer to break them into tokens. Then apply the + Myers diff algorithm :cite:`Myers` on the tokens and add appropriate highlighting. + +Notes: + +* Aside from the highlights, output for the "on" option should be identical + to the undiffed output. +* Goals completed in the last proof step will not be shown even with the + "removed" setting. + +.. comment The following screenshots show diffs working with multiple goals and with compacted + hypotheses. In the first one, notice that the goal ``P 1`` is not highlighted at + all after the split because it has not changed. + + .. todo: Use this script and remove the screenshots when COQ_COLORS + works for coqtop in sphinx + .. coqtop:: none + + Set Diffs "on". + Parameter P : nat -> Prop. + Goal P 1 /\ P 2 /\ P 3. + + .. coqtop:: out + + split. + + .. coqtop:: all + + 2: split. + + .. coqtop:: none + + Abort. + + .. + + .. coqtop:: none + + Set Diffs "on". + Goal forall n m : nat, n + m = m + n. + Set Diffs "on". + + .. coqtop:: out + + intros n. + + .. coqtop:: all + + intros m. + + .. coqtop:: none + + Abort. + +This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal +with 2 goals. Notice that the goal ``P 1`` is not highlighted at all after +the split because it has not changed. + +.. + + .. image:: ../_static/diffs-coqide-multigoal.png + :alt: coqide with Set Diffs on with multiple goals + +This is how diffs may appear after applying a :tacn:`intro` tactic that results +in compacted hypotheses: + +.. + + .. image:: ../_static/diffs-coqide-compacted.png + :alt: coqide with Set Diffs on with compacted hyptotheses Controlling the effect of proof editing commands ------------------------------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index f99c539251..db9f04ba11 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2214,6 +2214,7 @@ and an explanation of the underlying technique. ``simple inversion``. .. tacv:: inversion @ident using @ident + :name: inversion ... using ... Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 59cad3bea2..eacd7b4676 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -12,13 +12,15 @@ The ``Scheme`` command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema: -.. cmd:: Scheme @ident := Induction for @ident Sort sort {* with @ident := Induction for @ident Sort sort} +.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort sort {* with @ident__i := Induction for @ident__j Sort sort} -where each `ident'ᵢ` is a different inductive type identifier -belonging to the same package of mutual inductive definitions. This -command generates the `identᵢ`s to be mutually recursive -definitions. Each term `identᵢ` proves a general principle of mutual -induction for objects in type `identᵢ`. + This command is a high-level tool for generating automatically + (possibly mutual) induction principles for given types and sorts. + Each :n:`@ident__j` is a different inductive type identifier belonging to + the same package of mutual inductive definitions. + The command generates the :n:`@ident__i`\s to be mutually recursive + definitions. Each term :n:`@ident__i` proves a general principle of mutual + induction for objects in type :n:`@ident__j`. .. cmdv:: Scheme @ident := Minimality for @ident Sort sort {* with @ident := Minimality for @ident' Sort sort} @@ -44,9 +46,9 @@ induction for objects in type `identᵢ`. .. coqtop:: none - Axiom A : Set. - Axiom B : Set. - + Axiom A : Set. + Axiom B : Set. + .. coqtop:: all Inductive tree : Set := node : A -> forest -> tree @@ -79,7 +81,7 @@ induction for objects in type `identᵢ`. .. coqtop:: all Inductive odd : nat -> Prop := oddS : forall n:nat, even n -> odd (S n) - with even : nat -> Prop := + with even : nat -> Prop := | evenO : even 0 | evenS : forall n:nat, odd n -> even (S n). @@ -136,19 +138,20 @@ Automatic declaration of schemes Combined Scheme ~~~~~~~~~~~~~~~~~~~~~~ -The ``Combined Scheme`` command is a tool for combining induction -principles generated by the ``Scheme command``. Its syntax follows the -schema : - -.. cmd:: Combined Scheme @ident from {+, ident} +.. cmd:: Combined Scheme @ident from {+, @ident__i} -where each identᵢ after the ``from`` is a different inductive principle that must -belong to the same package of mutual inductive principle definitions. -This command generates the leftmost `ident` to be the conjunction of the -principles: it is built from the common premises of the principles and -concluded by the conjunction of their conclusions. + This command is a tool for combining induction principles generated + by the :cmd:`Scheme` command. + Each :n:`@ident__i` is a different inductive principle that must belong + to the same package of mutual inductive principle definitions. + This command generates :n:`@ident` to be the conjunction of the + principles: it is built from the common premises of the principles + and concluded by the conjunction of their conclusions. + In the case where all the inductive principles used are in sort + ``Prop``, the propositional conjunction ``and`` is used, otherwise + the simple product ``prod`` is used instead. -.. example:: +.. example:: We can define the induction principles for trees and forests using: @@ -170,6 +173,23 @@ concluded by the conjunction of their conclusions. Check tree_forest_mutind. +.. example:: + + We can also combine schemes at sort ``Type``: + + .. coqtop:: all + + Scheme tree_forest_rect := Induction for tree Sort Type + with forest_tree_rect := Induction for forest Sort Type. + + .. coqtop:: all + + Combined Scheme tree_forest_mutrect from tree_forest_rect, forest_tree_rect. + + .. coqtop:: all + + Check tree_forest_mutrect. + .. _functional-scheme: Generation of induction principles with ``Functional`` ``Scheme`` @@ -186,7 +206,7 @@ schema: where each `ident'ᵢ` is a different mutually defined function name (the names must be in the same order as when they were defined). This command generates the induction principle for each `identᵢ`, following -the recursive structure and case analyses of the corresponding function +the recursive structure and case analyses of the corresponding function identᵢ’. .. warning:: @@ -196,7 +216,7 @@ identᵢ’. :cmd:`Function` generally produces smaller principles that are closer to how a user would implement them. See :ref:`advanced-recursive-functions` for details. -.. example:: +.. example:: Induction scheme for div2. @@ -262,11 +282,11 @@ identᵢ’. We define trees by the following mutual inductive type: .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning - + .. coqtop:: reset all Axiom A : Set. - + Inductive tree : Set := node : A -> forest -> tree with forest : Set := @@ -313,20 +333,21 @@ identᵢ’. Check tree_size_ind2. .. _derive-inversion: - + Generation of inversion principles with ``Derive`` ``Inversion`` ----------------------------------------------------------------- -The syntax of ``Derive`` ``Inversion`` follows the schema: - .. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort -This command generates an inversion principle for the `inversion … using` -tactic. Let `I` be an inductive predicate and `x` the variables occurring -in t. This command generates and stocks the inversion lemma for the -sort `sort` corresponding to the instance `∀ (x:T), I t` with the name -`ident` in the global environment. When applied, it is equivalent to -having inverted the instance with the tactic `inversion`. + This command generates an inversion principle for the + :tacn:`inversion ... using ...` tactic. Let :g:`I` be an inductive + predicate and :g:`x` the variables occurring in t. This command + generates and stocks the inversion lemma for the sort :g:`sort` + corresponding to the instance :g:`∀ (x:T), I t` with the name + :n:`@ident` in the global environment. When applied, it is + equivalent to having inverted the instance with the tactic + :g:`inversion`. + .. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort sort @@ -347,7 +368,7 @@ having inverted the instance with the tactic `inversion`. Consider the relation `Le` over natural numbers and the following parameter ``P``: - + .. coqtop:: all Inductive Le : nat -> nat -> Set := @@ -370,9 +391,9 @@ having inverted the instance with the tactic `inversion`. .. coqtop:: none - Goal forall (n m : nat) (H : Le (S n) m), P n m. + Goal forall (n m : nat) (H : Le (S n) m), P n m. intros. - + .. coqtop:: all Show. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 0fa42cadad..4cbf75b715 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -600,8 +600,8 @@ through the <tt>Require Import</tt> command.</p> </dt> <dd> theories/Compat/AdmitAxiom.v - theories/Compat/Coq86.v theories/Compat/Coq87.v theories/Compat/Coq88.v + theories/Compat/Coq89.v </dd> </dl> diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index edf4e6ec9d..2c69dcfe08 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -560,6 +560,9 @@ class CoqtopDirective(Directive): Print nat. Definition a := 1. + The blank line after the directive is required. If you begin a proof, + include an ``Abort`` afterwards to reset coqtop for the next example. + Here is a list of permissible options: - Display options |
