Fix exception catchalls

Some remain when they may be correct, cf coq#19217

boot/util.ml

@@ -10,7 +10,7 @@
 
 let parse_env_line l =
   try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
-  with _ -> None
+  with Scanf.Scan_failure _ | End_of_file -> None
 
 let with_ic file f =
   let ic = open_in file in

checker/check.ml

@@ -312,7 +312,7 @@ let marshal_in_segment (type a) ~validate ~value ~(segment : a ObjFile.segment)
         let digest = Digest.input ch in
         let () = if not (String.equal digest segment.ObjFile.hash) then raise_notrace Exit in
         v
-      with _ ->
+      with exn when CErrors.noncritical exn ->
         CErrors.user_err (str "Corrupted file " ++ quote (str f))
     in
     let () = Validate.validate value v in

checker/checker.ml

@@ -55,7 +55,7 @@ let get_version () =
     let rev = input_line ch in
     let () = close_in ch in
     Printf.sprintf "%s (%s)" ver rev
-  with _ -> Coq_config.version
+  with Sys_error _ | End_of_file -> Coq_config.version
 
 let print_header () =
   Printf.printf "Welcome to Chicken %s\n%!" (get_version ())

clib/terminal.ml

@@ -312,7 +312,7 @@ let parse s =
         let attrs = List.map int_of_string attrs in
         let attrs = parse_style (make ()) attrs in
         (name, attrs) :: accu
-      with _ -> accu
+      with Failure _ | Invalid_argument _ -> accu
     in
     accu
   | _ -> accu

engine/termops.ml

@@ -88,7 +88,10 @@ module Internal = struct
 
   let protect f x =
     try f x
-    with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
+    with e when
+        (* maybe should be just "not is_interrupted"? *)
+        CErrors.noncritical e || !Flags.in_debugger ->
+      str "EXCEPTION: " ++ str (Printexc.to_string e)
 
   let print_kconstr env sigma a =
     protect (fun c -> print_constr_env env sigma c) a

kernel/nativelib.ml

@@ -43,7 +43,7 @@ let () = at_exit (fun () ->
         let d = Lazy.force my_temp_dir in
         Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d);
         Unix.rmdir d
-      with e ->
+      with (Unix.Unix_error _ | Sys_error _) as e ->
         Feedback.msg_warning
           Pp.(str "Native compile: failed to cleanup: " ++
               str(Printexc.to_string e) ++ fnl()))

lib/envars.ml

@@ -14,7 +14,7 @@ open Util
 
 let parse_env_line l =
   try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
-  with _ -> None
+  with Scanf.Scan_failure _ | End_of_file -> None
 
 let with_ic file f =
   let ic = open_in file in

lib/spawn.ml

@@ -147,7 +147,7 @@ let spawn_with_control prefer_sock env prog args =
 let output_death_sentence pid oob_req =
   prerr_endline ("death sentence for " ^ pid);
   try output_value oob_req ReqDie; flush oob_req
-  with e -> prerr_endline ("death sentence: " ^ Printexc.to_string e)
+  with e when CErrors.noncritical e -> prerr_endline ("death sentence: " ^ Printexc.to_string e)
 
 (* spawn a process and read its output asynchronously *)
 module Async(ML : MainLoopModel) = struct
@@ -182,7 +182,7 @@ let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) =
     Option.iter close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid Sys.sigkill;
     p.watch <- None
-  with e -> prerr_endline ("kill: "^Printexc.to_string e) end
+  with e when CErrors.noncritical e -> prerr_endline ("kill: "^Printexc.to_string e) end
 
 let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
     prog args callback
@@ -249,7 +249,7 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) =
     Option.iter close_in_noerr oob_resp;
     Option.iter close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid Sys.sigkill;
-  with e -> prerr_endline ("kill: "^Printexc.to_string e) end
+  with e when CErrors.noncritical e -> prerr_endline ("kill: "^Printexc.to_string e) end
 
 let rec wait p =
   (* On windows kill is not reliable, so wait may never return. *)

lib/system.ml

