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. --- vernac/obligations.ml | 97 +++++++++++++++++++++++++++---------------------- vernac/vernacentries.ml | 3 +- 2 files changed, 54 insertions(+), 46 deletions(-) (limited to 'vernac') diff --git a/vernac/obligations.ml b/vernac/obligations.ml index c2805674e4..b1deee7798 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -826,18 +826,34 @@ let rec string_of_list sep f = function | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl (* Solve an obligation using tactics, return the corresponding proof term *) +let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~category:"tactics" (fun err -> + Pp.seq [str "Solve Obligations tactic returned error: "; err; fnl (); + str "This will become an error in the future"]) -let solve_by_tac name evi t poly ctx = +let solve_by_tac ?loc name evi t poly ctx = let id = name in (* spiwack: the status is dropped. *) - let (entry,_,ctx') = Pfedit.build_constant_by_tactic - id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl (Tacticals.New.tclCOMPLETE t) in - let env = Global.env () in - let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in - let body, () = Future.force entry.const_entry_body in - let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in - Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); - (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' + try + let (entry,_,ctx') = + Pfedit.build_constant_by_tactic + id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in + let env = Global.env () in + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let body, () = Future.force entry.const_entry_body in + let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in + Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); + Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx') + with + | Refiner.FailError (_, s) as exn -> + let _ = CErrors.push exn in + user_err ?loc ~hdr:"solve_obligation" (Lazy.force s) + (* If the proof is open we absorb the error and leave the obligation open *) + | Proof.OpenProof _ -> + None + | e when CErrors.noncritical e -> + let err = CErrors.print e in + warn_solve_errored ?loc err; + None let obligation_terminator name num guard hook auto pf = let open Proof_global in @@ -987,41 +1003,34 @@ and solve_obligation_by_tac prg obls i tac = match obl.obl_body with | Some _ -> None | None -> - try - if List.is_empty (deps_remaining obls obl.obl_deps) then - let obl = subst_deps_obl obls obl in - let tac = - match tac with - | Some t -> t - | None -> - match obl.obl_tac with - | Some t -> t - | None -> !default_tactic - in - let evd = Evd.from_ctx prg.prg_ctx in - let evd = Evd.update_sigma_env evd (Global.env ()) in - let t, ty, ctx = - solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 prg.prg_kind) (Evd.evar_universe_context evd) - in - let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in - let prg = {prg with prg_ctx = ctx} in - let def, obl' = declare_obligation prg obl t ty uctx in - obls.(i) <- obl'; - if def && not (pi2 prg.prg_kind) then ( - (* Declare the term constraints with the first obligation only *) - let evd = Evd.from_env (Global.env ()) in - let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in - let ctx' = Evd.evar_universe_context evd in - Some {prg with prg_ctx = ctx'}) - else Some prg - else None - with e when CErrors.noncritical e -> - let (e, _) = CErrors.push e in - match e with - | Refiner.FailError (_, s) -> - user_err ?loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s) - | e -> None (* FIXME really ? *) + if List.is_empty (deps_remaining obls obl.obl_deps) then + let obl = subst_deps_obl obls obl in + let tac = + match tac with + | Some t -> t + | None -> + match obl.obl_tac with + | Some t -> t + | None -> !default_tactic + in + let evd = Evd.from_ctx prg.prg_ctx in + let evd = Evd.update_sigma_env evd (Global.env ()) in + match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac + (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with + | None -> None + | Some (t, ty, ctx) -> + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in + let prg = {prg with prg_ctx = ctx} in + let def, obl' = declare_obligation prg obl t ty uctx in + obls.(i) <- obl'; + if def && not (pi2 prg.prg_kind) then ( + (* Declare the term constraints with the first obligation only *) + let evd = Evd.from_env (Global.env ()) in + let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in + let ctx' = Evd.evar_universe_context evd in + Some {prg with prg_ctx = ctx'}) + else Some prg + else None and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1fab35b650..7b81fbf81b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -457,8 +457,7 @@ let start_proof_and_print k l hook = Evarutil.is_ground_term sigma concl) then raise Exit; let c, _, ctx = - Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) - concl (Tacticals.New.tclCOMPLETE tac) + Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) concl tac in Evd.set_universe_context sigma ctx, EConstr.of_constr c with Logic_monad.TacticFailure e when Logic.catchable_exception e -> user_err Pp.(str "The statement obligations could not be resolved \ -- cgit v1.2.3