# HG changeset patch # User blanchet # Date 1343980288 -7200 # Node ID 5caa414ce9a24661824f3a5c90168f471f956e51 # Parent 875a4657523ebec8013de5c5165d759043d83efa cleaner temporary file cleanup for MaSh, based on tried-and-trusted code diff -r 875a4657523e -r 5caa414ce9a2 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r 875a4657523e -r 5caa414ce9a2 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 diff -r 875a4657523e -r 5caa414ce9a2 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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 =