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/proof.ml | 47 ++++++++++++++++++++++++++++++-----------------
 1 file changed, 30 insertions(+), 17 deletions(-)

(limited to 'proofs/proof.ml')

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 =
-- 
cgit v1.2.3