# HG changeset patch # User blanchet # Date 1342815586 -7200 # Node ID 82fc8c956cdc152a9dca932ad39fa97d7be81032 # Parent db3db32c9195bc870fbc3570aac4eec1b5419076 fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully diff -r db3db32c9195 -r 82fc8c956cdc src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 20 22:19:46 2012 +0200 @@ -114,7 +114,7 @@ end fun all_non_tautological_facts_of thy css_table = - Sledgehammer_Fact.all_facts_of thy css_table + Sledgehammer_Fact.all_facts_of (Proof_Context.init_global thy) css_table |> filter_out (Sledgehammer_MaSh.is_likely_tautology_or_too_meta o snd) fun generate_atp_inference_file_for_theory ctxt thy format type_enc file_name = diff -r db3db32c9195 -r 82fc8c956cdc src/HOL/TPTP/mash_eval.ML --- a/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/TPTP/mash_eval.ML Fri Jul 20 22:19:46 2012 +0200 @@ -39,7 +39,7 @@ val path = file_name |> Path.explode val lines = path |> File.read_lines val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_facts_of thy css_table + val facts = all_facts_of (Proof_Context.init_global thy) css_table val all_names = all_names (facts |> map snd) val mepo_ok = Unsynchronized.ref 0 val mash_ok = Unsynchronized.ref 0 diff -r db3db32c9195 -r 82fc8c956cdc src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/TPTP/mash_export.ML Fri Jul 20 22:19:46 2012 +0200 @@ -63,7 +63,7 @@ val _ = File.append path s in [fact] end val thy_map = - all_facts_of thy Termtab.empty + all_facts_of (Proof_Context.init_global thy) Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) |> thy_map_from_facts fun do_thy facts = @@ -79,7 +79,7 @@ val _ = File.write path "" val css_table = clasimpset_rule_table_of ctxt val facts = - all_facts_of thy css_table + all_facts_of (Proof_Context.init_global thy) css_table |> not include_thy ? filter_out (has_thy thy o snd) fun do_fact ((_, stature), th) = let @@ -95,7 +95,7 @@ val path = file_name |> Path.explode val _ = File.write path "" val ths = - all_facts_of thy Termtab.empty + all_facts_of (Proof_Context.init_global thy) Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) |> map snd val all_names = all_names ths @@ -114,7 +114,7 @@ val _ = File.write path "" val prover = hd provers val facts = - all_facts_of thy Termtab.empty + all_facts_of (Proof_Context.init_global thy) Termtab.empty |> not include_thy ? filter_out (has_thy thy o snd) val ths = facts |> map snd val all_names = all_names ths @@ -132,7 +132,7 @@ val path = file_name |> Path.explode val _ = File.write path "" val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_facts_of thy css_table + val facts = all_facts_of (Proof_Context.init_global thy) css_table val (new_facts, old_facts) = facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) @@ -162,7 +162,7 @@ val _ = File.write path "" val prover = hd provers val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_facts_of thy css_table + val facts = all_facts_of (Proof_Context.init_global thy) css_table val (new_facts, old_facts) = facts |> List.partition (has_thy thy o snd) |>> sort (thm_ord o pairself snd) diff -r db3db32c9195 -r 82fc8c956cdc src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 20 22:19:46 2012 +0200 @@ -23,12 +23,13 @@ val fact_from_ref : Proof.context -> unit Symtab.table -> thm list -> status Termtab.table -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list + val backquote_thm : thm -> string val clasimpset_rule_table_of : Proof.context -> status Termtab.table val maybe_instantiate_inducts : Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list - val all_facts_of : theory -> status Termtab.table -> fact list + val all_facts_of : Proof.context -> status Termtab.table -> fact list val nearly_all_facts : Proof.context -> bool -> fact_override -> unit Symtab.table -> status Termtab.table -> thm list -> term list -> term -> fact list @@ -212,9 +213,9 @@ is_that_fact thm end -fun hackish_string_for_term ctxt t = +fun hackish_string_for_term thy t = Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) - (print_mode_value ())) (Syntax.string_of_term ctxt) t + (print_mode_value ())) (Syntax.string_of_term_global thy) t |> String.translate (fn c => if Char.isPrint c then str c else "") |> simplify_spaces @@ -240,6 +241,11 @@ (Term.add_vars t [] |> sort_wrt (fst o fst)) |> fst +fun backquote_thm th = + th |> prop_of |> close_form + |> hackish_string_for_term (theory_of_thm th) + |> backquote + fun clasimpset_rule_table_of ctxt = let val thy = Proof_Context.theory_of ctxt @@ -302,13 +308,14 @@ fun instantiate_induct_rule ctxt concl_prop p_name ((name, stature), th) ind_x = let + val thy = Proof_Context.theory_of ctxt fun varify_noninducts (t as Free (s, T)) = if (s, T) = ind_x orelse can dest_funT T then t else Var ((s, 0), T) | varify_noninducts t = t val p_inst = concl_prop |> map_aterms varify_noninducts |> close_form |> lambda (Free ind_x) - |> hackish_string_for_term ctxt + |> hackish_string_for_term thy in ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)]) @@ -374,8 +381,6 @@ else let val multi = length ths > 1 - val backquote_thm = - backquote o hackish_string_for_term ctxt o close_form o prop_of fun check_thms a = case try (Proof_Context.get_thms ctxt) a of NONE => false @@ -392,7 +397,7 @@ val new = (((fn () => if name0 = "" then - th |> backquote_thm + backquote_thm th else [Facts.extern ctxt facts name0, Name_Space.extern ctxt full_space name0] @@ -415,11 +420,9 @@ |> op @ end -fun all_facts_of thy css_table = - let val ctxt = Proof_Context.init_global thy in - all_facts ctxt false Symtab.empty [] [] css_table - |> rev (* try to restore the original order of facts, for MaSh *) - end +fun all_facts_of ctxt css_table = + all_facts ctxt false Symtab.empty [] [] css_table + |> rev (* try to restore the original order of facts, for MaSh *) fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css_table chained_ths hyp_ts concl_t = diff -r db3db32c9195 -r 82fc8c956cdc src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 20 22:19:46 2012 +0200 @@ -101,9 +101,10 @@ val relearn_atpN = "relearn_atp" fun mash_home () = getenv "MASH_HOME" -fun mash_state_dir () = +fun mash_model_dir () = getenv "ISABELLE_HOME_USER" ^ "/mash" |> tap (Isabelle_System.mkdir o Path.explode) +val mash_state_dir = mash_model_dir fun mash_state_path () = mash_state_dir () ^ "/state" |> Path.explode @@ -115,14 +116,14 @@ String.str c else (* fixed width, in case more digits follow *) - "\\" ^ stringN_of_int 3 (Char.ord c) + "$" ^ stringN_of_int 3 (Char.ord c) fun unmeta_chars accum [] = String.implode (rev accum) - | unmeta_chars accum (#"\\" :: d1 :: d2 :: d3 :: cs) = + | unmeta_chars accum (#"$" :: d1 :: d2 :: d3 :: cs) = (case Int.fromString (String.implode [d1, d2, d3]) of SOME n => unmeta_chars (Char.chr n :: accum) cs | NONE => "" (* error *)) - | unmeta_chars _ (#"\\" :: _) = "" (* error *) + | unmeta_chars _ (#"$" :: _) = "" (* error *) | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs val escape_meta = String.translate meta_char @@ -149,13 +150,16 @@ val local_prefix = "local" ^ Long_Name.separator fun nickname_of th = - let val hint = Thm.get_name_hint th in - (* FIXME: There must be a better way to detect local facts. *) - case try (unprefix local_prefix) hint of - SOME suff => - parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suff - | NONE => hint - end + if Thm.has_name_hint th then + let val hint = Thm.get_name_hint th in + (* FIXME: There must be a better way to detect local facts. *) + case try (unprefix local_prefix) hint of + SOME suf => + parent_of_local_thm th ^ Long_Name.separator ^ Long_Name.separator ^ suf + | NONE => hint + end + else + backquote_thm th fun suggested_facts suggs facts = let @@ -369,56 +373,47 @@ (*** 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.write file "" + fun write_file (xs, f) file = let val path = Path.explode file in - File.write path ""; + wipe_out path; xs |> chunk_list 500 |> List.app (File.append path o space_implode "" o map f) end -fun mash_info overlord = - if overlord then (getenv "ISABELLE_HOME_USER", "") - else (getenv "ISABELLE_TMP", serial_string ()) - -fun and_rm_files overlord flags files = - if overlord then - "" - else - " && rm -f" ^ flags ^ " -- " ^ - space_implode " " (map File.shell_quote files) - -fun run_mash ctxt overlord (temp_dir, serial) async core = +fun run_mash_tool ctxt overlord save max_suggs write_cmds read_suggs = let - val log_file = temp_dir ^ "/mash_log" ^ serial + val (temp_dir, serial) = + if overlord then (getenv "ISABELLE_HOME_USER", "") + else (getenv "ISABELLE_TMP", serial_string ()) + val log_file = if overlord then temp_dir ^ "/mash_log" else "/dev/null" val err_file = temp_dir ^ "/mash_err" ^ serial - val command = - "(" ^ mash_home () ^ "/mash --quiet --outputDir " ^ mash_state_dir () ^ - " --log " ^ log_file ^ " " ^ core ^ ") 2>&1 > " ^ err_file ^ - and_rm_files overlord "" [log_file, err_file] ^ - (if async then " &" else "") - in - trace_msg ctxt (fn () => - (if async then "Launching " else "Running ") ^ command); - write_file ([], K "") log_file; - write_file ([], K "") err_file; - Isabelle_System.bash command; - if not async then trace_msg ctxt (K "Done") else () - end - -fun run_mash_commands ctxt overlord save max_suggs write_cmds read_suggs = - let - val info as (temp_dir, serial) = mash_info overlord val sugg_file = temp_dir ^ "/mash_suggs" ^ serial val cmd_file = temp_dir ^ "/mash_commands" ^ serial + val core = + "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ + " --numberOfPredictions " ^ string_of_int max_suggs ^ + (if save then " --saveModel" else "") + val command = + mash_home () ^ "/mash --quiet --outputDir " ^ mash_model_dir () ^ + " --log " ^ log_file ^ " " ^ core ^ " >& " ^ err_file in write_file ([], K "") sugg_file; write_file write_cmds cmd_file; - run_mash ctxt overlord info false - ("--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file ^ - " --numberOfPredictions " ^ string_of_int max_suggs ^ - (if save then " --saveModel" else "") ^ - (and_rm_files overlord "" [sugg_file, cmd_file])); - read_suggs (fn () => File.read_lines (Path.explode sugg_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 o Path.explode) + [err_file, sugg_file, cmd_file]) end fun str_of_update (name, parents, feats, deps) = @@ -429,24 +424,28 @@ "? " ^ escape_metas parents ^ "; " ^ escape_metas feats fun mash_CLEAR ctxt = - let val path = mash_state_dir () |> Path.explode in + let val path = mash_model_dir () |> Path.explode in trace_msg ctxt (K "MaSh CLEAR"); - File.fold_dir (fn file => fn () => - File.rm (Path.append path (Path.basic file))) - path () + File.fold_dir (fn file => fn _ => + try File.rm (Path.append path (Path.basic file))) + path NONE; + () end fun mash_ADD _ _ [] = () | mash_ADD ctxt overlord upds = (trace_msg ctxt (fn () => "MaSh ADD " ^ elide_string 1000 (space_implode " " (map #1 upds))); - run_mash_commands ctxt overlord true 0 (upds, str_of_update) (K ())) + run_mash_tool ctxt overlord true 0 (upds, str_of_update) (K ())) fun mash_QUERY ctxt overlord max_suggs (query as (_, feats)) = (trace_msg ctxt (fn () => "MaSh QUERY " ^ space_implode " " feats); - run_mash_commands ctxt overlord false max_suggs + run_mash_tool ctxt overlord false max_suggs ([query], str_of_query) - (fn suggs => snd (extract_query (List.last (suggs ())))) + (fn suggs => + case suggs () of + [] => [] + | suggs => snd (extract_query (List.last suggs))) handle List.Empty => []) @@ -529,8 +528,7 @@ fun mash_unlearn ctxt = Synchronized.change global_state (fn _ => - (mash_CLEAR ctxt; File.write (mash_state_path ()) ""; - (true, empty_state))) + (mash_CLEAR ctxt; wipe_out (mash_state_path ()); (true, empty_state))) end @@ -642,16 +640,20 @@ |> sort (thm_ord o pairself snd) val num_new_facts = length new_facts in - "MaShing" ^ (if not auto then - " " ^ string_of_int num_new_facts ^ " fact" ^ - plural_s num_new_facts ^ - (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")" else "") + "MaShing" ^ + (if not auto then + " " ^ string_of_int num_new_facts ^ " fact" ^ + plural_s num_new_facts ^ + (if atp then " (ATP timeout: " ^ string_from_time timeout ^ ")" + else "") + else + "") ^ "..." else - "") ^ "..." + "") |> Output.urgent_message; if null new_facts then - if verbose orelse not auto then + if not auto then "Nothing to learn.\n\nHint: Try " ^ sendback relearn_isarN ^ " or " ^ sendback relearn_atpN ^ " to learn from scratch." else @@ -694,6 +696,7 @@ (if atp then atp_dependencies_of ctxt params prover auto facts else isar_dependencies_of) all_names th |> trim_deps + val n = n |> not (null deps) ? Integer.add 1 val upds = (name, parents, feats, deps) :: upds val (upds, next_commit) = if Time.> (Timer.checkRealTimer timer, next_commit) then @@ -702,7 +705,7 @@ (upds, next_commit) val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) - in (upds, ([name], n + 1, next_commit, timed_out)) end + in (upds, ([name], n, next_commit, timed_out)) end val parents = parents_wrt_facts facts fact_graph val (upds, (_, n, _, _)) = ([], (parents, 0, next_commit_time (), false)) @@ -710,7 +713,7 @@ in commit true upds; if verbose orelse not auto then - "Learned " ^ string_of_int n ^ " proof" ^ plural_s n ^ + "Learned " ^ string_of_int n ^ " nontrivial proof" ^ plural_s n ^ (if verbose then " in " ^ string_from_time (Timer.checkRealTimer timer) else @@ -722,9 +725,8 @@ fun mash_learn ctxt (params as {provers, ...}) atp = let - val thy = Proof_Context.theory_of ctxt val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt - val facts = all_facts_of thy css_table + val facts = all_facts_of ctxt css_table in mash_learn_facts ctxt params (hd provers) false atp infinite_timeout facts |> Output.urgent_message diff -r db3db32c9195 -r 82fc8c956cdc src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200 @@ -256,7 +256,7 @@ end fun maybe_minimize ctxt mode do_learn name - (params as {debug, verbose, isar_proof, minimize, ...}) + (params as {verbose, isar_proof, minimize, ...}) ({state, subgoal, subgoal_count, facts, ...} : prover_problem) (result as {outcome, used_facts, run_time, preplay, message, message_tail} : prover_result) = @@ -310,19 +310,8 @@ in case used_facts of SOME used_facts => - (if debug andalso not (null used_facts) then - tag_list 1 facts - |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j)) - |> filter_used_facts used_facts - |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) - |> commas - |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ - " proof (of " ^ string_of_int (length facts) ^ "): ") "." - |> Output.urgent_message - else - (); - {outcome = NONE, used_facts = used_facts, run_time = run_time, - preplay = preplay, message = message, message_tail = message_tail}) + {outcome = NONE, used_facts = used_facts, run_time = run_time, + preplay = preplay, message = message, message_tail = message_tail} | NONE => result end diff -r db3db32c9195 -r 82fc8c956cdc src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jul 20 22:19:46 2012 +0200 @@ -84,12 +84,24 @@ ? filter_out (curry (op =) Induction o snd o snd o fst o untranslated_fact) |> take num_facts} + fun print_used_facts used_facts = + tag_list 1 facts + |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j)) + |> filter_used_facts used_facts + |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) + |> commas + |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^ + " proof (of " ^ string_of_int (length facts) ^ "): ") "." + |> Output.urgent_message fun really_go () = problem |> get_minimizing_prover ctxt mode (mash_learn_proof ctxt params name (prop_of goal) (map untranslated_fact facts)) name params minimize_command + |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} => + print_used_facts used_facts + | _ => ()) |> (fn {outcome, preplay, message, message_tail, ...} => (if outcome = SOME ATP_Proof.TimedOut then timeoutN else if is_some outcome then noneN @@ -228,7 +240,7 @@ hyp_ts concl_t |> map (apfst (apfst (fn name => name ()))) |> tap (fn facts => - if debug then + if verbose then label ^ plural_s (length provers) ^ ": " ^ (if null facts then "Found no relevant facts."