Merge branch 'catch_why3_error' into 'master'

Print backtrace only in debug mode

See merge request laiser/caisar!17

src/main.ml

@@ -47,6 +47,9 @@ let setup_logs =
   in
   Term.(const setup_log $ Logs_cli.level ())
 
+let log_level_is_debug () =
+  match Logs.level () with Some Debug -> true | _ -> false
+
 (* -- Commands. *)
 
 let config detect () =
@@ -54,7 +57,7 @@ let config detect () =
   then (
     Logs.debug (fun m -> m "Automatic detection.");
     let config =
-      let debug = match Logs.level () with Some Debug -> true | _ -> false in
+      let debug = log_level_is_debug () in
       Autodetect.autodetection ~debug ()
     in
     let open Why3 in
@@ -66,7 +69,7 @@ let config detect () =
         provers))
 
 let verify format loadpath memlimit timeout prover files =
-  let debug = match Logs.level () with Some Debug -> true | _ -> false in
+  let debug = log_level_is_debug () in
   List.iter
     ~f:(Verification.verify ~debug format loadpath ?memlimit ?timeout ~prover)
     files
@@ -173,6 +176,11 @@ let default_cmd =
     Term.info caisar ~version ~doc ~sdocs ~exits:Term.default_exits ~man )
 
 let () =
-  match Term.(eval_choice default_cmd [ config_cmd; verify_cmd ]) with
-  | `Error _ -> Caml.exit 1
-  | _ -> Caml.exit (if Logs.err_count () > 0 then 1 else 0)
+  try
+    match
+      Term.(eval_choice ~catch:false default_cmd [ config_cmd; verify_cmd ])
+    with
+    | `Error _ -> Caml.exit 1
+    | _ -> Caml.exit (if Logs.err_count () > 0 then 1 else 0)
+  with exn when not (log_level_is_debug ()) ->
+    Fmt.epr "%a@." Why3.Exn_printer.exn_printer exn