From 758041989f29ed960eba8bf7fe0d232d3937db60 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 13 Nov 2018 02:06:12 +0100
Subject: [proof] Provide better control of "open proofs" exceptions.

This is inspired and an alternative to #8981. We consolidate the "open
proof" exception, allowing clients to explicitly capture it and
removing some ugly duplicated code in the way.

The `Solve Obligation tac` semantics are then tweaked as to removed
the wide-scope "catch-all" and indeed will now relay errors in `tac`
as it will only absorb tactics that don't error but fail to close the
goal such as `auto`. For the rest of the cases, we introduce a
warning, and may move to a full error in later releases.

We also remove an unnecessary `tclCOMPLETE` call to code that will
actually call `close_proof`. In this case, it is better to delegate
error management to the core function.

Some error messages have changed [as we consolidate two error paths]
so this PR may require adjustment in that area.
---
 proofs/logic.ml        |  2 ++
 proofs/proof.ml        | 47 ++++++++++++++++++++++++++++++-----------------
 proofs/proof.mli       | 14 +++++++++-----
 proofs/proof_global.ml | 16 +---------------
 proofs/proofs.mllib    |  2 +-
 5 files changed, 43 insertions(+), 38 deletions(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 4d5711c195..f9e2edd888 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -62,6 +62,8 @@ let is_unification_error = function
 
 let catchable_exception = function
   | CErrors.UserError _ | TypeError _
+  | Proof.OpenProof _
+  (* abstract will call close_proof inside a tactic *)
   | Notation.NumeralNotationError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8220949856..76a9a9f4c8 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -335,28 +335,42 @@ let dependent_start goals =
   let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
   _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
 
-exception UnfinishedProof
-exception HasShelvedGoals
-exception HasGivenUpGoals
-exception HasUnresolvedEvar
+type open_error_reason =
+  | UnfinishedProof
+  | HasShelvedGoals
+  | HasGivenUpGoals
+  | HasUnresolvedEvar
+
+let print_open_error_reason er = let open Pp in match er with
+  | UnfinishedProof ->
+    str "Attempt to save an incomplete proof"
+  | HasShelvedGoals ->
+    str "Attempt to save a proof with shelved goals"
+  | HasGivenUpGoals ->
+    strbrk "Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed."
+  | HasUnresolvedEvar ->
+    strbrk "Attempt to save a proof with existential variables still non-instantiated"
+
+exception OpenProof of Names.Id.t option * open_error_reason
+
 let _ = CErrors.register_handler begin function
-  | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.")
-  | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.")
-  | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.")
-  | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.")
-  | _ -> raise CErrors.Unhandled
-end
+    | OpenProof (pid, reason) ->
+      let open Pp in
+      Option.cata (fun pid ->
+          str " (in proof " ++ Names.Id.print pid ++ str "): ") (mt()) pid ++ print_open_error_reason reason
+    | _ -> raise CErrors.Unhandled
+  end
 
-let return p =
+let return ?pid (p : t) =
   if not (is_done p) then
-    raise UnfinishedProof
+    raise (OpenProof(pid, UnfinishedProof))
   else if has_shelved_goals p then
-    raise HasShelvedGoals
+    raise (OpenProof(pid, HasShelvedGoals))
   else if has_given_up_goals p then
-    raise HasGivenUpGoals
+    raise (OpenProof(pid, HasGivenUpGoals))
   else if has_unresolved_evar p then
     (* spiwack: for compatibility with <= 8.3 proof engine *)
-    raise HasUnresolvedEvar
+    raise (OpenProof(pid, HasUnresolvedEvar))
   else
     let p = unfocus end_of_stack_kind p () in
     Proofview.return p.proofview
@@ -449,11 +463,10 @@ module V82 = struct
 
   let grab_evars p =
     if not (is_done p) then
-      raise UnfinishedProof
+      raise (OpenProof(None, UnfinishedProof))
     else
       { p with proofview = Proofview.V82.grab p.proofview }
 
-
   (* Main component of vernac command Existential *)
   let instantiate_evar n com pr =
     let tac =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 8cf543557b..aaabea3454 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -89,11 +89,15 @@ val compact : t -> t
     Raises [HasShelvedGoals] if some goals are left on the shelf.
     Raises [HasGivenUpGoals] if some goals have been given up.
     Raises [HasUnresolvedEvar] if some evars have been left undefined. *)
-exception UnfinishedProof
-exception HasShelvedGoals
-exception HasGivenUpGoals
-exception HasUnresolvedEvar
-val return : t -> Evd.evar_map
+type open_error_reason =
+  | UnfinishedProof
+  | HasShelvedGoals
+  | HasGivenUpGoals
+  | HasUnresolvedEvar
+
+exception OpenProof of Names.Id.t option * open_error_reason
+
+val return : ?pid:Names.Id.t -> t -> Evd.evar_map
 
 (*** Focusing actions ***)
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 25cf789193..cb4b5759dc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -176,7 +176,6 @@ let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ())
 
 let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact)
 
-
 (* Sets the tactic to be used when a tactic line is closed with [...] *)
 let set_endline_tactic tac =
   match !pstates with
@@ -416,20 +415,7 @@ let return_proof ?(allow_partial=false) () =
     proofs, Evd.evar_universe_context evd
  end else
   let initial_goals = Proof.initial_goals proof in
-  let evd =
-    let error s =
-      let prf = str " (in proof " ++ Id.print pid ++ str ")" in
-      raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf))
-    in
-    try Proof.return proof with
-    | Proof.UnfinishedProof ->
-        error(str"Attempt to save an incomplete proof")
-    | Proof.HasShelvedGoals ->
-        error(str"Attempt to save a proof with shelved goals")
-    | Proof.HasGivenUpGoals ->
-        error(strbrk"Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed.")
-    | Proof.HasUnresolvedEvar->
-        error(strbrk"Attempt to save a proof with existential variables still non-instantiated") in
+  let evd = Proof.return ~pid proof in
   let eff = Evd.eval_side_effects evd in
   let evd = Evd.minimize_universes evd in
   (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 197f71ca91..f9bb2c3d60 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -2,9 +2,9 @@ Miscprint
 Goal
 Evar_refiner
 Proof_type
-Logic
 Refine
 Proof
+Logic
 Goal_select
 Proof_bullet
 Proof_global
-- 
cgit v1.2.3