@@ -74,7 +74,7 @@ let apply_subdir f path name =
     | Unix.S_REG -> f (FileRegular name)
     | _ -> ()
 
-let readdir dir = try Sys.readdir dir with any -> [||]
+let readdir dir = try Sys.readdir dir with Sys_error _ -> [||]
 
 let process_directory f path =
   Array.iter (apply_subdir f path) (readdir path)

plugins/ltac/tactic_debug.ml

@@ -69,7 +69,7 @@ let update_bpt fname offset opt =
           (try
             let p = Loadpath.find_load_path (CUnix.physical_path_of_string dirname) in
             DirPath.repr (Loadpath.logical p)
-          with _ -> []))
+          with exn when CErrors.noncritical exn -> []))
     end
   in
   let dirpath = DirPath.to_string dp in
@@ -170,14 +170,14 @@ let cvt_loc loc =
              let knlen = String.length text in
              let lastdot = String.rindex text '.' in
              String.sub text (lastdot+1) (knlen - (lastdot + 1))
-           with _ -> text
+           with exn when CErrors.noncritical exn -> text
          in
          Printf.sprintf "%s:%d, %s  (%s)" routine line_nb file module_name;
        | Some { fname=ToplevelInput; line_nb } ->
          let items = String.split_on_char '.' text in
          Printf.sprintf "%s:%d, %s" (List.nth items 1) line_nb (List.hd items);
        | _ -> text
-   with _ -> text
+   with exn when CErrors.noncritical exn -> text
 
 let format_stack s =
   List.map (fun (tac, loc) ->

plugins/micromega/coq_micromega.ml

@@ -1972,11 +1972,7 @@ Tacticals.tclTHEN
                   ( EConstr.mkVar goal_name
                   , arith_args @ List.map EConstr.mkVar ids )))
       with
-      | CsdpNotFound -> fail_csdp_not_found ()
-      | x ->
-        if debug then
-          Tacticals.tclFAIL (Pp.str (Printexc.get_backtrace ()))
-        else raise x)
+      | CsdpNotFound -> fail_csdp_not_found ())
 
 let micromega_wit_gen pre_process cnf spec prover wit_id ff =
   Proofview.Goal.enter (fun gl ->
@@ -1998,12 +1994,7 @@ let micromega_wit_gen pre_process cnf spec prover wit_id ff =
           let tres' = EConstr.mkApp (Lazy.force coq_list, [|spec.proof_typ|]) in
           Tactics.letin_tac
             None (Names.Name wit_id) res' (Some tres') Locusops.nowhere
-      with
-      | CsdpNotFound -> fail_csdp_not_found ()
-      | x ->
-        if debug then
-          Tacticals.tclFAIL (Pp.str (Printexc.get_backtrace ()))
-        else raise x)
+      with CsdpNotFound -> fail_csdp_not_found ())
 
 let micromega_order_changer cert env ff =
   (*let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *)
@@ -2127,8 +2118,7 @@ let micromega_genr prover tac =
                 [ Generalize.generalize (List.map EConstr.mkVar ids)
                 ; Tactics.exact_check
                     (EConstr.applist (EConstr.mkVar goal_name, arith_args)) ] ]
-      with
-      | CsdpNotFound -> fail_csdp_not_found ())
+      with CsdpNotFound -> fail_csdp_not_found ())
 
 let lift_ratproof prover l =
   match prover l with

plugins/micromega/mutils.ml

@@ -360,10 +360,11 @@ let command exe_path args vl =
       | Unix.WEXITED 0 -> (
         let inch = Unix.in_channel_of_descr stdout_read in
         try Marshal.from_channel inch
-        with any ->
+        with (End_of_file | Failure _) as exn ->
           failwith
-            (Printf.sprintf "command \"%s\" exited %s" exe_path
-               (Printexc.to_string any)) )
+            (Printf.sprintf "command \"%s\" exited with code 0 but result could not be read back: %s"
+               exe_path
+               (Printexc.to_string exn)) )
       | Unix.WEXITED i ->
         failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
       | Unix.WSIGNALED i ->
