Displays the differences between successive proof steps in coqtop and…

… CoqIDE.

Proof General requires minor changes to make the diffs visible, but this code
shouldn't break the existing version of PG.  Also provides an option to generate
diffs in HTML in a file.

Diffs are computed for the hypotheses and conclusion of the first goal between
the old and new proofs. Strings are split into tokens using the Coq lexer,
then the list of tokens are diffed using the Myers algorithm.  A fixup routine
(Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases.

Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or
"-diffs on|off|removed" on the OS command line.  The "on" option shows only the
new item with added text, while "removed" shows each modified item twice--once
with the old value showing removed text and once with the new value showing
added text.

The highlights use 4 tags to specify the color and underline/strikeout.
These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg".
The first two are for added or removed text; the last two are for
unmodified parts of a modified item.

Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and
"end.diff.*", but only on the first and last strings of the span.

CHANGES

@@ -9,7 +9,7 @@ Tactics
 
 - The undocumented "nameless" forms `fix N`, `cofix` that were
   deprecated in 8.8 have been removed from LTAC's syntax; please use
-  `fix ident N/cofix ident` to explicitely name the (co)fixpoint
+  `fix ident N/cofix ident` to explicitly name the (co)fixpoint
   hypothesis to be introduced.
 
 - Introduction tactics "intro"/"intros" on a goal which is an
@@ -55,6 +55,14 @@ Coq binaries and process model
   `coq{proof,tactic,query}worker` are in charge of task-specific and
   parallel proof checking.
 
+Display diffs between proof steps
+
+- coqtop and coqide can now highlight the differences between proof steps
+  in color. This can be enabled from the command line or the
+  "Set Diffs on|off|removed" command. Please see the documentation for
+  details.  Showing diffs in Proof General requires small changes to PG
+  (under discussion).
+
 Changes from 8.8.0 to 8.8.1
 ===========================
 

clib/clib.mllib

@@ -38,3 +38,5 @@ Backtrace
 IStream
 Terminal
 Monad
+
+Diff2

clib/diff2.ml

@@ -0,0 +1,158 @@
+(* copied from https://github.com/leque/ocaml-diff.git and renamed from "diff.ml" *)
+
+(*
+ * Copyright (C) 2016 OOHASHI Daichi
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ * The above copyright notice and this permission notice shall be included in
+ * all copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+ * THE SOFTWARE.
+ *)
+
+type 'a common =
+  [ `Common of int * int * 'a ]
+
+type 'a edit =
+  [ `Added of int * 'a
+  | `Removed of int * 'a
+  | 'a common
+  ]
+
+module type SeqType = sig
+  type t
+  type elem
+  val get : t -> int -> elem
+  val length : t -> int
+end
+
+module type S = sig
+  type t
+  type elem
+
+  val lcs :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem common list
+
+  val diff :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem edit list
+
+  val fold_left :
+      ?equal:(elem -> elem -> bool) ->
+      f:('a -> elem edit -> 'a) ->
+      init:'a ->
+      t -> t -> 'a
+
+  val iter :
+      ?equal:(elem -> elem -> bool) ->
+      f:(elem edit -> unit) ->
+      t -> t -> unit
+end
+
+module Make(M : SeqType) : (S with type t = M.t and type elem = M.elem) = struct
+  type t = M.t
+  type elem = M.elem
+
+  let lcs ?(equal = (=)) a b =
+    let n = M.length a in
+    let m = M.length b in
+    let mn = m + n in
+    let sz = 2 * mn + 1 in
+    let vd = Array.make sz 0 in
+    let vl = Array.make sz 0 in
+    let vr = Array.make sz [] in
+    let get v i = Array.get v (i + mn) in
+    let set v i x = Array.set v (i + mn) x in
+    let finish () =
+      let rec loop i maxl r =
+        if i > mn then
+          List.rev r
+        else if get vl i > maxl then
+          loop (i + 1) (get vl i) (get vr i)
+        else
+          loop (i + 1) maxl r
+      in loop (- mn) 0 []
+    in
+    if mn = 0 then
+      []
+    else
+      (* For d <- 0 to mn Do *)
+      let rec dloop d =
+        assert (d <= mn);
+        (* For k <- -d to d in steps of 2 Do *)
+        let rec kloop k =
+          if k > d then
+            dloop @@ d + 1
+          else
+            let x, l, r =
+              if k = -d || (k <> d && get vd (k - 1) < get vd (k + 1)) then
+                get vd (k + 1), get vl (k + 1), get vr (k + 1)
+              else
+                get vd (k - 1) + 1, get vl (k - 1), get vr (k - 1)
+            in
+            let x, y, l, r =
+              let rec xyloop x y l r =
+                if x < n && y < m && equal (M.get a x) (M.get b y) then
+                  xyloop (x + 1) (y + 1) (l + 1) (`Common(x, y, M.get a x) :: r)
+                else
+                  x, y, l, r
+              in xyloop x (x - k) l r
+            in
+            set vd k x;
+            set vl k l;
+            set vr k r;
+            if x >= n && y >= m then
+              (* Stop *)
+              finish ()
+            else
+              kloop @@ k + 2
+        in kloop @@ -d
+      in dloop 0
+
+  let fold_left ?(equal = (=)) ~f ~init a b =
+    let ff x y = f y x in
+    let fold_map f g x from to_ init =
+      let rec loop i init =
+        if i >= to_ then
+          init
+        else
+          loop (i + 1) (f (g i @@ M.get x i) init)
+      in loop from init
+    in
+    let added i x = `Added (i, x) in
+    let removed i x = `Removed (i, x) in
+    let rec loop cs apos bpos init =
+      match cs with
+      | [] ->
+          init
+          |> fold_map ff removed a apos (M.length a)
+          |> fold_map ff added b bpos (M.length b)
+      | `Common (aoff, boff, _) as e :: rest ->
+          init
+          |> fold_map ff removed a apos aoff
+          |> fold_map ff added b bpos boff
+          |> ff e
+          |> loop rest (aoff + 1) (boff + 1)
+    in loop (lcs ~equal a b) 0 0 init
+
+  let diff ?(equal = (=)) a b =
+    fold_left ~equal ~f:(fun xs x -> x::xs) ~init:[] a b
+
+  let iter ?(equal = (=)) ~f a b =
+    fold_left a b
+      ~equal
+      ~f:(fun () x -> f x)
+      ~init:()
+end

clib/diff2.mli

@@ -0,0 +1,101 @@
+(* copied from https://github.com/leque/ocaml-diff.git and renamed from "diff.mli" *)
+(**
+   An implementation of Eugene Myers' O(ND) Difference Algorithm\[1\].
+   This implementation is a port of util.lcs module of
+   {{:http://practical-scheme.net/gauche} Gauche Scheme interpreter}.
+
+   - \[1\] Eugene Myers, An O(ND) Difference Algorithm and Its Variations, Algorithmica Vol. 1 No. 2, pp. 251-266, 1986.
+ *)
+
+type 'a common = [
+    `Common of int * int * 'a
+  ]
+(** an element of lcs of seq1 and seq2 *)
+
+type 'a edit =
+  [ `Removed of int * 'a
+  | `Added of int * 'a
+  | 'a common
+  ]
+(** an element of diff of seq1 and seq2. *)
+
+module type SeqType = sig
+  type t
+  (** The type of the sequence. *)
+
+  type elem
+  (** The type of the elements of the sequence. *)
+
+  val get : t -> int -> elem
+  (** [get t n] returns [n]-th element of the sequence [t]. *)
+
+  val length : t -> int
+  (** [length t] returns the length of the sequence [t]. *)
+end
+(** Input signature of {!Diff.Make}. *)
+
+module type S = sig
+  type t
+  (** The type of input sequence. *)
+
+  type elem
+  (** The type of the elements of result / input sequence. *)
+
+  val lcs :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem common list
+  (**
+     [lcs ~equal seq1 seq2] computes the LCS (longest common sequence) of
+     [seq1] and [seq2].
+     Elements of [seq1] and [seq2] are compared with [equal].
+     [equal] defaults to [Pervasives.(=)].
+
+     Elements of lcs are [`Common (pos1, pos2, e)]
+     where [e] is an element, [pos1] is a position in [seq1],
+     and [pos2] is a position in [seq2].
+   *)
+
+  val diff :
+      ?equal:(elem -> elem -> bool) ->
+      t -> t -> elem edit list
+  (**
+     [diff ~equal seq1 seq2] computes the diff of [seq1] and [seq2].
+     Elements of [seq1] and [seq2] are compared with [equal].
+
+     Elements only in [seq1] are represented as [`Removed (pos, e)]
+     where [e] is an element, and [pos] is a position in [seq1];
+     those only in [seq2] are represented as [`Added (pos, e)]
+     where [e] is an element, and [pos] is a position in [seq2];
+     those common in [seq1] and [seq2] are represented as
+     [`Common (pos1, pos2, e)]
+     where [e] is an element, [pos1] is a position in [seq1],
+     and [pos2] is a position in [seq2].
+   *)
+
+  val fold_left :
+      ?equal:(elem -> elem -> bool) ->
+      f:('a -> elem edit -> 'a) ->
+      init:'a ->
+      t -> t -> 'a
+  (**
+     [fold_left ~equal ~f ~init seq1 seq2] is same as
+     [diff ~equal seq1 seq2 |> ListLabels.fold_left ~f ~init],
+     but does not create an intermediate list.
+   *)
+
+  val iter :
+      ?equal:(elem -> elem -> bool) ->
+      f:(elem edit -> unit) ->
+      t -> t -> unit
+  (**
+     [iter ~equal ~f seq1 seq2] is same as
+     [diff ~equal seq1 seq2 |> ListLabels.iter ~f],
+     but does not create an intermediate list.
+   *)
+end
+(** Output signature of {!Diff.Make}. *)
+
+module Make :
+  functor (M : SeqType) -> (S with type t = M.t and type elem = M.elem)
+(** Functor building an implementation of the diff structure
+    given a sequence type.  *)

ide/idetop.ml

@@ -202,13 +202,27 @@ let export_pre_goals pgs =
     Interface.given_up_goals = pgs.Proof.given_up_goals
   }
 
