--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Thu Sep 28 14:43:07 2023 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Thu Sep 28 19:36:54 2023 +0200
@@ -273,31 +273,32 @@
local
fun run_sh params keep pos state =
- let
- fun set_file_name (SOME (dir, keep_probs, keep_proofs)) =
- let
- val filename = "prob_" ^
- StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^
- StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos))
- in
- Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__")
- #> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir)
- #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir)
- #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
- end
- | set_file_name NONE = I
- val state' = state
- |> Proof.map_context (set_file_name keep)
+ \<^try>\<open>
+ let
+ fun set_file_name (SOME (dir, keep_probs, keep_proofs)) =
+ let
+ val filename = "prob_" ^
+ StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^
+ StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos))
+ in
+ Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__")
+ #> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir)
+ #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir)
+ #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
+ end
+ | set_file_name NONE = I
+ val state' = state
+ |> Proof.map_context (set_file_name keep)
- val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () =>
- Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1
- Sledgehammer_Fact.no_fact_override state') ()
- in
- (sledgehammer_outcome, msg, cpu_time)
- end
- handle
- ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0)
- | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0)
+ val ((_, (sledgehammer_outcome, msg)), cpu_time) = Mirabelle.cpu_time (fn () =>
+ Sledgehammer.run_sledgehammer params Sledgehammer_Prover.Normal NONE 1
+ Sledgehammer_Fact.no_fact_override state') ()
+ in
+ (sledgehammer_outcome, msg, cpu_time)
+ end
+ catch ERROR msg => (Sledgehammer.SH_Unknown, " error: " ^ msg, 0)
+ | _ => (Sledgehammer.SH_Unknown, " error: unexpected error", 0)
+ \<close>
in
--- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Sep 28 14:43:07 2023 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Sep 28 19:36:54 2023 +0200
@@ -1006,23 +1006,25 @@
if overlord then ()
else List.app (ignore o try File.rm) [kki_path, out_path, err_path]
in
- let
- val _ = File.write kki_path kki
- val rc =
- Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
- \\"$KODKODI/bin/kodkodi\"" ^
- (" -max-msecs " ^ string_of_int timeout) ^
- (if solve_all then " -solve-all" else "") ^
- " -max-solutions " ^ string_of_int max_solutions ^
- (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^
- " < " ^ File.bash_path kki_path ^
- " > " ^ File.bash_path out_path ^
- " 2> " ^ File.bash_path err_path)
- val out = File.read out_path
- val err = File.read err_path
- val _ = remove_temporary_files ()
- in (rc, out, err) end
- handle exn => (remove_temporary_files (); Exn.reraise exn)
+ \<^try>\<open>
+ let
+ val _ = File.write kki_path kki
+ val rc =
+ Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
+ \\"$KODKODI/bin/kodkodi\"" ^
+ (" -max-msecs " ^ string_of_int timeout) ^
+ (if solve_all then " -solve-all" else "") ^
+ " -max-solutions " ^ string_of_int max_solutions ^
+ (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^
+ " < " ^ File.bash_path kki_path ^
+ " > " ^ File.bash_path out_path ^
+ " 2> " ^ File.bash_path err_path)
+ val out = File.read out_path
+ val err = File.read err_path
+ val _ = remove_temporary_files ()
+ in (rc, out, err) end
+ finally remove_temporary_files ()
+ \<close>
end
else
(timeout, (solve_all, (max_solutions, (max_threads, kki))))