@@ -373,7 +374,7 @@ let command exe_path args vl =
     (* Cleanup  *)
       (fun () ->
       List.iter
-        (fun x -> try Unix.close x with any -> ())
+        (fun x -> try Unix.close x with Unix.Unix_error _ -> ())
         [ stdin_read
         ; stdin_write
         ; stdout_read

plugins/ssr/ssrcommon.ml

@@ -795,8 +795,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
    loop ty [] sigma m
 
 let dependent_apply_error =
-  try CErrors.user_err (Pp.str "Could not fill dependent hole in \"apply\"")
-  with err -> err
+  CErrors.UserError (Pp.str "Could not fill dependent hole in \"apply\"")
 
 (* TASSI: Sometimes Coq's apply fails. According to my experience it may be
  * related to goals that are products and with beta redexes. In that case it

sysinit/coqinit.ml

@@ -120,7 +120,7 @@ let print_memory_stat () =
     let oc = open_out fn in
     Gc.print_stat oc;
     close_out oc
-  with _ -> ()
+  with exn when CErrors.noncritical exn -> ()
 
 let init_load_paths opts =
   let open Coqargs in

tools/configure/util.ml

@@ -172,7 +172,7 @@ let is_executable f =
 (** Equivalent of rm -f *)
 
 let safe_remove f =
-  try Unix.chmod f 0o644; Sys.remove f with _ -> ()
+  try Unix.chmod f 0o644; Sys.remove f with Unix.Unix_error _ | Sys_error _ -> ()
 
 (** The PATH list for searching programs *)
 
@@ -233,4 +233,7 @@ let write_config_file ~file ?(bin=false) action =
     action o;
     close_out o;
     Unix.chmod file 0o444
-  with _ -> close_out o; safe_remove file
+  with exn ->
+    close_out o;
+    safe_remove file;
+    raise exn

toplevel/common_compile.ml

@@ -30,7 +30,7 @@ let ensure_ext ext f =
   end
 
 let safe_chop_extension f =
-  try Filename.chop_extension f with _ -> f
+  try Filename.chop_extension f with Invalid_argument _ -> f
 
 let ensure_bname src tgt =
   let src, tgt = Filename.basename src, Filename.basename tgt in

toplevel/coqtop.ml

@@ -26,7 +26,7 @@ let get_version ~boot =
     let rev = input_line ch in
     let () = close_in ch in
     Printf.sprintf "%s (%s)" ver rev
-  with _ -> Coq_config.version
+  with Sys_error _ | End_of_file -> Coq_config.version
 
 let print_header ~boot () =
   Feedback.msg_info (str "Welcome to Coq " ++ str (get_version ~boot));

vernac/indschemes.ml

@@ -119,7 +119,7 @@ let alarm what internal msg =
 
 let try_declare_scheme ?locmap what f internal names kn =
   try f ?locmap names kn
-  with e ->
+  with e when CErrors.noncritical e ->
   let e = Exninfo.capture e in
   let rec extract_exn = function Logic_monad.TacticFailure e -> extract_exn e | e -> e in
   let msg = match extract_exn (fst e) with
@@ -168,10 +168,9 @@ let try_declare_scheme ?locmap what f internal names kn =
     | InternalDependencies ->
          alarm what internal
            (strbrk "Inductive types with internal dependencies in constructors not supported.")
-    | e when CErrors.noncritical e ->
+    | e ->
         alarm what internal
           (str "Unexpected error during scheme creation: " ++ CErrors.print e)
-    | _ -> Exninfo.iraise e
   in
   match msg with
   | None -> ()

vernac/topfmt.ml

@@ -270,7 +270,7 @@ let make_style_stack () =
     | Format.String_tag tag ->
       let (tpfx, _) = split_tag tag in
       if tpfx = start_pfx then "" else begin
-        if tpfx = end_pfx then diff_tag_stack := (try List.tl !diff_tag_stack with tl -> []);
+        if tpfx = end_pfx then diff_tag_stack := (match !diff_tag_stack with _ :: tl -> tl | [] -> []);
         match !style_stack with
         | []       -> (* Something went wrong, we fallback *)
           Terminal.eval default_style