aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/09-coqide/12874-show_proof_diffs.rst5
-rw-r--r--doc/sphinx/_static/diffs-show-proof.pngbin0 -> 13641 bytes
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst38
-rw-r--r--ide/coqide/coq.ml4
-rw-r--r--ide/coqide/coq.mli5
-rw-r--r--ide/coqide/coqOps.ml22
-rw-r--r--ide/coqide/coqOps.mli2
-rw-r--r--ide/coqide/coqide.ml33
-rw-r--r--ide/coqide/coqide_ui.ml1
-rw-r--r--ide/coqide/fake_ide.ml30
-rw-r--r--ide/coqide/idetop.ml19
-rw-r--r--ide/coqide/protocol/interface.ml5
-rw-r--r--ide/coqide/protocol/xmlprotocol.ml31
-rw-r--r--ide/coqide/protocol/xmlprotocol.mli1
-rw-r--r--lib/flags.ml1
-rw-r--r--lib/flags.mli1
-rw-r--r--lib/pp_diff.ml14
-rw-r--r--printing/proof_diffs.ml22
-rw-r--r--printing/proof_diffs.mli6
-rw-r--r--test-suite/ide/proof-diffs.fake10
-rw-r--r--toplevel/coqargs.ml1
-rw-r--r--toplevel/coqloop.ml44
-rw-r--r--toplevel/g_toplevel.mlg5
-rw-r--r--toplevel/usage.ml1
24 files changed, 225 insertions, 76 deletions
diff --git a/doc/changelog/09-coqide/12874-show_proof_diffs.rst b/doc/changelog/09-coqide/12874-show_proof_diffs.rst
new file mode 100644
index 0000000000..51bebad9be
--- /dev/null
+++ b/doc/changelog/09-coqide/12874-show_proof_diffs.rst
@@ -0,0 +1,5 @@
+- **Added:**
+ Support showing diffs for :cmd:`Show Proof` in CoqIDE from the :n:`View` menu.
+ See :ref:`showing_proof_diffs`.
+ (`#12874 <https://github.com/coq/coq/pull/12874>`_,
+ by Jim Fehrle and Enrico Tassi)
diff --git a/doc/sphinx/_static/diffs-show-proof.png b/doc/sphinx/_static/diffs-show-proof.png
new file mode 100644
index 0000000000..62bd9cccd0
--- /dev/null
+++ b/doc/sphinx/_static/diffs-show-proof.png
Binary files differ
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 00aafe1266..2cf436b27e 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -586,11 +586,11 @@ Requesting information
constructed. Each hole is an existential variable, which appears as a
question mark followed by an identifier.
- Experimental: Specifying “Diffs” highlights the difference between the
+ Specifying “Diffs” highlights the difference between the
current and previous proof step. By default, the command shows the
output once with additions highlighted. Including “removed” shows
the output twice: once showing removals and once showing additions.
- It does not examine the :opt:`Diffs` option. See :ref:`showing_diffs`.
+ It does not examine the :opt:`Diffs` option. See :ref:`showing_proof_diffs`.
.. cmdv:: Show Conjectures
:name: Show Conjectures
@@ -671,12 +671,9 @@ Requesting information
Showing differences between proof steps
---------------------------------------
-
Coq can automatically highlight the differences between successive proof steps
-and between values in some error messages. Also, as an experimental feature,
-Coq can also highlight differences between proof steps shown in the :cmd:`Show Proof`
-command, but only, for now, when using coqtop and Proof General.
-
+and between values in some error messages. Coq can also highlight differences
+in the proof term.
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
@@ -822,14 +819,37 @@ 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:
+Diffs may appear like this after applying a :tacn:`intro` tactic that results
+in a compacted hypotheses:
..
.. image:: ../_static/diffs-coqide-compacted.png
:alt: coqide with Set Diffs on with compacted hypotheses
+.. _showing_proof_diffs:
+
+"Show Proof" differences
+````````````````````````
+
+To show differences in the proof term:
+
+- In coqtop and Proof General, use the :cmd:`Show Proof` `Diffs` command.
+
+- In CoqIDE, position the cursor on or just after a tactic to compare the proof term
+ after the tactic with the proof term before the tactic, then select
+ `View / Show Proof` from the menu or enter the associated key binding.
+ Differences will be shown applying the current `Show Diffs` setting
+ from the `View` menu. If the current setting is `Don't show diffs`, diffs
+ will not be shown.
+
+ Output with the "added and removed" option looks like this:
+
+ ..
+
+ .. image:: ../_static/diffs-show-proof.png
+ :alt: coqide with Set Diffs on with compacted hypotheses
+
Controlling the effect of proof editing commands
------------------------------------------------
diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml
index 57cdccce6d..6e5d57c9a5 100644
--- a/ide/coqide/coq.ml
+++ b/ide/coqide/coq.ml
@@ -512,6 +512,7 @@ let hints x = eval_call (Xmlprotocol.hints x)
let search flags = eval_call (Xmlprotocol.search flags)
let init x = eval_call (Xmlprotocol.init x)
let stop_worker x = eval_call (Xmlprotocol.stop_worker x)
+let proof_diff x = eval_call (Xmlprotocol.proof_diff x)
let break_coqtop coqtop workers =
if coqtop.status = Busy then
@@ -578,6 +579,9 @@ struct
let set (type a) (opt : a t) (v : a) =
Hashtbl.replace current_state (opt_name opt) (opt_data opt v)
+ let get (type a) (opt : a t) =
+ Hashtbl.find current_state (opt_name opt)
+
let reset () =
let init_descr d = List.iter (fun o -> set o d.init) d.opts in
List.iter init_descr bool_items;
diff --git a/ide/coqide/coq.mli b/ide/coqide/coq.mli
index 82df36c91c..aaaf14e4d0 100644
--- a/ide/coqide/coq.mli
+++ b/ide/coqide/coq.mli
@@ -127,6 +127,7 @@ val hints : Interface.hints_sty -> Interface.hints_rty query
val mkcases : Interface.mkcases_sty -> Interface.mkcases_rty query
val search : Interface.search_sty -> Interface.search_rty query
val init : Interface.init_sty -> Interface.init_rty query
+val proof_diff : Interface.proof_diff_sty -> Interface.proof_diff_rty query
val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query
@@ -144,6 +145,10 @@ sig
val set : 'a t -> 'a -> unit
+ val get : 'a t -> Interface.option_value
+
+ val diff : string t
+
val printing_unfocused: unit -> bool
(** [enforce] transmits to coq the current option values.
diff --git a/ide/coqide/coqOps.ml b/ide/coqide/coqOps.ml
index 29ea3ce9ea..97076745a3 100644
--- a/ide/coqide/coqOps.ml
+++ b/ide/coqide/coqOps.ml
@@ -142,6 +142,7 @@ object
method handle_reset_initial : unit task
method raw_coq_query :
route_id:int -> next:(query_rty value -> unit task) -> string -> unit task
+ method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task
method show_goals : unit task
method backtrack_last_phrase : unit task
method initialize : unit task
@@ -361,6 +362,27 @@ object(self)
let query = Coq.query (route_id,(phrase,sid)) in
Coq.bind (Coq.seq action query) next
+ method proof_diff where ~next : unit Coq.task =
+ (* todo: would be nice to ignore comments, too *)
+ let rec back iter =
+ if iter#is_start then iter
+ else
+ let c = iter#char in
+ if Glib.Unichar.isspace c || c = 0 then back (iter#backward_char)
+ else if c = int_of_char '.' then iter#backward_char
+ else iter in
+
+ let where = back (buffer#get_iter_at_mark where) in
+ let until _ start stop =
+ (buffer#get_iter_at_mark stop)#compare where >= 0 &&
+ (buffer#get_iter_at_mark start)#compare where <= 0 in
+ let state_id = fst @@ self#find_id until in
+ let diff_opt = Interface.(match Coq.PrintOpt.(get diff) with
+ | StringValue diffs -> diffs
+ | _ -> "off") in
+ let proof_diff = Coq.proof_diff (diff_opt, state_id) in
+ Coq.bind proof_diff next
+
method private still_valid { edit_id = id } =
try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true
with Not_found -> false
diff --git a/ide/coqide/coqOps.mli b/ide/coqide/coqOps.mli
index 3a4678ae9c..84911a6aa8 100644
--- a/ide/coqide/coqOps.mli
+++ b/ide/coqide/coqOps.mli
@@ -20,6 +20,7 @@ object
method handle_reset_initial : unit task
method raw_coq_query :
route_id:int -> next:(query_rty value -> unit task) -> string -> unit task
+ method proof_diff : GText.mark -> next:(Pp.t value -> unit task) -> unit task
method show_goals : unit task
method backtrack_last_phrase : unit task
method initialize : unit task
@@ -30,7 +31,6 @@ object
method get_errors : (int * string) list
method get_slaves_status : int * int * string CString.Map.t
-
method handle_failure : handle_exn_rty -> unit task
method destroy : unit -> unit
diff --git a/ide/coqide/coqide.ml b/ide/coqide/coqide.ml
index b66da11e7b..f9e6e74372 100644
--- a/ide/coqide/coqide.ml
+++ b/ide/coqide/coqide.ml
@@ -747,6 +747,24 @@ let coq_icon () =
let dir = List.find chk (Minilib.coqide_data_dirs ()) in
Filename.concat dir name
+let show_proof_diff where sn =
+ sn.messages#default_route#clear;
+ Coq.try_grab sn.coqtop (sn.coqops#proof_diff where
+ ~next:(function
+ | Interface.Fail (_, _, err) ->
+ let err = if (Pp.string_of_ppcmds err) <> "No proofs to diff." then err else
+ Pp.str "Put the cursor over proven lines for \"Show Proof\" diffs"
+ in
+ let err = Ideutils.validate err in
+ sn.messages#default_route#add err;
+ Coq.return ()
+ | Interface.Good diff ->
+ sn.messages#default_route#add diff;
+ Coq.return ()))
+ ignore
+
+let show_proof_diffs _ = cb_on_current_term (show_proof_diff `INSERT) ()
+
let about _ =
let dialog = GWindow.about_dialog () in
let _ = dialog#connect#response ~callback:(fun _ -> dialog#destroy ()) in
@@ -1103,6 +1121,8 @@ let build_ui () =
radio "Set diff" 1 ~label:"Show diffs: only _added";
radio "Set removed diff" 2 ~label:"Show diffs: added and _removed";
];
+ item "Show Proof Diffs" ~label:"_Show Proof (with diffs, if set)" ~accel:(modifier_for_display#get ^ "S")
+ ~callback:MiscMenu.show_proof_diffs;
];
toggle_items view_menu Coq.PrintOpt.bool_items;
@@ -1352,6 +1372,11 @@ let main files =
this default coqtop path *)
let read_coqide_args argv =
+ let set_debug () =
+ Minilib.debug := true;
+ Flags.debug := true;
+ Exninfo.record_backtrace true
+ in
let rec filter_coqtop coqtop project_files bindings_files out = function
|"-unicode-bindings" :: sfilenames :: args ->
let filenames = Str.split (Str.regexp ",") sfilenames in
@@ -1371,10 +1396,12 @@ let read_coqide_args argv =
|"-coqtop" :: [] ->
output_string stderr "Error: missing argument after -coqtop"; exit 1
|"-debug"::args ->
- Minilib.debug := true;
- Flags.debug := true;
- Exninfo.record_backtrace true;
+ set_debug ();
filter_coqtop coqtop project_files bindings_files ("-debug"::out) args
+ |"-xml-debug"::args ->
+ set_debug ();
+ Flags.xml_debug := true;
+ filter_coqtop coqtop project_files bindings_files ("-xml-debug"::out) args
|"-coqtop-flags" :: flags :: args->
Coq.ideslave_coqtop_flags := Some flags;
filter_coqtop coqtop project_files bindings_files out args
diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml
index e9ff1bbba1..6540fc6fca 100644
--- a/ide/coqide/coqide_ui.ml
+++ b/ide/coqide/coqide_ui.ml
@@ -89,6 +89,7 @@ let init () =
\n <menuitem action='Unset diff' />\
\n <menuitem action='Set diff' />\
\n <menuitem action='Set removed diff' />\
+\n <menuitem action='Show Proof Diffs' />\
\n </menu>\
\n <menu action='Navigation'>\
\n <menuitem action='Forward' />\
diff --git a/ide/coqide/fake_ide.ml b/ide/coqide/fake_ide.ml
index e1736a5fe0..034f5b4e2a 100644
--- a/ide/coqide/fake_ide.ml
+++ b/ide/coqide/fake_ide.ml
@@ -136,7 +136,7 @@ module Parser = struct (* {{{ *)
match g with
| Item (s,_) -> Printf.sprintf "%s" (clean s)
| Opt g -> Printf.sprintf "[%s]" (print g)
- | Alt gs -> Printf.sprintf "( %s )" (String.concat " | " (List.map print gs))
+ | Alt gs -> Printf.sprintf "( %s )" (String.concat "\n| " (List.map print gs))
| Seq gs -> String.concat " " (List.map print gs)
let rec print_toklist = function
@@ -253,6 +253,9 @@ let eval_print l coq =
after_edit_at (to_id, need_unfocus) (base_eval_call (edit_at to_id) coq)
| [ Tok(_,"QUERY"); Top []; Tok(_,phrase) ] ->
eval_call (query (0,(phrase,tip_id()))) coq
+ | [ Tok(_,"PDIFF"); Tok(_,id) ] ->
+ let to_id, _ = get_id id in
+ eval_call (proof_diff ("on",to_id)) coq
| [ Tok(_,"QUERY"); Top [Tok(_,id)]; Tok(_,phrase) ] ->
let to_id, _ = get_id id in
eval_call (query (0,(phrase, to_id))) coq
@@ -282,6 +285,7 @@ let grammar =
; Seq [Item (eat_rex "FAILADD"); Item eat_phrase]
; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
+ ; Seq [Item (eat_rex "PDIFF"); Item eat_id ]
; Seq [Item (eat_rex "WAIT")]
; Seq [Item (eat_rex "JOIN")]
; Seq [Item (eat_rex "GOALS")]
@@ -295,12 +299,11 @@ let grammar =
let read_command inc = Parser.parse grammar inc
let usage () =
- error (Printf.sprintf
- "A fake coqide process talking to a coqtop -toploop coqidetop.\n\
- Usage: %s (file|-) [<coqtop>]\n\
- Input syntax is the following:\n%s\n"
- (Filename.basename Sys.argv.(0))
- (Parser.print grammar))
+ prerr_endline (Printf.sprintf "Usage: %s ( file | - ) [ \"<coqtop arguments>\" ]\n\
+ Input syntax is:\n%s\n"
+ (Filename.basename Sys.argv.(0))
+ (Parser.print grammar));
+ exit 1
module Coqide = Spawn.Sync ()
@@ -308,14 +311,15 @@ let main =
if Sys.os_type = "Unix" then Sys.set_signal Sys.sigpipe
(Sys.Signal_handle
(fun _ -> prerr_endline "Broken Pipe (coqtop died ?)"; exit 1));
- let def_args = ["--xml_format=Ppcmds"] in
let idetop_name = System.get_toplevel_path "coqidetop" in
- let coqtop_args, input_file = match Sys.argv with
- | [| _; f |] -> Array.of_list def_args, f
- | [| _; f; ct |] ->
- let ct = Str.split (Str.regexp " ") ct in
- Array.of_list (def_args @ ct), f
+ let input_file, args = match Sys.argv with
+ | [| _; f |] -> f, []
+ | [| _; f; args |] ->
+ let args = Str.split (Str.regexp " ") args in
+ f, args
| _ -> usage () in
+ let def_coqtop_args = ["--xml_format=Ppcmds"] in
+ let coqtop_args = Array.of_list(def_coqtop_args @ args) in
let inc = if input_file = "-" then stdin else open_in input_file in
prerr_endline ("Running: "^idetop_name^" "^
(String.concat " " (Array.to_list coqtop_args)));
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml
index 2adc35ae3e..2be8f862ea 100644
--- a/ide/coqide/idetop.ml
+++ b/ide/coqide/idetop.ml
@@ -367,6 +367,17 @@ let export_option_state s = {
Interface.opt_value = export_option_value s.Goptions.opt_value;
}
+exception NotSupported of string
+
+let proof_diff (diff_opt, sid) =
+ let diff_opt = Proof_diffs.string_to_diffs diff_opt in
+ let doc = get_doc () in
+ match Stm.get_proof ~doc sid with
+ | None -> CErrors.user_err (Pp.str "No proofs to diff.")
+ | Some proof ->
+ let old = Stm.get_prev_proof ~doc sid in
+ Proof_diffs.diff_proofs ~diff_opt ?old proof
+
let get_options () =
let table = Goptions.get_tables () in
let fold key state accu = (key, export_option_state state) :: accu in
@@ -455,6 +466,7 @@ let eval_call c =
Interface.hints = interruptible hints;
Interface.status = interruptible status;
Interface.search = interruptible search;
+ Interface.proof_diff = interruptible proof_diff;
Interface.get_options = interruptible get_options;
Interface.set_options = interruptible set_options;
Interface.mkcases = interruptible idetop_make_cases;
@@ -479,6 +491,8 @@ let print_xml =
let m = Mutex.create () in
fun oc xml ->
Mutex.lock m;
+ if !Flags.xml_debug then
+ Printf.printf "SENT --> %s\n%!" (Xml_printer.to_string_fmt xml);
try Control.protect_sigalrm (Xml_printer.print oc) xml; Mutex.unlock m
with e -> let e = Exninfo.capture e in Mutex.unlock m; Exninfo.iraise e
@@ -507,7 +521,7 @@ let loop run_mode ~opts:_ state =
set_doc state.doc;
init_signal_handler ();
catch_break := false;
- let in_ch, out_ch = Spawned.get_channels () in
+ let in_ch, out_ch = Spawned.get_channels () in
let xml_oc = Xml_printer.make (Xml_printer.TChannel out_ch) in
let in_lb = Lexing.from_function (fun s len ->
CThread.thread_friendly_read in_ch s ~off:0 ~len) in
@@ -518,7 +532,8 @@ let loop run_mode ~opts:_ state =
while not !quit do
try
let xml_query = Xml_parser.parse xml_ic in
-(* pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
+ if !Flags.xml_debug then
+ pr_with_pid (Xml_printer.to_string_fmt xml_query);
let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in
let () = pr_debug_call q in
let r = eval_call q in
diff --git a/ide/coqide/protocol/interface.ml b/ide/coqide/protocol/interface.ml
index 646012dcaa..86a81446e8 100644
--- a/ide/coqide/protocol/interface.ml
+++ b/ide/coqide/protocol/interface.ml
@@ -187,6 +187,10 @@ type status_rty = status
type search_sty = search_flags
type search_rty = string coq_object list
+(** Diffs between the proof term at a given stateid and the previous one *)
+type proof_diff_sty = string * Stateid.t
+type proof_diff_rty = Pp.t
+
(** Retrieve the list of options of the current toplevel *)
type get_options_sty = unit
type get_options_rty = (option_name * option_state) list
@@ -252,6 +256,7 @@ type handler = {
stop_worker : stop_worker_sty -> stop_worker_rty;
print_ast : print_ast_sty -> print_ast_rty;
annotate : annotate_sty -> annotate_rty;
+ proof_diff : proof_diff_sty -> proof_diff_rty;
handle_exn : handle_exn_sty -> handle_exn_rty;
init : init_sty -> init_rty;
quit : quit_sty -> quit_rty;
diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml
index 6cb0cec008..0780f03903 100644
--- a/ide/coqide/protocol/xmlprotocol.ml
+++ b/ide/coqide/protocol/xmlprotocol.ml
@@ -12,7 +12,7 @@
(** WARNING: TO BE UPDATED WHEN MODIFIED! *)
-let protocol_version = "20170413"
+let protocol_version = "20200911"
type msg_format = Richpp of int | Ppcmds
let msg_format = ref (Richpp 72)
@@ -278,6 +278,7 @@ module ReifType : sig
val state_id_t : state_id val_t
val route_id_t : route_id val_t
val search_cst_t : search_constraint val_t
+ val pp_t : Pp.t val_t
val of_value_type : 'a val_t -> 'a -> xml
val to_value_type : 'a val_t -> xml -> 'a
@@ -314,6 +315,7 @@ end = struct
| State_id : state_id val_t
| Route_id : route_id val_t
| Search_cst : search_constraint val_t
+ | Pp : Pp.t val_t
type value_type = Value_type : 'a val_t -> value_type
@@ -340,6 +342,7 @@ end = struct
let state_id_t = State_id
let route_id_t = Route_id
let search_cst_t = Search_cst
+ let pp_t = Pp
let of_value_type (ty : 'a val_t) : 'a -> xml =
let rec convert : type a. a val_t -> a -> xml = function
@@ -362,6 +365,7 @@ end = struct
| State_id -> of_stateid
| Route_id -> of_routeid
| Search_cst -> of_search_cst
+ | Pp -> of_pp
in
convert ty
@@ -386,6 +390,7 @@ end = struct
| State_id -> to_stateid
| Route_id -> to_routeid
| Search_cst -> to_search_cst
+ | Pp -> to_pp
in
convert ty
@@ -443,6 +448,8 @@ end = struct
| In_Module s -> "In_Module " ^ String.concat "." s
| Include_Blacklist -> "Include_Blacklist"
+ let pr_pp = Pp.string_of_ppcmds
+
let rec print : type a. a val_t -> a -> string = function
| Unit -> pr_unit
| Bool -> pr_bool
@@ -463,6 +470,7 @@ end = struct
| Union (t1,t2) -> (pr_union (print t1) (print t2))
| State_id -> pr_state_id
| Route_id -> pr_int
+ | Pp -> pr_pp
(* This is to break if a rename/refactoring makes the strings below outdated *)
type 'a exists = bool
@@ -489,6 +497,7 @@ end = struct
Printf.sprintf "((%s, %s) CSig.union)" (print_val_t t1) (print_val_t t2)
| State_id -> assert(true : Stateid.t exists); "Stateid.t"
| Route_id -> assert(true : route_id exists); "route_id"
+ | Pp -> assert(true : Pp.t exists); "Pp.t"
let print_type = function Value_type ty -> print_val_t ty
@@ -507,6 +516,8 @@ end = struct
(pr_xml (of_pair of_bool of_int (false,3)));
Printf.printf "%s:\n\n%s\n\n" (print_val_t (Union (Bool,Int)))
(pr_xml (of_union of_bool of_int (Inl false)));
+ Printf.printf "%s:\n\n%s\n\n" (print_val_t Pp)
+ (pr_xml (of_pp Pp.(hv 3 (str "foo" ++ spc () ++ str "bar") )));
print_endline ("All other types are records represented by a node named like the OCaml\n"^
"type which contains a flattened n-tuple. We provide one example.\n");
Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state)
@@ -538,6 +549,7 @@ let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t
let stop_worker_sty_t : stop_worker_sty val_t = string_t
let print_ast_sty_t : print_ast_sty val_t = state_id_t
let annotate_sty_t : annotate_sty val_t = string_t
+let proof_diff_sty_t : proof_diff_sty val_t = pair_t string_t state_id_t
let add_rty_t : add_rty val_t =
pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t)
@@ -563,6 +575,7 @@ let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string
let stop_worker_rty_t : stop_worker_rty val_t = unit_t
let print_ast_rty_t : print_ast_rty val_t = xml_t
let annotate_rty_t : annotate_rty val_t = xml_t
+let proof_diff_rty_t : proof_diff_rty val_t = pp_t
let ($) x = erase x
let calls = [|
@@ -585,6 +598,7 @@ let calls = [|
"StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t;
"PrintAst", ($)print_ast_sty_t, ($)print_ast_rty_t;
"Annotate", ($)annotate_sty_t, ($)annotate_rty_t;
+ "PDiff", ($)proof_diff_sty_t, ($)proof_diff_rty_t;
|]
type 'a call =
@@ -609,7 +623,9 @@ type 'a call =
| Interp : interp_sty -> interp_rty call
| PrintAst : print_ast_sty -> print_ast_rty call
| Annotate : annotate_sty -> annotate_rty call
+ | PDiff : proof_diff_sty -> proof_diff_rty call
+(* the order of the entries must match the order in "calls" above *)
let id_of_call : type a. a call -> int = function
| Add _ -> 0
| Edit_at _ -> 1
@@ -630,6 +646,7 @@ let id_of_call : type a. a call -> int = function
| StopWorker _ -> 16
| PrintAst _ -> 17
| Annotate _ -> 18
+ | PDiff _ -> 19
let str_of_call c = pi1 calls.(id_of_call c)
@@ -652,8 +669,9 @@ let init x : init_rty call = Init x
let wait x : wait_rty call = Wait x
let interp x : interp_rty call = Interp x
let stop_worker x : stop_worker_rty call = StopWorker x
-let print_ast x : print_ast_rty call = PrintAst x
-let annotate x : annotate_rty call = Annotate x
+let print_ast x : print_ast_rty call = PrintAst x
+let annotate x : annotate_rty call = Annotate x
+let proof_diff x : proof_diff_rty call = PDiff x
let abstract_eval_call : type a. _ -> a call -> a value = fun handler c ->
let mkGood : type a. a -> a value = fun x -> Good x in
@@ -678,6 +696,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c ->
| StopWorker x -> mkGood (handler.stop_worker x)
| PrintAst x -> mkGood (handler.print_ast x)
| Annotate x -> mkGood (handler.annotate x)
+ | PDiff x -> mkGood (handler.proof_diff x)
with any ->
let any = Exninfo.capture any in
Fail (handler.handle_exn any)
@@ -703,6 +722,7 @@ let of_answer : type a. a call -> a value -> xml = function
| StopWorker _ -> of_value (of_value_type stop_worker_rty_t)
| PrintAst _ -> of_value (of_value_type print_ast_rty_t )
| Annotate _ -> of_value (of_value_type annotate_rty_t )
+ | PDiff _ -> of_value (of_value_type proof_diff_rty_t )
let of_answer msg_fmt =
msg_format := msg_fmt; of_answer
@@ -727,6 +747,7 @@ let to_answer : type a. a call -> xml -> a value = function
| StopWorker _ -> to_value (to_value_type stop_worker_rty_t)
| PrintAst _ -> to_value (to_value_type print_ast_rty_t )
| Annotate _ -> to_value (to_value_type annotate_rty_t )
+ | PDiff _ -> to_value (to_value_type proof_diff_rty_t )
let of_call : type a. a call -> xml = fun q ->
let mkCall x = constructor "call" (str_of_call q) [x] in
@@ -750,6 +771,7 @@ let of_call : type a. a call -> xml = fun q ->
| StopWorker x -> mkCall (of_value_type stop_worker_sty_t x)
| PrintAst x -> mkCall (of_value_type print_ast_sty_t x)
| Annotate x -> mkCall (of_value_type annotate_sty_t x)
+ | PDiff x -> mkCall (of_value_type proof_diff_sty_t x)
let to_call : xml -> unknown_call =
do_match "call" (fun s a ->
@@ -774,6 +796,7 @@ let to_call : xml -> unknown_call =
| "StopWorker" -> Unknown (StopWorker (mkCallArg stop_worker_sty_t a))
| "PrintAst" -> Unknown (PrintAst (mkCallArg print_ast_sty_t a))
| "Annotate" -> Unknown (Annotate (mkCallArg annotate_sty_t a))
+ | "PDiff" -> Unknown (PDiff (mkCallArg proof_diff_sty_t a))
| x -> raise (Marshal_error("call",PCData x)))
(** Debug printing *)
@@ -805,6 +828,7 @@ let pr_full_value : type a. a call -> a value -> string = fun call value -> matc
| StopWorker _ -> pr_value_gen (print stop_worker_rty_t) value
| PrintAst _ -> pr_value_gen (print print_ast_rty_t ) value
| Annotate _ -> pr_value_gen (print annotate_rty_t ) value
+ | PDiff _ -> pr_value_gen (print proof_diff_rty_t ) value
let pr_call : type a. a call -> string = fun call ->
let return what x = str_of_call call ^ " " ^ print what x in
match call with
@@ -827,6 +851,7 @@ let pr_call : type a. a call -> string = fun call ->
| StopWorker x -> return stop_worker_sty_t x
| PrintAst x -> return print_ast_sty_t x
| Annotate x -> return annotate_sty_t x
+ | PDiff x -> return proof_diff_sty_t x
let document to_string_fmt =
Printf.printf "=== Available calls ===\n\n";
diff --git a/ide/coqide/protocol/xmlprotocol.mli b/ide/coqide/protocol/xmlprotocol.mli
index 44584d44d7..4dc05c18a9 100644
--- a/ide/coqide/protocol/xmlprotocol.mli
+++ b/ide/coqide/protocol/xmlprotocol.mli
@@ -37,6 +37,7 @@ val wait : wait_sty -> wait_rty call
val interp : interp_sty -> interp_rty call
val print_ast : print_ast_sty -> print_ast_rty call
val annotate : annotate_sty -> annotate_rty call
+val proof_diff : proof_diff_sty -> proof_diff_rty call
val abstract_eval_call : handler -> 'a call -> 'a value
diff --git a/lib/flags.ml b/lib/flags.ml
index 1d9d6d49bc..83733cf00d 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -47,6 +47,7 @@ let async_proofs_is_worker () = !async_proofs_worker_id <> "master"
let load_vos_libraries = ref false
let debug = ref false
+let xml_debug = ref false
let in_debugger = ref false
let in_toplevel = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 30d1b5b2bd..ebd23a4d20 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -41,6 +41,7 @@ val load_vos_libraries : bool ref
(** Debug flags *)
val debug : bool ref
+val xml_debug : bool ref
val in_debugger : bool ref
val in_toplevel : bool ref
diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml
index 988e8e4303..4593bf4b07 100644
--- a/lib/pp_diff.ml
+++ b/lib/pp_diff.ml
@@ -109,7 +109,7 @@ let shorten_diff_span dtype diff_list =
iter 0 len (<) 1; (* left to right *)
iter (len-1) (-1) (>) (-1); (* right to left *)
- if !changed then Array.to_list diffs else diff_list;;
+ if !changed then Array.to_list diffs else diff_list
let has_changes diffs =
let rec has_changes_r diffs added removed =
@@ -118,12 +118,12 @@ let has_changes diffs =
| `Removed _ :: t -> has_changes_r t added true
| h :: t -> has_changes_r t added removed
| [] -> (added, removed) in
- has_changes_r diffs false false;;
+ has_changes_r diffs false false
(* get the Myers diff of 2 lists of strings *)
let diff_strs old_strs new_strs =
let diffs = List.rev (StringDiff.diff old_strs new_strs) in
- shorten_diff_span `Removed (shorten_diff_span `Added diffs);;
+ shorten_diff_span `Removed (shorten_diff_span `Added diffs)
(* Default string tokenizer. Makes each character a separate strin.
Whitespace is not ignored. Doesn't handle UTF-8 differences well. *)
@@ -139,7 +139,7 @@ let def_tokenize_string s =
let diff_str ?(tokenize_string=def_tokenize_string) old_str new_str =
let old_toks = Array.of_list (tokenize_string old_str)
and new_toks = Array.of_list (tokenize_string new_str) in
- diff_strs old_toks new_toks;;
+ diff_strs old_toks new_toks
let get_dinfo = function
| `Common (_, _, s) -> (`Common, s)
@@ -281,14 +281,14 @@ let add_diff_tags which pp diffs =
skip ();
if !diffs <> [] then
raise (Diff_Failure "left-over diff info at end of Pp.t, should be impossible");
- if has_added || has_removed then wrap_in_bg diff_tag rv else rv;;
+ if has_added || has_removed then wrap_in_bg diff_tag rv else rv
let diff_pp ?(tokenize_string=def_tokenize_string) o_pp n_pp =
let open Pp in
let o_str = string_of_ppcmds o_pp in
let n_str = string_of_ppcmds n_pp in
let diffs = diff_str ~tokenize_string o_str n_str in
- (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs);;
+ (add_diff_tags `Removed o_pp diffs, add_diff_tags `Added n_pp diffs)
let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false) o_pp n_pp =
let open Pp in
@@ -300,4 +300,4 @@ let diff_pp_combined ?(tokenize_string=def_tokenize_string) ?(show_removed=false
if show_removed && has_removed then
let removed = add_diff_tags `Removed o_pp diffs in
(v 0 (removed ++ cut() ++ added))
- else added;;
+ else added
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 43f70dfecc..dd372ecb0f 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -252,6 +252,9 @@ let pp_of_type env sigma ty =
let pr_leconstr_env ?lax ?inctx ?scope env sigma t =
Ppconstr.pr_lconstr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t)
+let pr_econstr_env ?lax ?inctx ?scope env sigma t =
+ Ppconstr.pr_constr_expr env sigma (Constrextern.extern_constr ?lax ?inctx ?scope env sigma t)
+
let pr_lconstr_env ?lax ?inctx ?scope env sigma c =
pr_leconstr_env ?lax ?inctx ?scope env sigma (EConstr.of_constr c)
@@ -660,3 +663,22 @@ let make_goal_map op np =
let ng_to_og = make_goal_map_i op np in
(*db_goal_map op np ng_to_og;*)
ng_to_og
+
+let diff_proofs ~diff_opt ?old proof =
+ let pp_proof p =
+ let sigma, env = Proof.get_proof_context p in
+ let pprf = Proof.partial_proof p in
+ Pp.prlist_with_sep Pp.fnl (pr_econstr_env env sigma) pprf in
+ match diff_opt with
+ | DiffOff -> pp_proof proof
+ | _ -> begin
+ try
+ let n_pp = pp_proof proof in
+ let o_pp = match old with
+ | None -> Pp.mt()
+ | Some old -> pp_proof old in
+ let show_removed = Some (diff_opt = DiffRemoved) in
+ Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp
+ with
+ | Pp_diff.Diff_Failure msg -> Pp.str msg
+ end
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index ea64439456..6bdd7004fb 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -25,6 +25,10 @@ val write_color_enabled : bool -> unit
(** true indicates that color output is enabled *)
val color_enabled : unit -> bool
+type diffOpt = DiffOff | DiffOn | DiffRemoved
+
+val string_to_diffs : string -> diffOpt
+
open Evd
open Environ
open Constr
@@ -84,3 +88,5 @@ type hyp_info = {
}
val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list
+
+val diff_proofs : diff_opt:diffOpt -> ?old:Proof.t -> Proof.t -> Pp.t
diff --git a/test-suite/ide/proof-diffs.fake b/test-suite/ide/proof-diffs.fake
new file mode 100644
index 0000000000..594ebced23
--- /dev/null
+++ b/test-suite/ide/proof-diffs.fake
@@ -0,0 +1,10 @@
+ADD { Goal True /\ False /\ True = False. }
+ADD { split. }
+GOALS
+ADD here { split. }
+GOALS
+PDIFF here
+ADD there { auto. }
+GOALS
+PDIFF there
+ADD { Admitted. }
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index eb386ea3e8..d587e57fd8 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -508,6 +508,7 @@ let parse_args ~help ~init arglist : t * string list =
|"-color" -> set_color oval (next ())
|"-config"|"--config" -> set_query oval PrintConfig
|"-debug" -> Coqinit.set_debug (); oval
+ |"-xml-debug" -> Flags.xml_debug := true; Coqinit.set_debug (); oval
|"-diffs" ->
add_set_option oval Proof_diffs.opt_name @@ Stm.OptionSet (Some (next ()))
|"-stm-debug" -> Stm.stm_debug := true; oval
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 79de3c86b6..a94c1aea66 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -371,41 +371,13 @@ let exit_on_error =
declare_bool_option_and_ref ~depr:false ~key:["Coqtop";"Exit";"On";"Error"]
~value:false
-(* XXX: This is duplicated with Vernacentries.show_proof , at some
- point we should consolidate the code *)
-let show_proof_diff_to_pp pstate =
- let p = Option.get pstate in
- let sigma, env = Proof.get_proof_context p in
- let pprf = Proof.partial_proof p in
- Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
-
-let show_proof_diff_cmd ~state removed =
+let show_proof_diff_cmd ~state diff_opt =
let open Vernac.State in
- try
- let n_pp = show_proof_diff_to_pp state.proof in
- if true (*Proof_diffs.show_diffs ()*) then
- let doc = state.doc in
- let oproof = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
- try
- let o_pp = show_proof_diff_to_pp oproof in
- let tokenize_string = Proof_diffs.tokenize_string in
- let show_removed = Some removed in
- Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp
- with
- | Proof.NoSuchGoal _
- | Option.IsNone -> n_pp
- | Pp_diff.Diff_Failure msg -> begin
- (* todo: print the unparsable string (if we know it) *)
- Feedback.msg_warning Pp.(str ("Diff failure: " ^ msg) ++ cut()
- ++ str "Showing results without diff highlighting" );
- n_pp
- end
- else
- n_pp
- with
- | Proof.NoSuchGoal _
- | Option.IsNone ->
- CErrors.user_err (str "No goals to show.")
+ match state.proof with
+ | None -> CErrors.user_err (str "No proofs to diff.")
+ | Some proof ->
+ let old = Stm.get_prev_proof ~doc:state.doc state.sid in
+ Proof_diffs.diff_proofs ~diff_opt ?old proof
let process_toplevel_command ~state stm =
let open Vernac.State in
@@ -444,12 +416,12 @@ let process_toplevel_command ~state stm =
Feedback.msg_notice (v 0 (goal ++ evars));
state
- | VernacShowProofDiffs removed ->
+ | VernacShowProofDiffs diff_opt ->
(* We print nothing if there are no goals left *)
if not (Proof_diffs.color_enabled ()) then
CErrors.user_err Pp.(str "Show Proof Diffs requires setting the \"-color\" command line argument to \"on\" or \"auto\".")
else
- let out = show_proof_diff_cmd ~state removed in
+ let out = show_proof_diff_cmd ~state diff_opt in
Feedback.msg_notice out;
state
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index 1902103a3e..ef79f4562e 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -20,7 +20,7 @@ type vernac_toplevel =
| VernacQuit
| VernacControl of vernac_control
| VernacShowGoal of { gid : int; sid: int }
- | VernacShowProofDiffs of bool
+ | VernacShowProofDiffs of Proof_diffs.diffOpt
module Toplevel_ : sig
val vernac_toplevel : vernac_toplevel option Entry.t
@@ -52,7 +52,8 @@ GRAMMAR EXTEND Gram
| test_show_goal; IDENT "Show"; IDENT "Goal"; gid = natural; IDENT "at"; sid = natural; "." ->
{ Some (VernacShowGoal {gid; sid}) }
| IDENT "Show"; IDENT "Proof"; IDENT "Diffs"; removed = OPT [ IDENT "removed" -> { () } ]; "." ->
- { Some (VernacShowProofDiffs (removed <> None)) }
+ { Some (VernacShowProofDiffs
+ (if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) }
| cmd = Pvernac.Vernac_.main_entry ->
{ match cmd with
| None -> None
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 732ad05b26..6fb5f821ee 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -72,6 +72,7 @@ let print_usage_common co command =
\n -init-file f set the rcfile to f\
\n -bt print backtraces (requires configure debug flag)\
\n -debug debug mode (implies -bt)\
+\n -xml-debug debug mode and print XML messages to/from coqide\
\n -diffs (on|off|removed) highlight differences between proof steps\
\n -stm-debug STM debug mode (will trace every transaction)\
\n -noglob do not dump globalizations\
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:13:13 +0000