Report the proof state when an error occurs during a proof

When a command fails while a proof is in progress, the error now
carries the proof state, printed after the error message (as the
err_desc of Fatal):

- a tactic failure reports the state the tactic was applied to;
- a subproof-count mismatch reports the state before and after the
  tactic (previously the goals were embedded in the message itself,
  and one of the four cases did not show them at all);
- `end` on an unfinished proof reports the remaining goals
  (previously embedded in the message).

Error messages themselves are unchanged and stay on the first line,
printed in red; the proof state follows uncolored. The LSP server does
not attach the state to tactic failures since editors display the
proof state themselves.

Author: ciaran-matthew-dunne

CHANGES.md

@@ -33,6 +33,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - LSP server: position of the error is removed from diagnostics when the error occurs in the file currently open in the editor.
 - Syntax of search query is modified as follows : `in` is used instead of `|` (filtering). `with` is used instead of `,` (conjunction). `|` is used instead of `;` (disjunction).
 - Type of `#assume` in order to generate a new symbol and use it inside a tactic term.
+- Errors occurring while a proof is in progress now report the proof state: the goals a failing tactic was applied to, the goals before and after the tactic for a subproof-count mismatch, and the remaining goals when a proof is unfinished at `end`. The state is printed after the error message, which stays unchanged. The LSP server does not attach the proof state to tactic failures since editors display it themselves.
 
 ### Fixed
 

src/handle/command.ml

@@ -569,7 +569,9 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
         | P_proof_end ->
             (* Check that the proof is indeed finished. *)
             if not (finished ps) then
-              fatal pe.pos "The proof is not finished:@.%a" goals ps;
+              fatal pe.pos
+                ~err_desc:(Format.asprintf "Proof state:@.%a@." goals ps)
+                "The proof is not finished.";
             (* Keep the definition only if the symbol is not opaque. *)
             let d =
               if opaq then None else

src/handle/proof.ml

@@ -27,6 +27,31 @@ let goals : proof_state pp = fun ppf ps ->
       let goal ppf i g = out ppf "\n%d. %a" (i+1) Goal.pp_no_hyp g in
       List.iteri (goal ppf) gs
 
+(** [state_on_error] controls whether the failure of a tactic attaches the
+    current proof state to the error, as the [err_desc] argument of the
+    [Fatal] exception, printed after the error message. It is enabled by
+    default, and disabled by the LSP server, which has its own means of
+    displaying the proof state. Errors that always reported the proof state
+    (subproof-count mismatches, unfinished proofs) keep doing so regardless
+    of this setting. *)
+let state_on_error : bool Stdlib.ref = Stdlib.ref true
+
+(** [error_state ?after ps] renders, for attachment to an error report, the
+    proof state [ps] a failing tactic was applied to, followed, when the
+    failure was only detected after the tactic was applied (a subproof-count
+    mismatch), by the proof state [after] its application. *)
+let error_state : ?after:proof_state -> proof_state -> string =
+  fun ?after before ->
+  match after with
+  | None ->
+      Format.asprintf "Proof state before tactic application:@.%a@."
+        goals before
+  | Some after ->
+      Format.asprintf
+        "Proof state before tactic application:@.%a@.\
+         Proof state after tactic application:@.%a@."
+        goals before goals after
+
 (** [remove_solved_goals ps] removes from the proof state [ps] the typing
    goals that are solved. *)
 let remove_solved_goals : proof_state -> proof_state = fun ps ->

src/handle/tactic.ml

@@ -811,30 +811,53 @@ let handle :
 
 (** [handle sym_pos priv r tac n] applies the tactic [tac] from the previous
    tactic output [r] and checks that the number of goals of the new proof
-   state is compatible with the number [n] of subproofs. *)
+   state is compatible with the number [n] of subproofs. When [tac] fails,
+   the proof state it was applied to is attached to the error (see
+   {!val:Proof.state_on_error}). *)
 let handle :
   Sig_state.t -> popt -> bool -> tac_output -> p_tactic -> int -> tac_output =
   fun ss sym_pos priv (ps, _) t nb_subproofs ->
