Sledgehammer already has its own ways of reporting and recovering from crashes in external provers -- no need to additionally print scores of warnings (cf. 4b0daca2bf88)
1.1 --- a/src/HOL/Tools/SMT/smt_solver.ML Thu Jul 26 10:48:03 2012 +0200
1.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML Thu Jul 26 10:48:03 2012 +0200
1.3 @@ -52,8 +52,8 @@
1.4 local
1.5
1.6 fun make_cmd command options problem_path proof_path = space_implode " " (
1.7 - map File.shell_quote (command () @ options) @
1.8 - [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
1.9 + "(exec 2>&1;" :: map File.shell_quote (command () @ options) @
1.10 + [File.shell_path problem_path, ")", ">", File.shell_path proof_path])
1.11
1.12 fun trace_and ctxt msg f x =
1.13 let val _ = SMT_Config.trace_msg ctxt (fn () => msg) ()
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 26 10:48:03 2012 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Jul 26 10:48:03 2012 +0200
2.3 @@ -775,9 +775,9 @@
2.4 val args = arguments ctxt full_proof extra slice_timeout
2.5 (ord, ord_info, sel_weights)
2.6 val command =
2.7 - File.shell_path command0 ^ " " ^ args ^ " " ^
2.8 - File.shell_path prob_file
2.9 - |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1"
2.10 + "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
2.11 + File.shell_path prob_file ^ ")"
2.12 + |> enclose "TIMEFORMAT='%3R'; { time " " ; }"
2.13 val _ =
2.14 atp_problem
2.15 |> lines_for_atp_problem format ord ord_info