Stop catching async exceptions in hacks that catch anomalies

checker/coqchk_main.ml

@@ -17,9 +17,9 @@ open Environ
 
 let () = at_exit flush_all
 
-let fatal_error info anomaly =
+let fatal_error info code =
   flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]@\n%!" Pp.pp_with info; flush_all ();
-  exit (if anomaly then 129 else 1)
+  exit code
 
 let rocq_root = Id.of_string "Corelib"
 let parse_dir s =
@@ -355,7 +355,7 @@ let parse_args argv =
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then
-        fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
+        fatal_error (str "Directory '" ++ str s ++ str "' does not exist") 1;
       set_coqlib s;
       parse rem
 
@@ -400,7 +400,7 @@ let parse_args argv =
         Flags.quiet := true; parse rem
 
     | s :: _ when s<>"" && s.[0]='-' ->
-        fatal_error (str "Unknown option " ++ str s) false
+        fatal_error (str "Unknown option " ++ str s) 1
     | s :: rem ->  add_compile s; parse rem
   in
   parse (List.tl (Array.to_list argv))
@@ -438,7 +438,7 @@ let init_with_argv argv =
     includes := [];
     make_senv ()
   with e ->
-    fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e)
+    fatal_error (str "Error during initialization :" ++ (explain_exn e)) (CErrors.exit_code e)
 
 let init() = init_with_argv Sys.argv
 
@@ -448,7 +448,7 @@ let run senv =
     flush_all(); senv
   with e ->
     if CDebug.(get_flag misc) then Printexc.print_backtrace stderr;
-    fatal_error (explain_exn e) (is_anomaly e)
+    fatal_error (explain_exn e) (CErrors.exit_code e)
 
 let main () =
   let senv = init() in

dev/ci/user-overlays/21254-SkySkimmer-stop-anomalies.sh

@@ -0,0 +1,5 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi stop-anomalies 21254
+
+overlay equations https://github.com/SkySkimmer/Coq-Equations stop-anomalies 21254
+
+overlay coq_lsp https://github.com/SkySkimmer/coq-lsp stop-anomalies 21254

lib/cErrors.ml

@@ -82,11 +82,17 @@ 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
+  match e with
+  | Anomaly _ -> false (* anomaly is considered unhandled *)
+  | _ -> List.exists is_handled_by !handle_stack
 
-let is_anomaly = function
-| Anomaly _ -> true
-| exn -> not (is_handled exn)
+let is_async = function
+| Control.Timeout | Sys.Break | Out_of_memory | Stack_overflow -> true
+| e -> Memprof_coq.is_interrupted()
+
+let exit_code e = if is_handled e then 1 else 129
+
+let is_sync_anomaly e = not (is_async e) && not (is_handled e)
 
 (** Printing of additional error info, from Exninfo *)
 let additional_error_info_handler = ref []

lib/cErrors.mli

@@ -25,8 +25,16 @@ val anomaly : ?loc:Loc.t -> ?info:Exninfo.info -> ?label:string -> Pp.t -> 'a
 (** Raise an anomaly, with an optional location and an optional
     label identifying the anomaly. *)
 
-val is_anomaly : exn -> bool
-(** Check whether a given exception is an anomaly.
+val exit_code : exn -> int
+(** Return [1] for most exceptions and [129] for exceptions which
+    would print the "Please report" message. *)
+
+val is_async : exn -> bool
+(** Whether the exception may have been raised asynchronously
+    (Timeout, stack overflow, etc). Avoid catching such exceptions at all costs! *)
+
+val is_sync_anomaly : exn -> bool
+(** Check whether a given exception is an anomaly and not asynchronous.
     This is mostly provided for compatibility. Please avoid doing specific
     tricks with anomalies thanks to it. See rather [noncritical] below. *)
 

plugins/ltac/tacinterp.ml

@@ -1868,7 +1868,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let op = interp_typed_pattern ist env sigma op in
-        let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in
+        let to_catch = function Not_found -> true | e -> CErrors.is_sync_anomaly e in
         let c_interp patvars env sigma =
           let lfun' = Id.Map.fold (fun id c lfun ->
             Id.Map.add id (Value.of_constr c) lfun)

