1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
open Pp
(** Aliases *)
let push = Exninfo.capture
exception Anomaly of string option * Pp.t
let _ =
let pr = function
| Anomaly (s, pp) -> Some ("\"Anomaly: " ^ string_of_ppcmds pp ^ "\"")
| _ -> None
in
Printexc.register_printer pr
let anomaly ?loc ?info ?label pp =
let info = Option.default Exninfo.null info in
let info = Option.cata (Loc.add_loc info) info loc in
Exninfo.iraise (Anomaly (label, pp), info)
exception UserError of Pp.t
let _ = Printexc.register_printer (function
| UserError msg ->
Some (Format.asprintf "@[Coq Error: %a@]" Pp.pp_with msg)
| _ -> None)
let user_err ?loc ?info strm =
let info = Option.default Exninfo.null info in
let info = Option.cata (Loc.add_loc info) info loc in
Exninfo.iraise (UserError strm, info)
exception Timeout = Control.Timeout
(** Only anomalies should reach the bottom of the handler stack.
In usual situation, the [handle_stack] is treated as it if was always
non-empty with [print_anomaly] as its bottom handler. *)
let where = function
| None -> mt ()
| Some s ->
str "in " ++ str s ++ str ":" ++ spc ()
let raw_anomaly e = match e with
| Anomaly (s, pps) ->
where s ++ pps
| Assert_failure _ | Match_failure _ ->
str (Printexc.to_string e) ++ str "."
| _ ->
str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "."
let print_backtrace e = match Exninfo.get_backtrace e with
| None -> None
| Some bt ->
let bt = str (Exninfo.backtrace_to_string bt) in
Some (hov 0 bt)
let print_anomaly askreport e =
if askreport then
hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e)) ++ spc () ++
hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".")
else
hov 0 (raw_anomaly e)
let handle_stack = ref []
let register_handler h = handle_stack := h::!handle_stack
let is_handled e =
let is_handled_by h = Option.has_some (h e) in
List.exists is_handled_by !handle_stack
let is_anomaly = function
| Anomaly _ -> true
| exn -> not (is_handled exn)
(** Printing of additional error info, from Exninfo *)
let additional_error_info_handler = ref []
let register_additional_error_info (f : Exninfo.info -> Pp.t option) =
additional_error_info_handler := f :: !additional_error_info_handler
let () = register_additional_error_info print_backtrace
(** [print_gen] is a general exception printer which tries successively
all the handlers of a list, and finally a [bottom] handler if all
others have failed *)
let rec print_gen ~anomaly stk e =
match stk with
| [] ->
print_anomaly anomaly e
| h::stk' ->
match h e with
| Some err_msg -> err_msg
| None -> print_gen ~anomaly stk' e
let info =
let pp =
CList.map_filter (fun f -> f info) !additional_error_info_handler
in
if CList.is_empty pp then mt()
else fnl() ++ prlist_with_sep fnl (fun x -> x) pp
let print_gen ~anomaly (e, info) =
let = print_extra info in
try
print_gen ~anomaly !handle_stack e ++ extra_msg
with exn ->
let exn, info = Exninfo.capture exn in
str "<in exception printer>:" ++ spc() ++ print_anomaly anomaly exn ++ print_extra info ++ fnl() ++
str "<original exception>:" ++ spc() ++ print_anomaly false e ++ extra_msg
(** The standard exception printer *)
let iprint (e, info) =
print_gen ~anomaly:true (e,info)
let print e =
iprint (e, Exninfo.info e)
(** Same as [print], except that the "Please report" part of an anomaly
isn't printed (used in Ltac debugging). *)
let iprint_no_report (e, info) =
print_gen ~anomaly:false (e,info)
let print_no_report e = iprint_no_report (e, Exninfo.info e)
(** Predefined handlers **)
let _ = register_handler begin function
| UserError pps ->
Some pps
| _ -> None
end
(** Critical exceptions should not be caught and ignored by mistake
by inner functions during a [vernacinterp]. They should be handled
only at the very end of interp, to be displayed to the user. *)
[@@@ocaml.warning "-52"]
let noncritical = function
| Sys.Break | Out_of_memory | Stack_overflow
| Assert_failure _ | Match_failure _ | Anomaly _
| Control.Timeout -> false
| Invalid_argument "equal: functional value" -> false
| _ -> not (Memprof_coq.is_interrupted ())
[@@@ocaml.warning "+52"]
let to_result ~f x =
try Ok (f x)
with exn when noncritical exn ->
let iexn = Exninfo.capture exn in
Error iexn