Stop catching async exceptions in hacks that catch anomalies

Typically the reductionops "Tried to normalize ill-typed term" hack
deliberately catches anomalies (including those from CErrors.anomaly)
but shouldn't catch async exceptions.

Hopefully fixes the non working Fail Timeout in bedrock2, we could
also revert #21216 for our own test suite.

(debugging tip: apply

~~~diff
@@ -32,7 +32,14 @@ let check_for_interrupt () =
 (* This function assumes it is the only function calling [setitimer] *)
 let unix_timeout n f x =
   let open Unix in
-  let timeout_handler _ = raise Timeout in
+  let timeout_handler _ =
+    let info = Exninfo.reify () in
+    let () =
+      Exninfo.get_backtrace info |> Option.iter @@ fun bt ->
+      Printf.eprintf "timeout at %s\n%!" (Exninfo.backtrace_to_string bt)
+    in
+    raise Timeout
+  in
   let old_timer = getitimer ITIMER_REAL in
   (* Here we assume that the existing timer will also interrupt us. *)
   if old_timer.it_value > 0. && old_timer.it_value <= n then Ok (f x) else
~~~

then run a buggy Timeout with `Set Debug "backtrace"` on until you get
the bug, the function which catches the timeout exn should be in the
printed backtrace. For instance I had

~~~
Called from Reductionops.infer_conv_gen in file "pretyping/reductionops.ml", line 1324, characters 10-52
~~~
when trying the Fail Timeout in bedrock2 LeakageSemantics.)

Author: SkySkimmer

checker/coqchk_main.ml

@@ -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)) (is_anomaly ~async:true 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) (is_anomaly ~async:true 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

@@ -84,9 +84,10 @@ 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
+let is_anomaly ~async = function
 | Anomaly _ -> true
-| exn -> not (is_handled exn)
+| Control.Timeout | Sys.Break | Out_of_memory | Stack_overflow -> async
+| exn -> if Memprof_coq.is_interrupted() then async else not (is_handled exn)
 
 (** Printing of additional error info, from Exninfo *)
 let additional_error_info_handler = ref []

lib/cErrors.mli

@@ -25,10 +25,13 @@ 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
+val is_anomaly : async:bool -> exn -> bool
 (** Check whether a given exception is an anomaly.
     This is mostly provided for compatibility. Please avoid doing specific
-    tricks with anomalies thanks to it. See rather [noncritical] below. *)
+    tricks with anomalies thanks to it. See rather [noncritical] below.
+
+    [async] is the value returned for asynchronous exceptions (timeouts, user interrupts, etc).
+    Avoid catching these at all costs! *)
 
 exception UserError of Pp.t
 (** Main error signaling exception. It carries a header plus a pretty printing

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_anomaly ~async:false 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_anomaly ~async:false 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_anomaly ~async:false 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_anomaly ~async:false 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 = if (CErrors.is_anomaly ~async:true exn) then 129 else 1 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_anomaly ~async:false 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 = if (CErrors.is_anomaly ~async:true exn) then 129 else 1 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 = if (CErrors.is_anomaly ~async:true exn) then 129 else 1 in
     exit exit_code
 
 let fix_stm_opts opts stm_opts = match opts.Coqcargs.compilation_mode with