From 5ec7eca640a6ee495eb2c0fb8d8a4076256ff96d Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 6 Jul 2019 19:25:39 -0700 Subject: Show diffs in "Show Proof." Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output --- .../10494-diffs-in-show-proof.rst | 6 +++ doc/sphinx/proof-engine/proof-handling.rst | 15 ++++++-- printing/proof_diffs.mli | 3 ++ tactics/pfedit.ml | 7 +++- tactics/pfedit.mli | 4 ++ test-suite/output-coqtop/ShowProofDiffs.out | 42 +++++++++++++++++++++ test-suite/output-coqtop/ShowProofDiffs.v | 6 +++ toplevel/coqloop.ml | 44 ++++++++++++++++++++++ toplevel/g_toplevel.mlg | 3 ++ 9 files changed, 125 insertions(+), 5 deletions(-) create mode 100644 doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst create mode 100644 test-suite/output-coqtop/ShowProofDiffs.out create mode 100644 test-suite/output-coqtop/ShowProofDiffs.v diff --git a/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst new file mode 100644 index 0000000000..c1df728c5c --- /dev/null +++ b/doc/changelog/07-commands-and-options/10494-diffs-in-show-proof.rst @@ -0,0 +1,6 @@ +- Optionally highlight the differences between successive proof steps in the + :cmd:`Show Proof` command. Experimental; only available in coqtop + and Proof General for now, may be supported in other IDEs + in the future. + (`#10494 `_, + by Jim Fehrle). diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 57a54bc0ad..00f8269dc3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -535,7 +535,7 @@ Requesting information eexists ?[n]. Show n. - .. cmdv:: Show Proof + .. cmdv:: Show Proof {? Diffs {? removed } } :name: Show Proof Displays the proof term generated by the tactics @@ -544,6 +544,12 @@ 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 + 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`. + .. cmdv:: Show Conjectures :name: Show Conjectures @@ -624,8 +630,11 @@ Showing differences between proof steps --------------------------------------- -Coq can automatically highlight the differences between successive proof steps and between -values in some error messages. +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. + 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 diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli index f6fca91eea..a806ab7123 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -16,6 +16,9 @@ val write_diffs_option : string -> unit (** Returns true if the diffs option is "on" or "removed" *) val show_diffs : unit -> bool +(** Returns true if the diffs option is "removed" *) +val show_removed : unit -> bool + (** controls whether color output is enabled *) val write_color_enabled : bool -> unit diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index 413c6540a3..47bb0a6af0 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -55,8 +55,7 @@ let get_current_goal_context pf = let env = Global.env () in Evd.from_env env, env -let get_current_context pf = - let p = Proof_global.get_proof pf in +let get_proof_context p = try get_goal_context_gen p 1 with | NoSuchGoal -> @@ -64,6 +63,10 @@ let get_current_context pf = let { Proof.sigma } = Proof.data p in sigma, Global.env () +let get_current_context pf = + let p = Proof_global.get_proof pf in + get_proof_context p + let solve ?with_end_tac gi info_lvl tac pr = let tac = match with_end_tac with | None -> tac diff --git a/tactics/pfedit.mli b/tactics/pfedit.mli index 30514191fa..11ce50b659 100644 --- a/tactics/pfedit.mli +++ b/tactics/pfedit.mli @@ -27,6 +27,10 @@ val get_goal_context : Proof_global.t -> int -> Evd.evar_map * env (** [get_current_goal_context ()] works as [get_goal_context 1] *) val get_current_goal_context : Proof_global.t -> Evd.evar_map * env +(** [get_proof_context ()] gets the goal context for the first subgoal + of the proof *) +val get_proof_context : Proof.t -> Evd.evar_map * env + (** [get_current_context ()] returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out new file mode 100644 index 0000000000..285a3bcd89 --- /dev/null +++ b/test-suite/output-coqtop/ShowProofDiffs.out @@ -0,0 +1,42 @@ + +Coq < Coq < 1 subgoal + + ============================ + forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k + +x < +x < 1 focused subgoal +(shelved: 1) + i : nat + ============================ + exists k : nat, i = ?j /\ ?j = k /\ i = k + +(fun i : nat => + ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k) ?j ?Goal) + +x < 1 focused subgoal +(shelved: 2) + i : nat + ============================ + i = ?j /\ ?j = ?k /\ i = ?k + +(fun i : nat => + ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k)  + ?j (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k) ?k ?Goal)) + +x < 2 focused subgoals +(shelved: 2) + i : nat + ============================ + i = ?j + +subgoal 2 is: + ?j = ?k /\ i = ?k + +(fun i : nat => + ex_intro (fun j : nat => exists k : nat, i = j /\ j = k /\ i = k)  + ?j + (ex_intro (fun k : nat => i = ?j /\ ?j = k /\ i = k)  + ?k (conj ?Goal ?Goal0))) + +x < diff --git a/test-suite/output-coqtop/ShowProofDiffs.v b/test-suite/output-coqtop/ShowProofDiffs.v new file mode 100644 index 0000000000..4251c52cb4 --- /dev/null +++ b/test-suite/output-coqtop/ShowProofDiffs.v @@ -0,0 +1,6 @@ +(* coq-prog-args: ("-color" "on" "-diffs" "on") *) +Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k. +Proof using. + eexists. Show Proof Diffs. + eexists. Show Proof Diffs. + split. Show Proof Diffs. diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 1f319d2bfd..97f0e57d2e 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -418,6 +418,50 @@ let rec vernac_loop ~state = Feedback.msg_notice (v 0 (goal ++ evars)); vernac_loop ~state + | Some VernacShowProofDiffs removed -> + (* extension of Vernacentries.show_proof *) + let to_pp pstate = + let p = Option.get pstate in + let sigma, env = Pfedit.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 + (* We print nothing if there are no goals left *) + in + + 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 begin + let out = + try + let n_pp = 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 = 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 + | Pfedit.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 + | Pfedit.NoSuchGoal + | Option.IsNone -> + CErrors.user_err (str "No goals to show.") + in + Feedback.msg_notice out; + end; + vernac_loop ~state + | None -> top_stderr (fnl ()); exit 0 diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index e180d9e750..56fda58a25 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -22,6 +22,7 @@ type vernac_toplevel = | VernacQuit | VernacControl of vernac_control | VernacShowGoal of { gid : int; sid: int } + | VernacShowProofDiffs of bool module Toplevel_ : sig val vernac_toplevel : vernac_toplevel option Entry.t @@ -59,6 +60,8 @@ GRAMMAR EXTEND Gram (* show a goal for the specified proof state *) | 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)) } | cmd = Pvernac.Vernac_.main_entry -> { match cmd with | None -> None -- cgit v1.2.3