aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst8
-rw-r--r--printing/printer.ml16
-rw-r--r--printing/printer.mli2
-rw-r--r--stm/stm.ml2
-rw-r--r--stm/stm.mli2
-rw-r--r--test-suite/output-coqtop/ShowGoal.out73
-rw-r--r--test-suite/output-coqtop/ShowGoal.v11
-rw-r--r--toplevel/coqloop.ml5
-rw-r--r--toplevel/g_toplevel.mlg21
9 files changed, 139 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 0cff987a27..03b30d5d97 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -600,6 +600,14 @@ Requesting information
its normalized form at the current stage of the proof, useful for
debugging universe inconsistencies.
+ .. cmdv:: Show Goal @num at @num
+ :name: Show Goal
+
+ This command is only available in coqtop. Displays a goal at a
+ proof state using the goal ID number and the proof state ID number.
+ It is primarily for use by tools such as Prooftree that need to fetch
+ goal history in this way. Prooftree is a tool for visualizing a proof
+ as a tree that runs in Proof General.
.. cmd:: Guarded
diff --git a/printing/printer.ml b/printing/printer.ml
index 0bcea3b01c..1f68018678 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -831,6 +831,22 @@ let pr_goal_by_id ~proof id =
pr_selected_subgoal (pr_id id) sigma g)
with Not_found -> user_err Pp.(str "No such goal.")
+(** print a goal identified by the goal id as it appears in -emacs mode.
+ sid should be the Stm state id corresponding to proof. Used to support
+ the Prooftree tool in Proof General. (https://askra.de/software/prooftree/).
+*)
+let pr_goal_emacs ~proof gid sid =
+ match proof with
+ | None -> user_err Pp.(str "No proof for that state.")
+ | Some proof ->
+ let pr gs =
+ v 0 ((str "goal ID " ++ (int gid) ++ str " at state " ++ (int sid)) ++ cut ()
+ ++ pr_goal gs)
+ in
+ try
+ Proof.in_proof proof (fun sigma -> pr {it=(Evar.unsafe_of_int gid);sigma=sigma;})
+ with Not_found -> user_err Pp.(str "No such goal.")
+
(* Printer function for sets of Assumptions.assumptions.
It is used primarily by the Print Assumptions command. *)
diff --git a/printing/printer.mli b/printing/printer.mli
index 4923e9ec0e..a72f319636 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -206,4 +206,4 @@ module ContextObjectMap : CMap.ExtS
val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
-
+val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t
diff --git a/stm/stm.ml b/stm/stm.ml
index 28d5447c44..0216eef75f 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1105,6 +1105,7 @@ module Backtrack : sig
(* Returns the state that the command should backtract to *)
val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t
val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
+ val get_proof : doc:doc -> Stateid.t -> Proof.t option
end = struct (* {{{ *)
@@ -1250,6 +1251,7 @@ end = struct (* {{{ *)
end (* }}} *)
let get_prev_proof = Backtrack.get_prev_proof
+let get_proof = Backtrack.get_proof
let hints = ref Aux_file.empty_aux_file
let set_compilation_hints file =
diff --git a/stm/stm.mli b/stm/stm.mli
index f1bef2dc4d..92a782d965 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -119,6 +119,8 @@ the specified state AND that has differences in the underlying proof (i.e.,
ignoring proofview-only changes). Used to compute proof diffs. *)
val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
+val get_proof : doc:doc -> Stateid.t -> Proof.t option
+
(* [query at ?report_with cmd] Executes [cmd] at a given state [at],
throwing away side effects except messages. Feedback will
be sent with [report_with], which defaults to the dummy state id *)
diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out
new file mode 100644
index 0000000000..2eadd22db8
--- /dev/null
+++ b/test-suite/output-coqtop/ShowGoal.out
@@ -0,0 +1,73 @@
+
+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
+
+x < 1 focused subgoal
+(shelved: 2)
+
+ i : nat
+ ============================
+ i = ?j /\ ?j = ?k /\ i = ?k
+
+x < 2 focused subgoals
+(shelved: 2)
+
+ i : nat
+ ============================
+ i = ?j
+
+subgoal 2 is:
+ ?j = ?k /\ i = ?k
+
+x < 1 focused subgoal
+(shelved: 1)
+
+ i : nat
+ ============================
+ i = ?k /\ i = ?k
+
+x < 2 focused subgoals
+(shelved: 1)
+
+ i : nat
+ ============================
+ i = ?k
+
+subgoal 2 is:
+ i = ?k
+
+x < 1 subgoal
+
+ i : nat
+ ============================
+ i = i
+
+x < goal ID 16 at state 5
+
+ i : nat
+ ============================
+ i = ?j /\ ?j = ?k /\ i = ?k
+
+x < goal ID 16 at state 7
+
+ i : nat
+ ============================
+ i = i /\ i = ?k /\ i = ?k
+
+x < goal ID 16 at state 9
+
+ i : nat
+ ============================
+ i = i /\ i = i /\ i = i
+
+x <
diff --git a/test-suite/output-coqtop/ShowGoal.v b/test-suite/output-coqtop/ShowGoal.v
new file mode 100644
index 0000000000..9545254770
--- /dev/null
+++ b/test-suite/output-coqtop/ShowGoal.v
@@ -0,0 +1,11 @@
+Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k.
+Proof using.
+ eexists.
+ eexists.
+ split.
+ trivial.
+ split.
+ trivial.
+Show Goal 16 at 5.
+Show Goal 16 at 7.
+Show Goal 16 at 9.
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 4077c02604..4bcde566e3 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -403,6 +403,11 @@ let rec vernac_loop ~state =
top_goal_print ~doc:state.doc c state.proof nstate.proof;
vernac_loop ~state:nstate
+ | Some (VernacShowGoal {gid; sid}) ->
+ let proof = Stm.get_proof ~doc:state.doc (Stateid.of_int sid) in
+ Feedback.msg_notice (Printer.pr_goal_emacs ~proof gid sid);
+ vernac_loop ~state
+
| None ->
top_stderr (fnl ()); exit 0
diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg
index cddcd5faa7..fed337ab03 100644
--- a/toplevel/g_toplevel.mlg
+++ b/toplevel/g_toplevel.mlg
@@ -11,6 +11,8 @@
{
open Pcoq
open Pcoq.Prim
+open Tok
+open Util
open Vernacexpr
(* Vernaculars specific to the toplevel *)
@@ -19,6 +21,7 @@ type vernac_toplevel =
| VernacDrop
| VernacQuit
| VernacControl of vernac_control
+ | VernacShowGoal of { gid : int; sid: int }
module Toplevel_ : sig
val vernac_toplevel : vernac_toplevel option Entry.t
@@ -29,6 +32,21 @@ end
open Toplevel_
+let err () = raise Stream.Failure
+
+let test_show_goal =
+ Pcoq.Entry.of_parser "test_show_goal"
+ (fun strm ->
+ match stream_nth 0 strm with
+ | IDENT "Show" ->
+ (match stream_nth 1 strm with
+ | IDENT "Goal" ->
+ (match stream_nth 2 strm with
+ | NUMERAL _ -> ()
+ | _ -> err ())
+ | _ -> err ())
+ | _ -> err ())
+
}
GRAMMAR EXTEND Gram
@@ -38,6 +56,9 @@ GRAMMAR EXTEND Gram
| IDENT "Quit"; "." -> { Some VernacQuit }
| IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." ->
{ Some (VernacBacktrack (n,m,p)) }
+ (* 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}) }
| cmd = Pvernac.Vernac_.main_entry ->
{ match cmd with
| None -> None
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:08:44 +0000