-  let (ps', _) as a = handle ss sym_pos priv ps t in
+  (* Attach the proof state [t] was applied to, to any error escaping its
+     application. Errors raised inside tacticals like [try] or [orelse] are
+     caught below this point, so only failures actually reported to the user
+     are concerned. *)
+  let (ps', _) as a =
+    try handle ss sym_pos priv ps t
+    with Fatal(p, msg, desc)
+      when Stdlib.(!state_on_error) && ps.proof_goals <> [] ->
+        let state = error_state ps in
+        let desc = if desc = "" then state else desc ^ "\n" ^ state in
+        raise (Fatal(p, msg, desc))
+  in
   let nb_goals_before = List.length ps.proof_goals in
   let nb_goals_after = List.length ps'.proof_goals in
   let nb_newgoals = nb_goals_after - nb_goals_before in
+  (* [t] ran, but the number of subproofs given does not match the number of
+     subgoals it produced: report the proof state before and after its
+     application. *)
+  let mismatch : string -> 'a = fun reason ->
+    fatal t.pos ~err_desc:(error_state ~after:ps' ps) "%s" reason in
   if nb_newgoals <= 0 then
     if nb_subproofs = 0 then a
-    else fatal t.pos "A subproof is given but there is no subgoal."
+    else mismatch "A subproof is given but there is no subgoal."
   else if is_destructive t then
-    match nb_newgoals + 1 - nb_subproofs with
+    (match nb_newgoals + 1 - nb_subproofs with
     | 0 -> a
     | n when n > 0 ->
-      fatal t.pos "Missing subproofs (%d subproofs for %d subgoals):@.%a"
-        nb_subproofs (nb_newgoals + 1) goals ps'
+      mismatch (Printf.sprintf
+        "Missing subproofs (%d subproofs for %d subgoals)."
+        nb_subproofs (nb_newgoals + 1))
     | _ ->
-      fatal t.pos "Too many subproofs (%d subproofs for %d subgoals):@.%a"
-        nb_subproofs (nb_newgoals + 1) goals ps'
+      mismatch (Printf.sprintf
+        "Too many subproofs (%d subproofs for %d subgoals)."
+        nb_subproofs (nb_newgoals + 1)))
   else match nb_newgoals - nb_subproofs with
     | 0 -> a
     | n when n > 0 ->
-      fatal t.pos "Missing subproofs (%d subproofs for %d subgoals):@.%a"
-        nb_subproofs nb_newgoals goals ps'
-    | _ -> fatal t.pos "Too many subproofs (%d subproofs for %d subgoals)."
-             nb_subproofs nb_newgoals
+      mismatch (Printf.sprintf
+        "Missing subproofs (%d subproofs for %d subgoals)."
+        nb_subproofs nb_newgoals)
+    | _ ->
+      mismatch (Printf.sprintf
+        "Too many subproofs (%d subproofs for %d subgoals)."
+        nb_subproofs nb_newgoals)

src/lsp/dune

@@ -2,4 +2,4 @@
  (name lsp)
  (public_name lambdapi.lsp)
  (modules lsp_base lsp_io lp_doc lp_lsp)
- (libraries yojson lambdapi.pure))
+ (libraries yojson lambdapi.handle lambdapi.pure))

src/lsp/lp_lsp.ml

@@ -460,6 +460,9 @@ let main std log_file =
   let lp_fmt = F.formatter_of_buffer Lp_doc.lp_logger in
   Console.out_fmt := lp_fmt;
   Error.err_fmt := lp_fmt;
+  (* Editors display the proof state themselves, so do not attach it to
+     tactic failures. *)
+  Handle.Proof.state_on_error := false;
   (* Console.verbose := 4; *)
 
   let rec loop () =

tests/KO/proof_state_fail.lp

@@ -0,0 +1,13 @@
+// A tactic failing mid-proof: the error must carry the proof state
+// (hypotheses, separator, goals) as its description (see proof_state.ml).
+constant symbol Prop : TYPE;
+injective symbol π : Prop → TYPE;
+constant symbol A : Prop;
+constant symbol B : Prop;
+symbol imp : Prop → Prop → Prop;
+rule π (imp $a $b) ↪ π $a → π $b;
+opaque symbol demo : π (imp A (imp B A)) ≔
+begin
+  assume a b;
+  fail
+end;

tests/KO/proof_state_mismatch.lp

@@ -0,0 +1,12 @@
+// A subproof-count mismatch is only detected after the tactic ran: the error
+// must carry the proof state before AND after it (see proof_state.ml).
+constant symbol Prop : TYPE;
+builtin "Prop" ≔ Prop;
+injective symbol π : Prop → TYPE;
+builtin "P" ≔ π;
+inductive N : TYPE ≔ | z : N | succ : N → N;
+symbol Q : N → Prop;
+opaque symbol demo : Π n, π (Q n) ≔
+begin
+  induction
+end;

tests/KO/proof_state_unfinished.lp

@@ -0,0 +1,11 @@
+// Reaching `end` with goals remaining: the error must carry the remaining
+// proof state as its description (see proof_state.ml).
+constant symbol Prop : TYPE;
+injective symbol π : Prop → TYPE;
+constant symbol A : Prop;
+symbol imp : Prop → Prop → Prop;
+rule π (imp $a $b) ↪ π $a → π $b;
+opaque symbol demo : π (imp A A) ≔
+begin
+  assume a
+end;

tests/dune

@@ -1,5 +1,5 @@
 (tests
- (names ok_ko rewriting purity kernel)
+ (names ok_ko rewriting purity kernel proof_state)
  (deps
   (glob_files OK/*.lp)
   (glob_files OK/*.dk)