+let add_diffs oldp newp intf =
+  let open Interface in
+  let (hyps_pp_list, concl_pp) = Proof_diffs.diff_first_goal oldp newp in
+  match intf.fg_goals with
+  | [] -> intf
+  | first_goal :: tl ->
+    { intf with fg_goals = { first_goal with goal_hyp = hyps_pp_list; goal_ccl = concl_pp } :: tl }
+
 let goals () =
+  let oldp =
+    try Some (Proof_global.give_me_the_proof ())
+    with Proof_global.NoCurrentProof -> None in
   let doc = get_doc () in
   set_doc @@ Stm.finish ~doc;
   try
-    let pfts = Proof_global.give_me_the_proof () in
-    Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
-  with Proof_global.NoCurrentProof -> None
+    let newp = Proof_global.give_me_the_proof () in
+    let intf = export_pre_goals (Proof.map_structured_proof newp process_goal) in
+    try
+      Some (add_diffs oldp (Some newp) intf)
+    with Pp_diff.Diff_Failure _ -> Some intf
+  with Proof_global.NoCurrentProof -> None;;
 
 let evars () =
   try
@@ -515,6 +529,9 @@ let () = Usage.add_to_usage "coqidetop"
 let islave_init ~opts extra_args =
   let args = parse extra_args in
   CoqworkmgrApi.(init High);
+  let open Coqargs in
+    if not opts.diffs_set then
+      Proof_diffs.write_diffs_option "on";
   opts, args
 
 let () =