Report the proof state when an error occurs during a proof (#1453)

Attach the proof state to errors raised while a proof is in progress,
using the err_desc field of Fatal: the goals a failing tactic was
applied to, the goals before and after the tactic for a subproof-count
mismatch, and the remaining goals for an unfinished proof at `end`.
The error message itself is unchanged; the state is printed after it,
uncolored. The LSP server disables this for 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

@@ -567,7 +567,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

@@ -818,30 +818,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)