Documentation for proof diffs

13 files changed, 197 insertions, 3 deletions

diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index c1f3f7b4d0..062e14d615 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -220,6 +220,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
new 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
new 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
new 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
new 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
new 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
new 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
new 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
new 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/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/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/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 7992c10abb..029e100800 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -558,6 +558,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