aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.common2
-rw-r--r--dev/printers.mllib1
-rw-r--r--dev/top_printers.ml4
-rw-r--r--lib/errors.ml56
-rw-r--r--lib/errors.mli27
-rw-r--r--lib/lib.mllib3
-rw-r--r--parsing/grammar.mllib1
-rw-r--r--parsing/tacextend.ml42
-rw-r--r--parsing/vernacextend.ml42
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/indfun.ml10
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/subtac/g_subtac.ml42
-rw-r--r--plugins/subtac/subtac.ml2
-rw-r--r--plugins/subtac/subtac_obligations.ml2
-rw-r--r--toplevel/autoinstance.ml2
-rw-r--r--toplevel/cerrors.ml11
-rw-r--r--toplevel/cerrors.mli2
-rw-r--r--toplevel/coqtop.ml4
-rw-r--r--toplevel/ide_slave.ml2
-rw-r--r--toplevel/toplevel.ml2
24 files changed, 117 insertions, 36 deletions
diff --git a/Makefile.common b/Makefile.common
index 18f7e8b04..c27dd84ac 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -233,7 +233,7 @@ IDEMOD:=$(shell cat ide/ide.mllib)
COQENVCMO:=$(CONFIG) \
lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
- lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/system.cmo \
+ lib/segmenttree.cmo lib/unicodetable.cmo lib/util.cmo lib/errors.cmo lib/system.cmo \
lib/envars.cmo
COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 65283a843..7b2d08c2a 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -7,6 +7,7 @@ Flags
Segmenttree
Unicodetable
Util
+Errors
Bigint
Hashcons
Dyn
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 681cb0634..547ca0475 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -414,7 +414,7 @@ let _ =
(fun () -> in_current_context constr_display c)
| _ -> failwith "Vernac extension: cannot occur")
with
- e -> Pp.pp (Cerrors.explain_exn e)
+ e -> Pp.pp (Errors.print e)
let _ =
extend_vernac_command_grammar "PrintConstr" None
[[GramTerminal "PrintConstr";
@@ -431,7 +431,7 @@ let _ =
(fun () -> in_current_context print_pure_constr c)
| _ -> failwith "Vernac extension: cannot occur")
with
- e -> Pp.pp (Cerrors.explain_exn e)
+ e -> Pp.pp (Errors.print e)
let _ =
extend_vernac_command_grammar "PrintPureConstr" None
[[GramTerminal "PrintPureConstr";
diff --git a/lib/errors.ml b/lib/errors.ml
new file mode 100644
index 000000000..89e924948
--- /dev/null
+++ b/lib/errors.ml
@@ -0,0 +1,56 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+open Pp
+
+(* spiwack: it might be reasonable to decide and move the declarations
+ of Anomaly and so on to this module so as not to depend on Util. *)
+(* spiwack: This module contains stuff exfiltrated from Cerrors. *)
+
+let handle_stack = ref []
+
+exception Unhandled
+
+let register_handler h = handle_stack := h::!handle_stack
+
+(* spiwack: [anomaly_string] and [report_fn] are copies from Cerrors.
+ Ultimately they should disapear from Cerrors. *)
+let anomaly_string () = str "Anomaly: "
+let report_fn () = (str "." ++ spc () ++ str "Please report.")
+(* [print_unhandled_exception] is the virtual bottom of the stack:
+ the [handle_stack] is treated as it if was always non-empty
+ with [print_unhandled_exception] as its last handler. *)
+let print_unhandled_exception e =
+ hov 0 (anomaly_string () ++ str "Uncaught exception " ++
+ str (Printexc.to_string e) ++ report_fn ())
+
+let rec print_gen s e =
+ match s with
+ | [] -> print_unhandled_exception e
+ | h::s' ->
+ try h e
+ with
+ | Unhandled -> print_gen s' e
+ | e' -> print_gen s' e'
+
+let print e = print_gen !handle_stack e
+
+
+(*** Predefined handlers ***)
+
+let where s =
+ if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
+
+let _ = register_handler begin function
+ | Util.UserError(s,pps) ->
+ hov 0 (str "Error: " ++ where s ++ pps)
+ | Util.Anomaly (s,pps) ->
+ hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
+ | _ -> raise Unhandled
+end
+
diff --git a/lib/errors.mli b/lib/errors.mli
new file mode 100644
index 000000000..120634e60
--- /dev/null
+++ b/lib/errors.mli
@@ -0,0 +1,27 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(** This modules implements basic manipulations of errors for use
+ throughout Coq's code. *)
+
+(** [register_handler h] registers [h] as a handler.
+ When an expression is printed with [print e], it
+ goes through all registered handles (the most
+ recent first) until a handle deals with it.
+
+ Handles signal that they don't deal with some exception
+ by raisine [Unhandled].
+
+ Handles can raise exceptions themselves, in which
+ case, the exception is passed to the handles which
+ were registered before. *)
+exception Unhandled
+
+val register_handler : (exn -> Pp.std_ppcmds) -> unit
+
+val print : exn -> Pp.std_ppcmds
diff --git a/lib/lib.mllib b/lib/lib.mllib
index cfbedcc52..84180fc46 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -5,6 +5,7 @@ Flags
Segmenttree
Unicodetable
Util
+Errors
Bigint
Hashcons
Dyn
@@ -23,4 +24,4 @@ Heap
Option
Dnet
Store
-Unionfind \ No newline at end of file
+Unionfind
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 02e27827b..30376eeda 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -8,6 +8,7 @@ Flags
Segmenttree
Unicodetable
Util
+Errors
Bigint
Dyn
Hashcons
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index ec305ee2e..2fe1fdda7 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -163,7 +163,7 @@ let declare_tactic loc s cl =
(Tacexpr.TacAtom($default_loc$,
Tacexpr.TacExtend($default_loc$,s,[]))))
$atomic_tactics$
- with e -> Pp.pp (Cerrors.explain_exn e);
+ with e -> Pp.pp (Errors.print e);
Egrammar.extend_tactic_grammar $se$ $gl$;
List.iter Pptactic.declare_extra_tactic_pprule $pp$; } >>
])
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index cc3bd07e8..88a750792 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -54,7 +54,7 @@ let declare_command loc s nt cl =
declare_str_items loc
[ <:str_item< do {
try Vernacinterp.vinterp_add $mlexpr_of_string s$ $funcl$
- with e -> Pp.pp (Cerrors.explain_exn e);
+ with e -> Pp.pp (Errors.print e);
Egrammar.extend_vernac_command_grammar $mlexpr_of_string s$ $nt$ $gl$
} >> ]
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 4f32bbd99..21ee32539 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -36,7 +36,7 @@ let do_observe_tac s tac g =
with e ->
let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
msgnl (str "observation "++ s++str " raised exception " ++
- Cerrors.explain_exn e ++ str " on goal " ++ goal );
+ Errors.print e ++ str " on goal " ++ goal );
raise e;;
let observe_tac_stream s tac g =
@@ -608,7 +608,7 @@ let my_orelse tac1 tac2 g =
try
tac1 g
with e ->
-(* observe (str "using snd tac since : " ++ Cerrors.explain_exn e); *)
+(* observe (str "using snd tac since : " ++ Errors.print e); *)
tac2 g
let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id =
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 39f4cf07f..53ddfb967 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -180,12 +180,12 @@ let warning_error names e =
Pp.msg_warning
(str "Cannot define graph(s) for " ++
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
- if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ())
+ if do_observe () then (spc () ++ Errors.print e) else mt ())
| Defining_principle e ->
Pp.msg_warning
(str "Cannot define principle(s) for "++
h 1 (prlist_with_sep (fun _ -> str","++spc ()) Libnames.pr_reference names) ++
- if do_observe () then Cerrors.explain_exn e else mt ())
+ if do_observe () then Errors.print e else mt ())
| _ -> raise e
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 394417abb..6d4e8929a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1404,7 +1404,7 @@ let do_build_inductive
str "while trying to define"++ spc () ++
Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
++ fnl () ++
- Cerrors.explain_exn e
+ Errors.print e
in
observe msg;
raise e
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index dd48765fb..d98960a48 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -254,14 +254,14 @@ let derive_inversion fix_names =
with e ->
msg_warning
(str "Cannot built inversion information" ++
- if do_observe () then Cerrors.explain_exn e else mt ())
+ if do_observe () then Errors.print e else mt ())
with _ -> ()
let warning_error names e =
let e_explain e =
match e with
- | ToShow e -> spc () ++ Cerrors.explain_exn e
- | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+ | ToShow e -> spc () ++ Errors.print e
+ | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
in
match e with
| Building_graph e ->
@@ -279,8 +279,8 @@ let warning_error names e =
let error_error names e =
let e_explain e =
match e with
- | ToShow e -> spc () ++ Cerrors.explain_exn e
- | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt ()
+ | ToShow e -> spc () ++ Errors.print e
+ | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
in
match e with
| Building_graph e ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 426b496dd..1b7a19029 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -64,7 +64,7 @@ let do_observe_tac s tac g =
let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
with e ->
msgnl (str "observation "++ s++str " raised exception " ++
- Cerrors.explain_exn e ++ str " on goal " ++ goal );
+ Errors.print e ++ str " on goal " ++ goal );
raise e;;
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 11fbc01ba..5b689625b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -75,7 +75,7 @@ let rec print_debug_queue b e =
begin
let lmsg,goal = Stack.pop debug_queue in
if b then
- msgnl (lmsg ++ (str " raised exception " ++ Cerrors.explain_exn e) ++ str " on goal " ++ goal)
+ msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
else
begin
msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal);
@@ -1433,7 +1433,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
with e ->
begin
if Tacinterp.get_debug () <> Tactic_debug.DebugOff
- then pperrnl (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e)
+ then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
else anomaly "Cannot create equation Lemma"
;
(* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index c42f13b04..ca1240e5f 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -90,7 +90,7 @@ VERNAC COMMAND EXTEND Subtac
let try_catch_exn f e =
try f e
- with exn -> errorlabstrm "Program" (Cerrors.explain_exn exn)
+ with exn -> errorlabstrm "Program" (Errors.print exn)
let subtac_obligation e = try_catch_exn Subtac_obligations.subtac_obligation e
let next_obligation e = try_catch_exn Subtac_obligations.next_obligation e
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index fbdaa8d3b..710149ae4 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -224,5 +224,5 @@ let subtac (loc, command) =
Loc.Exc_located (loc, e') as e) -> raise e
| e ->
- (* msg_warning (str "Uncaught exception: " ++ Cerrors.explain_exn e); *)
+ (* msg_warning (str "Uncaught exception: " ++ Errors.print e); *)
raise e
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 76cc7644d..5c2f24a67 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -482,7 +482,7 @@ let rec solve_obligation prg num tac =
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
let res = try update_obls prg obls (pred rem)
- with e -> pperror (Cerrors.explain_exn e)
+ with e -> pperror (Errors.print e)
in
match res with
| Remain n when n > 0 ->
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index af1330a42..d6e88ed2c 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -202,7 +202,7 @@ let declare_class_instance gr ctx params =
(ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst));
new_instance_message ident typ def
- with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Cerrors.explain_exn e)
+ with e -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str" "++Errors.print e)
let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t;
match kind_of_term t with
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 737abb3f4..831e27bed 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -23,8 +23,6 @@ let print_loc loc =
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
@@ -40,16 +38,12 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
| Lexer.Error.E err -> hov 0 (str (Lexer.Error.to_string err))
| Sys_error msg ->
hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
- | UserError(s,pps) ->
- hov 0 (str "Error: " ++ where s ++ pps)
| Out_of_memory ->
hov 0 (str "Out of memory.")
| Stack_overflow ->
hov 0 (str "Stack overflow.")
| Timeout ->
hov 0 (str "Timeout!")
- | Anomaly (s,pps) ->
- hov 0 (anomaly_string () ++ where s ++ pps ++ report_fn ())
| AnomalyOnError (s,exc) ->
hov 0 (anomaly_string () ++ str s ++ str ". Received exception is:" ++
fnl() ++ explain_exn_default_aux anomaly_string report_fn exc)
@@ -81,9 +75,7 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
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 ())
+ | _ -> raise Errors.Unhandled
let wrap_vernac_error strm =
EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)
@@ -165,6 +157,7 @@ let _ = Tactic_debug.explain_logic_error_no_anomaly :=
let explain_exn_function = ref explain_exn_default
let explain_exn e = !explain_exn_function e
+let _ = Errors.register_handler explain_exn
let explain_exn_no_anomaly e =
explain_exn_default_aux (fun () -> raise e) mt e
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 0dae61f4a..2670160ab 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -13,7 +13,9 @@ open Util
val print_loc : loc -> std_ppcmds
+(*
val explain_exn : exn -> std_ppcmds
+*)
(** Precompute errors raised during vernac interpretation *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index e0f21aab8..c0f689467 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -306,9 +306,9 @@ let parse_args arglist =
try
Stream.empty s; exit 1
with Stream.Failure ->
- msgnl (Cerrors.explain_exn e); exit 1
+ msgnl (Errors.print e); exit 1
end
- | e -> begin msgnl (Cerrors.explain_exn e); exit 1 end
+ | e -> begin msgnl (Errors.print e); exit 1 end
let init arglist =
Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index a39e9c429..72ebecfa7 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -510,7 +510,7 @@ let explain_exn e =
| Error_in_file (s, _, inner) -> None,inner
| _ -> None,e
in
- toploc,(Cerrors.explain_exn exc)
+ toploc,(Errors.print exc)
let eval_call c =
let rec handle_exn e =
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index ddf3ac657..92e29c042 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -309,7 +309,7 @@ let print_toplevel_error exc =
raise Vernacexpr.Quit
| _ ->
(if is_pervasive_exn exc then (mt ()) else locstrm) ++
- Cerrors.explain_exn exc
+ Errors.print exc
(* Read the input stream until a dot is encountered *)
let parse_to_dot =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 05:55:59 +0000