158 val cmd_path = Path.explode cmd_file |
158 val cmd_path = Path.explode cmd_file |
159 val model_dir = File.shell_path (mash_model_dir ()) |
159 val model_dir = File.shell_path (mash_model_dir ()) |
160 val core = |
160 val core = |
161 "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ |
161 "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ |
162 " --numberOfPredictions " ^ string_of_int max_suggs ^ |
162 " --numberOfPredictions " ^ string_of_int max_suggs ^ |
163 (* " --learnTheories" ^ *) (if save then " --saveModel" else "") |
163 (if save then " --saveModel" else "") |
164 val command = |
164 val command = |
165 "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; " ^ |
165 "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; " ^ |
166 "./mash.py --quiet" ^ |
166 "./mash.py --quiet" ^ |
167 " --outputDir " ^ model_dir ^ |
167 " --outputDir " ^ model_dir ^ |
168 " --modelFile=" ^ model_dir ^ "/model.pickle" ^ |
168 " --modelFile=" ^ model_dir ^ "/model.pickle" ^ |
169 " --dictsFile=" ^ model_dir ^ "/dict.pickle" ^ |
169 " --dictsFile=" ^ model_dir ^ "/dict.pickle" ^ |
170 " --theoryFile=" ^ model_dir ^ "/theory.pickle" ^ |
|
171 " --log " ^ log_file ^ " " ^ core ^ |
170 " --log " ^ log_file ^ " " ^ core ^ |
172 " >& " ^ err_file |
171 " >& " ^ err_file |
173 fun run_on () = |
172 fun run_on () = |
174 (Isabelle_System.bash command |
173 (Isabelle_System.bash command |
175 |> tap (fn _ => trace_msg ctxt (fn () => |
174 |> tap (fn _ => trace_msg ctxt (fn () => |
230 fun str_of_query (learns, hints, parents, feats) = |
229 fun str_of_query (learns, hints, parents, feats) = |
231 implode (map str_of_learn learns) ^ |
230 implode (map str_of_learn learns) ^ |
232 "? " ^ encode_strs parents ^ "; " ^ encode_features feats ^ |
231 "? " ^ encode_strs parents ^ "; " ^ encode_features feats ^ |
233 (if null hints then "" else "; " ^ encode_strs hints) ^ "\n" |
232 (if null hints then "" else "; " ^ encode_strs hints) ^ "\n" |
234 |
233 |
235 (* The weights currently returned by "mash.py" are too spaced out to make any |
234 (* The suggested weights don't make much sense. *) |
236 sense. *) |
|
237 fun extract_suggestion sugg = |
235 fun extract_suggestion sugg = |
238 case space_explode "=" sugg of |
236 case space_explode "=" sugg of |
239 [name, _ (* weight *)] => |
237 [name, _ (* weight *)] => |
240 SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *)) |
238 SOME (unencode_str name (* , Real.fromString weight |> the_default 1.0 *)) |
241 | [name] => SOME (unencode_str name (* , 1.0 *)) |
239 | [name] => SOME (unencode_str name (* , 1.0 *)) |