1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200
1.3 @@ -101,9 +101,10 @@
1.4 val relearn_atpN = "relearn_atp"
1.5
1.6 fun mash_home () = getenv "MASH_HOME"
1.7 -fun mash_state_dir () =
1.8 +fun mash_model_dir () =
1.9 getenv "ISABELLE_HOME_USER" ^ "/mash"
1.10 |> tap (Isabelle_System.mkdir o Path.explode)
1.11 +val mash_state_dir = mash_model_dir
1.12 fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode
1.13
1.14
1.15 @@ -115,14 +116,14 @@
1.16 String.str c
1.17 else
1.18 (* fixed width, in case more digits follow *)
1.19 - "\\" ^ stringN_of_int 3 (Char.ord c)
1.20 + "$" ^ stringN_of_int 3 (Char.ord c)
1.21
1.22 fun unmeta_chars accum [] = String.implode (rev accum)
1.23 - | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) =
1.24 + | unmeta_chars accum (#"$" :: d1 :: d2 :: d3 :: cs) =
1.25 (case Int.fromString (String.implode [d1, d2, d3]) of
1.26 SOME n => unmeta_chars (Char.chr n :: accum) cs
1.27 | NONE => "" (* error *))
1.28 - | unmeta_chars _ (#"\\" :: _) = "" (* error *)
1.29 + | unmeta_chars _ (#"$" :: _) = "" (* error *)
1.30 | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
1.31
1.32 val escape_meta = String.translate meta_char
1.33 @@ -149,13 +150,16 @@
1.34 val local_prefix = "local" ^ Long_Name.separator
1.35
1.36 fun nickname_of th =
1.37 - let val hint = Thm.get_name_hint th in
1.38 - (* FIXME: There must be a better way to detect local facts. *)
1.39 - case try (unprefix local_prefix) hint of
1.40 - SOME suff =>
1.41 - parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff
1.42 - | NONE => hint
1.43 - end
1.44 + if Thm.has_name_hint th then
1.45 + let val hint = Thm.get_name_hint th in
1.46 + (* FIXME: There must be a better way to detect local facts. *)
1.47 + case try (unprefix local_prefix) hint of
1.48 + SOME suf =>
1.49 + parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf
1.50 + | NONE => hint
1.51 + end
1.52 + else
1.53 + backquote_thm th
1.54
1.55 fun suggested_facts suggs facts =
1.56 let
1.57 @@ -369,56 +373,47 @@
1.58
1.59 (*** Low-level communication with MaSh ***)
1.60
1.61 +(* more friendly than "try o File.rm" for those who keep the files open in their
1.62 + text editor *)
1.63 +fun wipe_out file = File.write file ""
1.64 +
1.65 fun write_file (xs, f) file =
1.66 let val path = Path.explode file in
1.67 - File.write path "";
1.68 + wipe_out path;
1.69 xs |> chunk_list 500
1.70 |> List.app (File.append path o space_implode "" o map f)
1.71 end
1.72
1.73 -fun mash_info overlord =
1.74 - if overlord then (getenv "ISABELLE_HOME_USER", "")
1.75 - else (getenv "ISABELLE_TMP", serial_string ())
1.76 -
1.77 -fun and_rm_files overlord flags files =
1.78 - if overlord then
1.79 - ""
1.80 - else
1.81 - " && rm -f" ^ flags ^ " -- " ^
1.82 - space_implode " " (map File.shell_quote files)
1.83 -
1.84 -fun run_mash ctxt overlord (temp_dir, serial) async core =
1.85 +fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs =
1.86 let
1.87 - val log_file = temp_dir ^ "/mash_log" ^ serial
1.88 + val (temp_dir, serial) =
1.89 + if overlord then (getenv "ISABELLE_HOME_USER", "")
1.90 + else (getenv "ISABELLE_TMP", serial_string ())
1.91 + val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null"
1.92 val err_file = temp_dir ^ "/mash_err" ^ serial
1.93 - val command =
1.94 - "(" ^ mash_home () ^ "/mash --quiet --outputDir " ^ mash_state_dir () ^
1.95 - " --log " ^ log_file ^ " " ^ core ^ ") 2>&1 > " ^ err_file ^
1.96 - and_rm_files overlord "" [log_file, err_file] ^
1.97 - (if async then " &" else "")
1.98 - in
1.99 - trace_msg ctxt (fn () =>
1.100 - (if async then "Launching " else "Running ") ^ command);
1.101 - write_file ([], K "") log_file;
1.102 - write_file ([], K "") err_file;
1.103 - Isabelle_System.bash command;
1.104 - if not async then trace_msg ctxt (K "Done") else ()
1.105 - end
1.106 -
1.107 -fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs =
1.108 - let
1.109 - val info as (temp_dir, serial) = mash_info overlord
1.110 val sugg_file = temp_dir ^ "/mash_suggs" ^ serial
1.111 val cmd_file = temp_dir ^ "/mash_commands" ^ serial
1.112 + val core =
1.113 + "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
1.114 + " --numberOfPredictions " ^ string_of_int max_suggs ^
1.115 + (if save then " --saveModel" else "")
1.116 + val command =
1.117 + mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^
1.118 + " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file
1.119 in
1.120 write_file ([], K "") sugg_file;
1.121 write_file write_cmds cmd_file;
1.122 - run_mash ctxt overlord info false
1.123 - ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^
1.124 - " --numberOfPredictions " ^ string_of_int max_suggs ^
1.125 - (if save then " --saveModel" else "") ^
1.126 - (and_rm_files overlord "" [sugg_file, cmd_file]));
1.127 - read_suggs (fn () => File.read_lines (Path.explode sugg_file))
1.128 + trace_msg ctxt (fn () => "Running " ^ command);
1.129 + Isabelle_System.bash command;
1.130 + read_suggs (fn () => try File.read_lines (Path.explode sugg_file) |> these)
1.131 + |> tap (fn _ => trace_msg ctxt (fn () =>
1.132 + case try File.read (Path.explode err_file) of
1.133 + NONE => "Done"
1.134 + | SOME "" => "Done"
1.135 + | SOME s => "Error: " ^ elide_string 1000 s))
1.136 + |> not overlord
1.137 + ? tap (fn _ => List.app (wipe_out o Path.explode)
1.138 + [err_file, sugg_file, cmd_file])
1.139 end
1.140
1.141 fun str_of_update (name, parents, feats, deps) =
1.142 @@ -429,24 +424,28 @@
1.143 "? " ^ escape_metas parents ^ "; " ^ escape_metas feats
1.144
1.145 fun mash_CLEAR ctxt =
1.146 - let val path = mash_state_dir () |> Path.explode in
1.147 + let val path = mash_model_dir () |> Path.explode in
1.148 trace_msg ctxt (K "MaSh CLEAR");
1.149 - File.fold_dir (fn file => fn () =>
1.150 - File.rm (Path.append path (Path.basic file)))
1.151 - path ()
1.152 + File.fold_dir (fn file => fn _ =>
1.153 + try File.rm (Path.append path (Path.basic file)))
1.154 + path NONE;
1.155 + ()
1.156 end
1.157
1.158 fun mash_ADD _ _ [] = ()
1.159 | mash_ADD ctxt overlord upds =
1.160 (trace_msg ctxt (fn () => "MaSh ADD " ^
1.161 elide_string 1000 (space_implode " " (map #1 upds)));
1.162 - run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ()))
1.163 + run_mash_tool ctxt overlord true 0 (upds, str_of_update) (K ()))
1.164
1.165 fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) =
1.166 (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats);
1.167 - run_mash_commands ctxt overlord false max_suggs
1.168 + run_mash_tool ctxt overlord false max_suggs
1.169 ([query], str_of_query)
1.170 - (fn suggs => snd (extract_query (List.last (suggs ()))))
1.171 + (fn suggs =>
1.172 + case suggs () of
1.173 + [] => []
1.174 + | suggs => snd (extract_query (List.last suggs)))
1.175 handle List.Empty => [])
1.176
1.177
1.178 @@ -529,8 +528,7 @@
1.179
1.180 fun mash_unlearn ctxt =
1.181 Synchronized.change global_state (fn _ =>
1.182 - (mash_CLEAR ctxt; File.write (mash_state_path ()) "";
1.183 - (true, empty_state)))
1.184 + (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state)))
1.185
1.186 end
1.187
1.188 @@ -642,16 +640,20 @@
1.189 |> sort (thm_ord o pairself snd)
1.190 val num_new_facts = length new_facts
1.191 in
1.192 - "MaShing" ^
1.193 (if not auto then
1.194 - " " ^ string_of_int num_new_facts ^ " fact" ^
1.195 - plural_s num_new_facts ^
1.196 - (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")" else "")
1.197 + "MaShing" ^
1.198 + (if not auto then
1.199 + " " ^ string_of_int num_new_facts ^ " fact" ^
1.200 + plural_s num_new_facts ^
1.201 + (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")"
1.202 + else "")
1.203 + else
1.204 + "") ^ "..."
1.205 else
1.206 - "") ^ "..."
1.207 + "")
1.208 |> Output.urgent_message;
1.209 if null new_facts then
1.210 - if verbose orelse not auto then
1.211 + if not auto then
1.212 "Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^
1.213 sendback relearn_atpN ^ " to learn from scratch."
1.214 else
1.215 @@ -694,6 +696,7 @@
1.216 (if atp then atp_dependencies_of ctxt params prover auto facts
1.217 else isar_dependencies_of) all_names th
1.218 |> trim_deps
1.219 + val n = n |> not (null deps) ? Integer.add 1
1.220 val upds = (name, parents, feats, deps) :: upds
1.221 val (upds, next_commit) =
1.222 if Time.> (Timer.checkRealTimer timer, next_commit) then
1.223 @@ -702,7 +705,7 @@
1.224 (upds, next_commit)
1.225 val timed_out =
1.226 Time.> (Timer.checkRealTimer timer, learn_timeout)
1.227 - in (upds, ([name], n + 1, next_commit, timed_out)) end
1.228 + in (upds, ([name], n, next_commit, timed_out)) end
1.229 val parents = parents_wrt_facts facts fact_graph
1.230 val (upds, (_, n, _, _)) =
1.231 ([], (parents, 0, next_commit_time (), false))
1.232 @@ -710,7 +713,7 @@
1.233 in
1.234 commit true upds;
1.235 if verbose orelse not auto then
1.236 - "Learned " ^ string_of_int n ^ " proof" ^ plural_s n ^
1.237 + "Learned " ^ string_of_int n ^ " nontrivial proof" ^ plural_s n ^
1.238 (if verbose then
1.239 " in " ^ string_from_time (Timer.checkRealTimer timer)
1.240 else
1.241 @@ -722,9 +725,8 @@
1.242
1.243 fun mash_learn ctxt (params as {provers, ...}) atp =
1.244 let
1.245 - val thy = Proof_Context.theory_of ctxt
1.246 val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
1.247 - val facts = all_facts_of thy css_table
1.248 + val facts = all_facts_of ctxt css_table
1.249 in
1.250 mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts
1.251 |> Output.urgent_message