pretyping/reductionops.ml

@@ -1143,15 +1143,17 @@ let clos_norm_flags flgs env sigma t =
       (Evarutil.create_clos_infos env sigma flgs)
       (CClosure.create_tab ())
       (Esubst.subs_id 0, UVars.Instance.empty) (EConstr.Unsafe.to_constr t))
-  with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
+  with e when is_sync_anomaly e ->
+    user_err Pp.(str "Tried to normalize ill-typed term")
 
 let clos_whd_flags flgs env sigma t =
   try
     EConstr.of_constr (CClosure.whd_val
       (Evarutil.create_clos_infos env sigma flgs)
       (CClosure.create_tab ())
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
-  with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
+  with e when is_sync_anomaly e ->
+    user_err Pp.(str "Tried to normalize ill-typed term")
 
 let nf_beta = clos_norm_flags RedFlags.beta
 let nf_betaiota = clos_norm_flags RedFlags.betaiota
@@ -1192,7 +1194,7 @@ let _ = CErrors.register_handler (function
 
 let report_anomaly (e, info) =
   let e =
-    if is_anomaly e then AnomalyInConversion e
+    if is_sync_anomaly e then AnomalyInConversion e
     else e
   in
   Exninfo.iraise (e, info)

stm/stmargs.ml

@@ -10,7 +10,7 @@
 
 let fatal_error exn =
   Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
-  let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
+  let exit_code = CErrors.exit_code exn in
   exit exit_code
 
 let set_worker_id opt s =

tactics/tactics.ml

@@ -2103,7 +2103,7 @@ let declare_intro_decomp_eq f = intro_decomp_eq_function := f
 
 let my_find_eq_data_decompose env sigma t =
   try Some (find_eq_data_decompose env sigma t)
-  with e when is_anomaly e
+  with e when is_sync_anomaly e
     (* Hack in case equality is not yet defined... one day, maybe,
        known equalities will be dynamically registered *)
       -> None

topbin/rocqnative.ml

@@ -386,5 +386,5 @@ let () =
     compile senv ~in_file
   with exn ->
     Format.eprintf "Error: @[%a@]@\n%!" Pp.pp_with (CErrors.print exn);
-    let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
+    let exit_code = CErrors.exit_code exn in
     exit exit_code

toplevel/coqc.ml

@@ -57,7 +57,7 @@ let coqc_run copts ~opts injections =
     flush_all();
     Topfmt.print_err_exn exn;
     flush_all();
-    let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
+    let exit_code = CErrors.exit_code exn in
     exit exit_code
 
 let fix_stm_opts opts stm_opts = match opts.Coqcargs.compilation_mode with

toplevel/coqcargs.ml

@@ -46,7 +46,7 @@ let depr opt =
 (* XXX Remove this duplication with Coqargs *)
 let fatal_error exn =
   Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
-  let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
+  let exit_code = CErrors.exit_code exn in
   exit exit_code
 
 let error_missing_arg s =

toplevel/coqtop.ml

@@ -45,7 +45,7 @@ let fatal_error_exn exn =
   Topfmt.(in_phase ~phase:Initialization print_err_exn exn);
   flush_all ();
   let exit_code =
-    if (CErrors.is_anomaly exn) then 129 else 1
+    CErrors.exit_code exn
   in
   exit exit_code
 

vernac/vernacControl.ml

@@ -159,9 +159,8 @@ let with_fail f : (Loc.t option * Pp.t, 'a) result =
   | e ->
     (* The error has to be printed in the failing state *)
     let _, info as exn = Exninfo.capture e in
-    (* Don't turn Sys.Break and anomalies into successes
-       NB: on windows Sys.Break is used instead of Control.Timeout *)
-    if e = Sys.Break || CErrors.is_anomaly e then Exninfo.iraise exn;
+    (* Don't catch async exceptions, don't turn anomalies into successes *)
+    if CErrors.is_async e || CErrors.is_sync_anomaly e then Exninfo.iraise exn;
     Ok (Loc.get_loc info, CErrors.iprint exn)
 
 type ('st0,'st) with_local_state = { with_local_state : 'a. 'st0 -> (unit -> 'a) -> 'st * 'a }