--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Aug 02 16:17:52 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Aug 03 09:51:28 2012 +0200
@@ -411,9 +411,7 @@
(*** Low-level communication with MaSh ***)
-(* more friendly than "try o File.rm" for those who keep the files open in their
- text editor *)
-fun wipe_out_file file = File.write (Path.explode file) ""
+fun wipe_out_file file = (try (File.rm o Path.explode) file; ())
fun write_file heading (xs, f) file =
let val path = Path.explode file in
@@ -438,19 +436,24 @@
val command =
mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
" --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
+
+ |> tap (fn _ => trace_msg ctxt (fn () =>
+ case try File.read (Path.explode err_file) of
+ NONE => "Done"
+ | SOME "" => "Done"
+ | SOME s => "Error: " ^ elide_string 1000 s))
+ fun run_on () =
+ (Isabelle_System.bash command;
+ read_suggs (fn () =>
+ try File.read_lines (Path.explode sugg_file) |> these))
+ fun clean_up () =
+ if overlord then ()
+ else List.app wipe_out_file [err_file, sugg_file, cmd_file]
in
write_file "" ([], K "") sugg_file;
write_file "" write_cmds cmd_file;
trace_msg ctxt (fn () => "Running " ^ command);
- Isabelle_System.bash command;
- read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
- |> tap (fn _ => trace_msg ctxt (fn () =>
- case try File.read (Path.explode err_file) of
- NONE => "Done"
- | SOME "" => "Done"
- | SOME s => "Error: " ^ elide_string 1000 s))
- |> not overlord
- ? tap (fn _ => List.app wipe_out_file [err_file, sugg_file, cmd_file])
+ with_cleanup clean_up run_on ()
end
fun str_of_add (name, parents, feats, deps) =
@@ -584,8 +587,7 @@
fun mash_unlearn ctxt =
Synchronized.change global_state (fn _ =>
- (mash_CLEAR ctxt;
- wipe_out_file (mash_state_file ());
+ (mash_CLEAR ctxt; (* also removes the state file *)
(true, empty_state)))
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Aug 02 16:17:52 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Aug 03 09:51:28 2012 +0200
@@ -435,12 +435,6 @@
fun overlord_file_location_for_prover prover =
(getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
-fun with_path cleanup after f path =
- Exn.capture f path
- |> tap (fn _ => cleanup path)
- |> Exn.release
- |> tap (after path)
-
fun proof_banner mode name =
case mode of
Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
@@ -653,7 +647,7 @@
val problem_file_name =
Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
suffix_for_mode mode ^ "_" ^ string_of_int subgoal)
- val problem_path_name =
+ val prob_path =
if dest_dir = "" then
File.tmp_path problem_file_name
else if File.exists (Path.explode dest_dir) then
@@ -687,7 +681,7 @@
val as_time =
raw_explode #> Scan.read Symbol.stopper time #> the_default 0
in (output, as_time t |> Time.fromMilliseconds) end
- fun run_on prob_file =
+ fun run () =
let
(* If slicing is disabled, we expand the last slice to fill the entire
time available. *)
@@ -776,13 +770,13 @@
(ord, ord_info, sel_weights)
val command =
"(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^
- File.shell_path prob_file ^ ")"
+ File.shell_path prob_path ^ ")"
|> enclose "TIMEFORMAT='%3R'; { time " " ; }"
val _ =
atp_problem
|> lines_for_atp_problem format ord ord_info
|> cons ("% " ^ command ^ "\n")
- |> File.write_list prob_file
+ |> File.write_list prob_path
val ((output, run_time), (atp_proof, outcome)) =
TimeLimit.timeLimit generous_slice_timeout
Isabelle_System.bash_output command
@@ -836,17 +830,16 @@
("", Time.zeroTime, [], SOME InternalError))
|> fold maybe_run_slice actual_slices
end
-
(* If the problem file has not been exported, remove it; otherwise, export
the proof file too. *)
- fun cleanup prob_file =
- if dest_dir = "" then try File.rm prob_file else NONE
- fun export prob_file (_, (output, _, _, _)) =
+ fun clean_up () =
+ if dest_dir = "" then (try File.rm prob_path; ()) else ()
+ fun export (_, (output, _, _, _)) =
if dest_dir = "" then ()
- else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
+ else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
val ((_, (_, pool, fact_names, _, sym_tab)),
(output, run_time, atp_proof, outcome)) =
- with_path cleanup export run_on problem_path_name
+ with_cleanup clean_up run () |> tap export
val important_message =
if mode = Normal andalso
random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 02 16:17:52 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Aug 03 09:51:28 2012 +0200
@@ -10,6 +10,7 @@
val plural_s : int -> string
val serial_commas : string -> string list -> string list
val simplify_spaces : string -> string
+ val with_cleanup : ('a -> unit) -> ('a -> 'b) -> 'a -> 'b
val infinite_timeout : Time.time
val time_mult : real -> Time.time -> Time.time
val parse_bool_option : bool -> string -> string -> bool option
@@ -31,6 +32,11 @@
val serial_commas = Try.serial_commas
val simplify_spaces = strip_spaces false (K true)
+fun with_cleanup clean_up f x =
+ Exn.capture f x
+ |> tap (fn _ => clean_up x)
+ |> Exn.release
+
val infinite_timeout = seconds 31536000.0 (* one year *)
fun time_mult k t =