aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library/states.ml4
-rw-r--r--library/states.mli2
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2388.v10
-rw-r--r--toplevel/cerrors.ml91
-rw-r--r--toplevel/cerrors.mli6
-rw-r--r--toplevel/vernac.ml10
-rw-r--r--toplevel/vernac.mli1
7 files changed, 74 insertions, 50 deletions
diff --git a/library/states.ml b/library/states.ml
index b7c66abf5..4619b3b53 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -28,12 +28,12 @@ let (extern_state,intern_state) =
(* Rollback. *)
-let with_heavy_rollback f x =
+let with_heavy_rollback f h x =
let st = freeze () in
try
f x
with reraise ->
- (unfreeze st; raise reraise)
+ let e = h reraise in (unfreeze st; raise e)
let with_state_protection f x =
let st = freeze () in
diff --git a/library/states.mli b/library/states.mli
index 70d139d36..4f114d576 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -25,7 +25,7 @@ val unfreeze : state -> unit
(** [with_heavy_rollback f x] applies [f] to [x] and restores the
state of the whole system as it was before the evaluation if an exception
is raised. *)
-val with_heavy_rollback : ('a -> 'b) -> 'a -> 'b
+val with_heavy_rollback : ('a -> 'b) -> (exn -> exn) -> 'a -> 'b
(** [with_state_protection f x] applies [f] to [x] and restores the
state of the whole system as it was before the evaluation of f *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v
new file mode 100644
index 000000000..c79267119
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2388.v
@@ -0,0 +1,10 @@
+(* Error message was not printed in the correct environment *)
+
+Fail Parameters (A:Prop) (a:A A).
+
+(* This is a variant (reported as part of bug #2347) *)
+
+Require Import EquivDec.
+Fail Program Instance bool_eq_eqdec : EqDec bool eq :=
+ {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}.
+
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 0d2111f8a..a34afda50 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -26,6 +26,8 @@ let guill s = "\""^s^"\""
let where s =
if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
+exception EvaluatedError of std_ppcmds * exn option
+
(* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
let rec explain_exn_default_aux anomaly_string report_fn = function
@@ -63,6 +65,26 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
| Sys.Break ->
hov 0 (fnl () ++ str "User interrupt.")
+ | Assert_failure (s,b,e) ->
+ hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
+ (if s = "" then mt ()
+ else
+ (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
+ str ", characters " ++ int e ++ str "-" ++
+ int (e+6) ++ str ")")) ++
+ report_fn ())
+ | EvaluatedError (msg,None) ->
+ msg
+ | EvaluatedError (msg,Some reraise) ->
+ msg ++ explain_exn_default_aux anomaly_string report_fn reraise
+ | reraise ->
+ hov 0 (anomaly_string () ++ str "Uncaught exception " ++
+ str (Printexc.to_string reraise) ++ report_fn ())
+
+let wrap_vernac_error strm =
+ EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)
+
+let rec process_vernac_interp_error = function
| Univ.UniverseInconsistency (o,u,v) ->
let msg =
if !Constrextern.print_universes then
@@ -71,59 +93,48 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
++ spc() ++ Univ.pr_uni v ++ str")"
else
mt() in
- hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
+ wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
| TypeError(ctx,te) ->
- hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te)
+ wrap_vernac_error (Himsg.explain_type_error ctx te)
| PretypeError(ctx,te) ->
- hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te)
+ wrap_vernac_error (Himsg.explain_pretype_error ctx te)
| Typeclasses_errors.TypeClassError(env, te) ->
- hov 0 (str "Error:" ++ spc () ++ Himsg.explain_typeclass_error env te)
+ wrap_vernac_error (Himsg.explain_typeclass_error env te)
| InductiveError e ->
- hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
+ wrap_vernac_error (Himsg.explain_inductive_error e)
| RecursionSchemeError e ->
- hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
- | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
- explain_exn_default_aux anomaly_string report_fn exc
- | Proof_type.LtacLocated (s,exc) ->
- hov 0 (Himsg.explain_ltac_call_trace s ++ fnl ()
- ++ explain_exn_default_aux anomaly_string report_fn exc)
+ wrap_vernac_error (Himsg.explain_recursion_scheme_error e)
| Cases.PatternMatchingError (env,e) ->
- hov 0
- (str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e)
+ wrap_vernac_error (Himsg.explain_pattern_matching_error env e)
| Tacred.ReductionTacticError e ->
- hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e)
+ wrap_vernac_error (Himsg.explain_reduction_tactic_error e)
| Logic.RefinerError e ->
- hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e)
+ wrap_vernac_error (Himsg.explain_refiner_error e)
| Nametab.GlobalizationError q ->
- hov 0 (str "Error:" ++ spc () ++
- str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
- spc () ++ str "was not found" ++
- spc () ++ str "in the current" ++ spc () ++ str "environment.")
+ wrap_vernac_error
+ (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
+ spc () ++ str "was not found" ++
+ spc () ++ str "in the current" ++ spc () ++ str "environment.")
| Nametab.GlobalizationConstantError q ->
- hov 0 (str "Error:" ++ spc () ++
- str "No constant of this name:" ++ spc () ++
- Libnames.pr_qualid q ++ str ".")
+ wrap_vernac_error
+ (str "No constant of this name:" ++ spc () ++
+ Libnames.pr_qualid q ++ str ".")
| Refiner.FailError (i,s) ->
- hov 0 (str "Error: Tactic failure" ++
+ EvaluatedError (hov 0 (str "Error: Tactic failure" ++
(if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++
- if i=0 then str "." else str " (level " ++ int i ++ str").")
- | Loc.Exc_located (loc,exc) ->
- hov 0 ((if loc = dummy_loc then (mt ())
- else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
- ++ explain_exn_default_aux anomaly_string report_fn exc)
- | Assert_failure (s,b,e) ->
- hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
- (if s = "" then mt ()
- else
- (str ("(file \"" ^ s ^ "\", line ") ++ int b ++
- str ", characters " ++ int e ++ str "-" ++
- int (e+6) ++ str ")")) ++
- report_fn ())
+ if i=0 then str "." else str " (level " ++ int i ++ str")."),
+ None)
| AlreadyDeclared msg ->
- hov 0 (str "Error: " ++ msg ++ str ".")
- | reraise ->
- hov 0 (anomaly_string () ++ str "Uncaught exception " ++
- str (Printexc.to_string reraise) ++ report_fn ())
+ wrap_vernac_error (msg ++ str ".")
+ | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
+ process_vernac_interp_error exc
+ | Proof_type.LtacLocated (s,exc) ->
+ EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
+ Some (process_vernac_interp_error exc))
+ | Loc.Exc_located (loc,exc) ->
+ Loc.Exc_located (loc,process_vernac_interp_error exc)
+ | exc ->
+ exc
let anomaly_string () = str "Anomaly: "
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 8dc7e7a79..0dae61f4a 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -15,10 +15,14 @@ val print_loc : loc -> std_ppcmds
val explain_exn : exn -> std_ppcmds
-(** Same, but will re-raise all anomalies instead of explaining them *)
+(** Precompute errors raised during vernac interpretation *)
val explain_exn_no_anomaly : exn -> std_ppcmds
+(** Pre-explain a vernac interpretation error *)
+
+val process_vernac_interp_error : exn -> exn
+
(** For debugging purpose (?), the explain function can be twicked *)
val explain_exn_function : (exn -> std_ppcmds) ref
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index f84097a16..aef772676 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -197,7 +197,10 @@ let rec vernac_com interpfun (loc,com) =
with e -> stop(); raise e
end
- | v -> if not !just_parsing then interpfun v
+ | v ->
+ if not !just_parsing then
+ States.with_heavy_rollback interpfun
+ Cerrors.process_vernac_interp_error v
in
try
@@ -236,13 +239,10 @@ and read_vernac_file verbosely s =
* with a new label to make vernac undoing easier. Also freeze state to speed up
* backtracking. *)
let eval_expr last =
- vernac_com (States.with_heavy_rollback Vernacentries.interp) last;
+ vernac_com Vernacentries.interp last;
Lib.add_frozen_state();
Lib.mark_end_of_command()
-let eval_ctrl ast =
- vernac_com Vernacentries.interp (Util.dummy_loc,ast)
-
(* raw_do_vernac : Pcoq.Gram.parsable -> unit
* vernac_step . parse_sentence *)
let raw_do_vernac po = eval_expr (parse_sentence (po,None))
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 767c53063..d89e90d0c 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -22,7 +22,6 @@ exception End_of_input
val just_parsing : bool ref
val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
-val eval_ctrl : Vernacexpr.vernac_expr -> unit
val raw_do_vernac : Pcoq.Gram.parsable -> unit
(** Set XML hooks *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 18:52:21 +0000