diff --git a/boot/util.ml b/boot/util.ml index 395bf72815f28..86342e742206a 100644 --- a/boot/util.ml +++ b/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 diff --git a/checker/check.ml b/checker/check.ml index c7b575fae542c..3e0d3cfa7ffd8 100644 --- a/checker/check.ml +++ b/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 diff --git a/checker/checker.ml b/checker/checker.ml index 80330f2443bf4..d9bdfd76f03ca 100644 --- a/checker/checker.ml +++ b/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 ()) @@ -396,7 +396,7 @@ let init_with_argv argv = (List.rev !includes); includes := []; make_senv () - with e -> + with e [@coqlint.allow_catchall "fatal"] -> fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e) let init() = init_with_argv Sys.argv @@ -405,7 +405,7 @@ let run senv = try let senv = compile_files senv in flush_all(); senv - with e -> + with e [@coqlint.allow_catchall "fatal"] -> if CDebug.(get_flag misc) then Printexc.print_backtrace stderr; fatal_error (explain_exn e) (is_anomaly e) diff --git a/clib/terminal.ml b/clib/terminal.ml index 00945f7507219..3d114227cb0a5 100644 --- a/clib/terminal.ml +++ b/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 diff --git a/engine/termops.ml b/engine/termops.ml index 67001f988cc72..98b1ac5ea678f 100644 --- a/engine/termops.ml +++ b/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 diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 7c25fcc924825..cf184566d1a54 100644 --- a/kernel/nativelib.ml +++ b/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())) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index fb1935cd4d18b..c4b26d58ce3df 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -117,7 +117,7 @@ let print_gen ~anomaly (e, info) = in try extra_msg ++ print_gen ~anomaly !handle_stack e - with exn -> + with exn [@coqlint.allow_catchall "grandfathered"] -> let exn, info = Exninfo.capture exn in (* exception in error printer *) str ":" ++ spc() ++ print_anomaly anomaly exn ++ diff --git a/lib/envars.ml b/lib/envars.ml index 3f1d024d26959..ab490b3408011 100644 --- a/lib/envars.ml +++ b/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 diff --git a/lib/spawn.ml b/lib/spawn.ml index b509eb042b9bd..b10e04f3184fe 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -148,7 +148,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 @@ -183,7 +183,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 @@ -252,7 +252,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. *) diff --git a/lib/system.ml b/lib/system.ml index e6085d8b136d4..334686710b026 100644 --- a/lib/system.ml +++ b/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) @@ -362,7 +362,7 @@ let measure_duration f x = let y = f x in let stop = get_time() in Ok (y, duration_between ~start ~stop) - with e -> + with e [@coqlint.allow_catchall "caller must reraise"] -> let stop = get_time() in let exn = Exninfo.capture e in Error (exn, duration_between ~start ~stop) @@ -399,7 +399,7 @@ let count_instructions f x = let y = f x in let c_end = Instr.read_counter () in Ok(y, instructions_between ~c_start ~c_end) - with e -> + with e [@coqlint.allow_catchall "caller must reraise"] -> let exn = Exninfo.capture e in let c_end = Instr.read_counter () in Error(exn, instructions_between ~c_start ~c_end) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 4524caffb68da..2cf6ce27a4d47 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/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) -> diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index c971b993d7bb5..8843c44029ccf 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -217,7 +217,8 @@ let catchable_exception = function *) let wrap_exceptions ?(passthrough=false) f = try f () - with e -> + with e [@coqlint.allow_catchall "will be reraised if critical"] -> + (* not sure if it's fully correct to do a tclBIND when we got a critical exn *) let e, info = Exninfo.capture e in set_bt info >>= fun info -> if not passthrough && catchable_exception e diff --git a/plugins/ltac2/tac2print.ml b/plugins/ltac2/tac2print.ml index 134355353af7b..608e646532172 100644 --- a/plugins/ltac2/tac2print.ml +++ b/plugins/ltac2/tac2print.ml @@ -870,20 +870,26 @@ end let () = register_init "constr" begin fun env sigma c -> let c = to_constr c in - let c = try Printer.pr_leconstr_env env sigma c with _ -> str "..." in + let c = try Printer.pr_leconstr_env env sigma c + with _ [@coqlint.allow_catchall "grandfathered"] -> str "..." + in hov 2 (str "constr:(" ++ c ++ str ")") end let () = register_init "preterm" begin fun env sigma c -> let c = to_preterm c in (* XXX should we get the ltac2 env out of the closure and print it too? Maybe with a debug flag? *) - let c = try Printer.pr_closed_glob_env env sigma c with _ -> str "..." in + let c = try Printer.pr_closed_glob_env env sigma c + with _ [@coqlint.allow_catchall "grandfathered"] -> str "..." + in hov 2 (str "preterm:(" ++ c ++ str ")") end let () = register_init "pattern" begin fun env sigma c -> let c = to_pattern c in - let c = try Printer.pr_lconstr_pattern_env env sigma c with _ -> str "..." in + let c = try Printer.pr_lconstr_pattern_env env sigma c + with _ [@coqlint.allow_catchall "grandfathered"] -> str "..." + in hov 2 (str "pat:(" ++ c ++ str ")") end diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index d1e43a81dae55..cc25f23a250f2 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1971,11 +1971,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 -> @@ -1997,12 +1993,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 *) @@ -2126,8 +2117,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 diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml index b9a55a4b504d8..39521ee387c16 100644 --- a/plugins/micromega/mutils.ml +++ b/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 diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 29426bb1c5a5b..cb69b8dbbfca3 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/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 diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e91456f303165..62769340604f9 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1229,7 +1229,7 @@ let is_fconv ?(reds=TransparentState.full) pb env sigma t1 t2 = | Result.Error (Some e) -> Empty.abort e end with - | e -> + | e [@coqlint.allow_catchall "report_anomaly"] -> let e = Exninfo.capture e in report_anomaly e @@ -1337,7 +1337,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Conversion.CUMUL) | Result.Error (Some e) -> raise (UGraph.UniverseInconsistency e) with | UGraph.UniverseInconsistency _ when catch_incon -> None - | e -> + | e [@coqlint.allow_catchall "report_anomaly"] -> let e = Exninfo.capture e in report_anomaly e @@ -1368,7 +1368,7 @@ let infer_conv_ustate ?(catch_incon=true) ?(pb=Conversion.CUMUL) | Result.Error (Some e) -> raise (UGraph.UniverseInconsistency e) with | UGraph.UniverseInconsistency _ when catch_incon -> None - | e -> + | e [@coqlint.allow_catchall "report_anomaly"] -> let e = Exninfo.capture e in report_anomaly e diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index c9c8e18e8037d..44bdcbd57d888 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -336,7 +336,7 @@ module Make(T : Task) () = struct stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2 | End_of_file -> stm_prerr_endline "connection lost"; flush_all (); exit 2 - | e -> + | e [@coqlint.allow_catchall "fatal"] -> stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]); flush_all (); exit 1 done diff --git a/stm/partac.ml b/stm/partac.ml index 64f33679970bd..bd9da777e876a 100644 --- a/stm/partac.ml +++ b/stm/partac.ml @@ -131,7 +131,7 @@ end = struct (* {{{ *) str" solves the goal and leaves no unresolved existential variables. The following" ++ str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key (Global.env ()) sigma) (Evar.Set.elements evars)) ) - with e -> + with e [@coqlint.allow_catchall "grandfathered"] -> let noncrit = CErrors.noncritical e in RespError (noncrit, CErrors.print e ++ spc() ++ str "(for goal "++int r_goalno ++ str ")") diff --git a/stm/spawned.ml b/stm/spawned.ml index ee9c8e9942804..833e665c97acc 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -34,7 +34,7 @@ let controller h pr pw = | Hello _ -> prerr_endline "internal protocol error"; exit 1 | ReqDie -> prerr_endline "death sentence received"; exit 0 with - | e -> + | e [@coqlint.allow_catchall "fatal"] -> prerr_endline ("control channel broken: " ^ Printexc.to_string e); exit 1 in loop () in diff --git a/stm/stm.ml b/stm/stm.ml index 70dc10157dffd..631ef000208c1 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -772,7 +772,7 @@ end = struct (* {{{ *) let run_command () = try while true do get_last_job () () done - with e -> () (* No failure *) + with e [@coqlint.allow_catchall "grandfathered"] -> () (* No failure *) let command ~now job = if now then job () @@ -2538,7 +2538,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) x c = stm_pperr_endline (fun () -> str "processed with " ++ pr_rc rc ++ str " }}}"); VCS.print (); rc - with e -> + with e [@coqlint.allow_catchall "handle_failure reraises"] -> let e = Exninfo.capture e in handle_failure e vcs @@ -2754,11 +2754,12 @@ let edit_at ~doc id = doc, rc with | Vcs_aux.Expired -> user_err Pp.(str "Unknown state " ++ Stateid.print id ++ str".") - | e -> + | e [@coqlint.allow_catchall "reraises"] -> let (e, info) = Exninfo.capture e in match Stateid.get info with | None -> VCS.print (); + (* should we be raising the original exn when it's critical? *) anomaly (str ("edit_at "^Stateid.to_string id^": ") ++ CErrors.print_no_report e ++ str ".") | Some (_, id) -> diff --git a/stm/stmargs.ml b/stm/stmargs.ml index 7ce306b4c6631..969c680618c4b 100644 --- a/stm/stmargs.ml +++ b/stm/stmargs.ml @@ -133,7 +133,7 @@ let parse_args ~init arglist : Stm.AsyncOpts.stm_opt * string list = in try parse init - with any -> fatal_error any + with any [@coqlint.allow_catchall "fatal"] -> fatal_error any let usage = "\ \n -stm-debug STM debug mode (will trace every transaction)\ diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml index e085f84ede562..4e3365b1b53fe 100644 --- a/sysinit/coqargs.ml +++ b/sysinit/coqargs.ml @@ -444,7 +444,7 @@ let parse_args ~usage ~init arglist : t * string list = in try parse init - with any -> fatal_error any + with any [@coqlint.allow_catchall "fatal"] -> fatal_error any (* We need to reverse a few lists *) let parse_args ~usage ~init args = diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml index 41920e9261220..99e72a714401d 100644 --- a/sysinit/coqinit.ml +++ b/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 diff --git a/tools/configure/util.ml b/tools/configure/util.ml index 6026fa52cfbb9..79764c30cb28b 100644 --- a/tools/configure/util.ml +++ b/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 diff --git a/toplevel/common_compile.ml b/toplevel/common_compile.ml index 5ec70808ac9a6..e82424c93eff8 100644 --- a/toplevel/common_compile.ml +++ b/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 diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index f0649d3146f51..a1f7bfac13915 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -53,7 +53,7 @@ let coqc_run copts ~opts injections = try coqc_main ~opts copts injections; exit 0 - with exn -> + with exn [@coqlint.allow_catchall "fatal"] -> flush_all(); Topfmt.print_err_exn exn; flush_all(); diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index 6871d18df97d9..f5a384c704544 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -134,4 +134,4 @@ let parse arglist : t = let opts, extra = parse default in let args = List.fold_left add_compile opts extra in args - with any -> fatal_error any + with any [@coqlint.allow_catchall "fatal"] -> fatal_error any diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index bc23c54f35aab..80a330147de55 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -294,7 +294,7 @@ let extract_default_loc loc doc_id sid : Loc.t option = try let doc = Stm.get_doc doc_id in Option.cata (fun {CAst.loc} -> loc) None Stm.(get_ast ~doc sid) - with _ -> loc + with exn [@coqlint.allow_catchall "grandfathered"] -> loc (** Coqloop Console feedback handler *) let coqloop_feed (fb : Feedback.feedback) = let open Feedback in @@ -387,7 +387,7 @@ let top_goal_print ~doc c oldp newp = print_and_diff dproof newp end with - | exn -> + | exn [@coqlint.allow_catchall "coqtop allows critical exceptions while printing goal"] -> let (e, info) = Exninfo.capture exn in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in @@ -501,7 +501,7 @@ let read_and_execute ~state = in TopErr.print_error_for_buffer Feedback.Error msg top_buffer; exit 1 - | any -> + | any [@coqlint.allow_catchall "coqtop continues even after critical exceptions"] -> let (e, info) = Exninfo.capture any in let loc = Loc.get_loc info in let msg = CErrors.iprint (e, info) in diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index a0f51f6005220..0d4d1e8a4e91e 100644 --- a/toplevel/coqtop.ml +++ b/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)); @@ -71,7 +71,7 @@ let start_coq custom = (* Init phase *) let opts, custom_opts, state = try init_toplevel custom - with any -> + with any [@coqlint.allow_catchall "fatal"] -> flush_all(); fatal_error_exn any in Feedback.del_feeder init_feeder; @@ -169,7 +169,7 @@ let get_native_name s = [ !Nativelib.output_dir ; Library.native_name_from_filename s ]) - with _ -> "" + with _ [@coqlint.allow_catchall "deliberately silent"] -> "" let coqtop_run ({ run_mode; color_mode },_) ~opts state = match run_mode with diff --git a/vernac/future.ml b/vernac/future.ml index 4b598375c48ce..3174bbcce3a98 100644 --- a/vernac/future.ml +++ b/vernac/future.ml @@ -129,7 +129,7 @@ let rec compute ck : 'a value = try let data = f () in c := Val data; `Val data - with e -> + with e [@coqlint.allow_catchall "grandfathered"] -> let e = Exninfo.capture e in let e = eval_fix_exn fix_exn e in match e with diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index a4bc88feff10e..f699f2cb780f7 100644 --- a/vernac/indschemes.ml +++ b/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 -> () diff --git a/vernac/synterp.ml b/vernac/synterp.ml index 4bf3742fc6422..523779e1c0142 100644 --- a/vernac/synterp.ml +++ b/vernac/synterp.ml @@ -378,7 +378,7 @@ let with_fail f : (Loc.t option * Pp.t, 'a) result = Error x with (* Fail Timeout is a common pattern so we need to support it. *) - | e -> + | e [@coqlint.allow_catchall "critical should count as anomaly and be reraised"] -> (* The error has to be printed in the failing state *) let _, info as exn = Exninfo.capture e in if CErrors.is_anomaly e && e != CErrors.Timeout then Exninfo.iraise exn; diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index ffb2fea32d64b..131d789991d8e 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -266,7 +266,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 @@ -448,7 +448,7 @@ let pr_cmd_header com = let (start,stop) = Option.cata Loc.unloc (0,0) com.CAst.loc in let safe_pr_vernac x = try Ppvernac.pr_vernac x - with e -> str (Printexc.to_string e) in + with e [@coqlint.allow_catchall "grandfathered"] -> str (Printexc.to_string e) in let cmd = noblank (shorten (string_of_ppcmds (safe_pr_vernac com))) in str "Chars " ++ int start ++ str " - " ++ int stop ++ str " [" ++ str cmd ++ str "] " diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index 457c364389c51..90694b2bca925 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -28,7 +28,7 @@ let with_fail f : (Loc.t option * Pp.t, unit) result = Error () with (* Fail Timeout is a common pattern so we need to support it. *) - | e -> + | e [@coqlint.allow_catchall "critical should count as anomaly and be reraised"] -> (* The error has to be printed in the failing state *) let _, info as exn = Exninfo.capture e in if CErrors.is_anomaly e && e != CErrors.Timeout then Exninfo.iraise exn;