# HG changeset patch # User blanchet # Date 1355268246 -3600 # Node ID 8ec31bdb9d36bd5d7a1210301953b81914a0d01e # Parent da63f2bc66b37ec782a384078d2d0c3f5a02d5db adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers) diff -r da63f2bc66b3 -r 8ec31bdb9d36 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Wed Dec 12 00:14:58 2012 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Wed Dec 12 00:24:06 2012 +0100 @@ -694,9 +694,9 @@ proofs. This happens automatically at Sledgehammer invocations if the \textit{learn} option (\S\ref{relevance-filter}) is enabled. -\item[\labelitemi] \textbf{\textit{learn\_atp}:} Invokes MaSh on the current -theory to process all the available facts, learning from ATP-generated proofs. -The ATP to use and its timeout can be set using the +\item[\labelitemi] \textbf{\textit{learn\_prover}:} Invokes MaSh on the current +theory to process all the available facts, learning from proofs generated by +automatic provers. The prover to use and its timeout can be set using the \textit{prover} (\S\ref{mode-of-operation}) and \textit{timeout} (\S\ref{timeouts}) options. It is recommended to perform learning using an efficient first-order ATP (such as E, SPASS, and Vampire) as opposed to a @@ -705,8 +705,8 @@ \item[\labelitemi] \textbf{\textit{relearn\_isar}:} Same as \textit{unlearn} followed by \textit{learn\_isar}. -\item[\labelitemi] \textbf{\textit{relearn\_atp}:} Same as \textit{unlearn} -followed by \textit{learn\_atp}. +\item[\labelitemi] \textbf{\textit{relearn\_prover}:} Same as \textit{unlearn} +followed by \textit{learn\_prover}. \item[\labelitemi] \textbf{\textit{running\_learners}:} Prints information about currently running machine learners, including elapsed runtime and remaining @@ -719,8 +719,8 @@ Sledgehammer's behavior can be influenced by various \qty{options}, which can be specified in brackets after the \textbf{sledgehammer} command. The \qty{options} are a list of key--value pairs of the form ``[$k_1 = v_1, -\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. For -example: +\ldots, k_n = v_n$]''. For Boolean options, ``= \textit{true\/}'' is optional. +For example: \prew \textbf{sledgehammer} [\textit{isar\_proofs}, \,\textit{timeout} = 120] diff -r da63f2bc66b3 -r 8ec31bdb9d36 src/HOL/TPTP/MaSh_Eval.thy --- a/src/HOL/TPTP/MaSh_Eval.thy Wed Dec 12 00:14:58 2012 +0100 +++ b/src/HOL/TPTP/MaSh_Eval.thy Wed Dec 12 00:24:06 2012 +0100 @@ -17,7 +17,7 @@ declare [[sledgehammer_instantiate_inducts]] ML {* -! Multithreading.max_threads +!Multithreading.max_threads *} ML {* diff -r da63f2bc66b3 -r 8ec31bdb9d36 src/HOL/TPTP/MaSh_Export.thy --- a/src/HOL/TPTP/MaSh_Export.thy Wed Dec 12 00:14:58 2012 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Wed Dec 12 00:24:06 2012 +0100 @@ -52,7 +52,8 @@ ML {* if do_it then - generate_isar_dependencies @{context} thys false (prefix ^ "mash_dependencies") + generate_isar_dependencies @{context} thys false + (prefix ^ "mash_dependencies") else () *} @@ -66,21 +67,24 @@ ML {* if do_it then - generate_mepo_suggestions @{context} params thys 1024 (prefix ^ "mash_mepo_suggestions") + generate_mepo_suggestions @{context} params thys 1024 + (prefix ^ "mash_mepo_suggestions") else () *} ML {* if do_it then - generate_atp_dependencies @{context} params thys false (prefix ^ "mash_atp_dependencies") + generate_prover_dependencies @{context} params thys false + (prefix ^ "mash_prover_dependencies") else () *} ML {* if do_it then - generate_atp_commands @{context} params thys (prefix ^ "mash_atp_commands") + generate_prover_commands @{context} params thys + (prefix ^ "mash_prover_commands") else () *} diff -r da63f2bc66b3 -r 8ec31bdb9d36 src/HOL/TPTP/mash_export.ML --- a/src/HOL/TPTP/mash_export.ML Wed Dec 12 00:14:58 2012 +0100 +++ b/src/HOL/TPTP/mash_export.ML Wed Dec 12 00:24:06 2012 +0100 @@ -15,11 +15,11 @@ Proof.context -> string -> theory list -> bool -> string -> unit val generate_isar_dependencies : Proof.context -> theory list -> bool -> string -> unit - val generate_atp_dependencies : + val generate_prover_dependencies : Proof.context -> params -> theory list -> bool -> string -> unit val generate_isar_commands : Proof.context -> string -> theory list -> string -> unit - val generate_atp_commands : + val generate_prover_commands : Proof.context -> params -> theory list -> string -> unit val generate_mepo_suggestions : Proof.context -> params -> theory list -> int -> string -> unit @@ -97,15 +97,15 @@ in File.append path s end in List.app do_fact facts end -fun isar_or_atp_dependencies_of ctxt params_opt facts all_names th = +fun isar_or_prover_dependencies_of ctxt params_opt facts all_names th = (case params_opt of SOME (params as {provers = prover :: _, ...}) => - atp_dependencies_of ctxt params prover 0 facts all_names th |> snd + prover_dependencies_of ctxt params prover 0 facts all_names th |> snd | NONE => isar_dependencies_of all_names th) |> these -fun generate_isar_or_atp_dependencies ctxt params_opt thys include_thys - file_name = +fun generate_isar_or_prover_dependencies ctxt params_opt thys include_thys + file_name = let val path = file_name |> Path.explode val _ = File.write path "" @@ -118,18 +118,18 @@ let val name = nickname_of th val deps = - isar_or_atp_dependencies_of ctxt params_opt facts all_names th + isar_or_prover_dependencies_of ctxt params_opt facts all_names th val s = escape_meta name ^ ": " ^ escape_metas deps ^ "\n" in File.append path s end in List.app do_thm ths end fun generate_isar_dependencies ctxt = - generate_isar_or_atp_dependencies ctxt NONE + generate_isar_or_prover_dependencies ctxt NONE -fun generate_atp_dependencies ctxt params = - generate_isar_or_atp_dependencies ctxt (SOME params) +fun generate_prover_dependencies ctxt params = + generate_isar_or_prover_dependencies ctxt (SOME params) -fun generate_isar_or_atp_commands ctxt prover params_opt thys file_name = +fun generate_isar_or_prover_commands ctxt prover params_opt thys file_name = let val path = file_name |> Path.explode val _ = File.write path "" @@ -144,7 +144,7 @@ val feats = features_of ctxt prover (theory_of_thm th) stature [prop_of th] val deps = - isar_or_atp_dependencies_of ctxt params_opt facts all_names th + isar_or_prover_dependencies_of ctxt params_opt facts all_names th val kind = Thm.legacy_get_kind th val core = escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^ @@ -159,10 +159,10 @@ in fold do_fact new_facts parents; () end fun generate_isar_commands ctxt prover = - generate_isar_or_atp_commands ctxt prover NONE + generate_isar_or_prover_commands ctxt prover NONE -fun generate_atp_commands ctxt (params as {provers = prover :: _, ...}) = - generate_isar_or_atp_commands ctxt prover (SOME params) +fun generate_prover_commands ctxt (params as {provers = prover :: _, ...}) = + generate_isar_or_prover_commands ctxt prover (SOME params) fun generate_mepo_suggestions ctxt (params as {provers, ...}) thys max_relevant file_name = diff -r da63f2bc66b3 -r 8ec31bdb9d36 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Dec 12 00:14:58 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Dec 12 00:24:06 2012 +0100 @@ -367,7 +367,7 @@ (if i = 1 then "" else " " ^ string_of_int i) end -val default_learn_atp_timeout = 0.5 +val default_learn_prover_timeout = 0.5 fun hammer_away override_params subcommand opt_i fact_override state = let @@ -404,21 +404,22 @@ running_provers () else if subcommand = unlearnN then mash_unlearn ctxt - else if subcommand = learn_isarN orelse subcommand = learn_atpN orelse - subcommand = relearn_isarN orelse subcommand = relearn_atpN then - (if subcommand = relearn_isarN orelse subcommand = relearn_atpN then + else if subcommand = learn_isarN orelse subcommand = learn_proverN orelse + subcommand = relearn_isarN orelse subcommand = relearn_proverN then + (if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt else (); - mash_learn ctxt (get_params Normal ctxt - ([("timeout", - [string_of_real default_learn_atp_timeout]), - ("slice", ["false"])] @ - override_params @ - [("minimize", ["true"]), - ("preplay_timeout", ["0"])])) - fact_override (#facts (Proof.goal state)) - (subcommand = learn_atpN orelse subcommand = relearn_atpN)) + mash_learn ctxt + (get_params Normal ctxt + ([("timeout", + [string_of_real default_learn_prover_timeout]), + ("slice", ["false"])] @ + override_params @ + [("minimize", ["true"]), + ("preplay_timeout", ["0"])])) + fact_override (#facts (Proof.goal state)) + (subcommand = learn_proverN orelse subcommand = relearn_proverN)) else if subcommand = running_learnersN then running_learners () else if subcommand = refresh_tptpN then diff -r da63f2bc66b3 -r 8ec31bdb9d36 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Dec 12 00:14:58 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Dec 12 00:24:06 2012 +0100 @@ -20,9 +20,9 @@ val meshN : string val unlearnN : string val learn_isarN : string - val learn_atpN : string + val learn_proverN : string val relearn_isarN : string - val relearn_atpN : string + val relearn_proverN : string val fact_filters : string list val escape_meta : string -> string val escape_metas : string list -> string @@ -55,7 +55,7 @@ Proof.context -> string -> theory -> stature -> term list -> (string * real) list val isar_dependencies_of : unit Symtab.table -> thm -> string list option - val atp_dependencies_of : + val prover_dependencies_of : Proof.context -> params -> string -> int -> fact list -> unit Symtab.table -> thm -> bool * string list option val weight_mash_facts : ('a * thm) list -> (('a * thm) * real) list @@ -105,9 +105,9 @@ val unlearnN = "unlearn" val learn_isarN = "learn_isar" -val learn_atpN = "learn_atp" +val learn_proverN = "learn_prover" val relearn_isarN = "relearn_isar" -val relearn_atpN = "relearn_atp" +val relearn_proverN = "relearn_prover" fun mash_model_dir () = Path.explode "$ISABELLE_HOME_USER/mash" |> tap Isabelle_System.mkdir @@ -248,15 +248,16 @@ (*** Middle-level communication with MaSh ***) -datatype proof_kind = Isar_Proof | ATP_Proof | Isar_Proof_wegen_ATP_Flop +datatype proof_kind = + Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop fun str_of_proof_kind Isar_Proof = "i" - | str_of_proof_kind ATP_Proof = "a" - | str_of_proof_kind Isar_Proof_wegen_ATP_Flop = "x" + | str_of_proof_kind Automatic_Proof = "a" + | str_of_proof_kind Isar_Proof_wegen_Prover_Flop = "x" fun proof_kind_of_str "i" = Isar_Proof - | proof_kind_of_str "a" = ATP_Proof - | proof_kind_of_str "x" = Isar_Proof_wegen_ATP_Flop + | proof_kind_of_str "a" = Automatic_Proof + | proof_kind_of_str "x" = Isar_Proof_wegen_Prover_Flop (* FIXME: Here a "Graph.update_node" function would be useful *) fun update_fact_graph_node (name, kind) = @@ -596,7 +597,8 @@ (* Too many dependencies is a sign that a decision procedure is at work. There isn't much to learn from such proofs. *) val max_dependencies = 20 -val atp_dependency_default_max_facts = 50 + +val prover_dependency_default_max_facts = 50 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *) val typedef_deps = [@{thm CollectI} |> nickname_of] @@ -634,8 +636,8 @@ fun isar_dependencies_of all_names th = th |> thms_in_proof (SOME all_names) |> trim_dependencies th -fun atp_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover - auto_level facts all_names th = +fun prover_dependencies_of ctxt (params as {verbose, max_facts, ...}) prover + auto_level facts all_names th = case isar_dependencies_of all_names th of SOME [] => (false, SOME []) | isar_deps => @@ -653,11 +655,12 @@ SOME ((name, status), th) => accum @ [((name, status), th)] | NONE => accum (* shouldn't happen *) val facts = - facts |> mepo_suggested_facts ctxt params prover - (max_facts |> the_default atp_dependency_default_max_facts) - NONE hyp_ts concl_t - |> fold (add_isar_dep facts) (these isar_deps) - |> map fix_name + facts + |> mepo_suggested_facts ctxt params prover + (max_facts |> the_default prover_dependency_default_max_facts) + NONE hyp_ts concl_t + |> fold (add_isar_dep facts) (these isar_deps) + |> map fix_name in if verbose andalso auto_level = 0 then let val num_facts = length facts in @@ -680,7 +683,7 @@ (); case used_facts |> map fst |> trim_dependencies th of NONE => (false, isar_deps) - | atp_deps => (true, atp_deps)) + | prover_deps => (true, prover_deps)) | _ => (false, isar_deps) end @@ -789,12 +792,12 @@ fun maybe_rep_from from (accum as (parents, graph)) = try_graph ctxt "updating graph" accum (fn () => (from :: parents, Graph.add_edge_acyclic (from, name) graph)) - val graph = graph |> update_fact_graph_node (name, ATP_Proof) + val graph = graph |> update_fact_graph_node (name, Automatic_Proof) val (deps, _) = ([], graph) |> fold maybe_rep_from deps in ((name, deps) :: reps, graph) end fun flop_wrt_fact_graph name = - update_fact_graph_node (name, Isar_Proof_wegen_ATP_Flop) + update_fact_graph_node (name, Isar_Proof_wegen_Prover_Flop) val learn_timeout_slack = 2.0 @@ -835,7 +838,7 @@ (* The timeout is understood in a very slack fashion. *) fun mash_learn_facts ctxt (params as {debug, verbose, overlord, ...}) prover - auto_level atp learn_timeout facts = + auto_level run_prover learn_timeout facts = let val timer = Timer.startRealTimer () fun next_commit_time () = @@ -845,11 +848,13 @@ facts |> List.partition (is_fact_in_graph fact_G) ||> sort (thm_ord o pairself snd) in - if null new_facts andalso (not atp orelse null old_facts) then + if null new_facts andalso (not run_prover orelse null old_facts) then if auto_level < 2 then - "No new " ^ (if atp then "ATP" else "Isar") ^ " proofs to learn." ^ - (if auto_level = 0 andalso not atp then - "\n\nHint: Try " ^ sendback learn_atpN ^ " to learn from ATP proofs." + "No new " ^ (if run_prover then "automatic" else "Isar") ^ + " proofs to learn." ^ + (if auto_level = 0 andalso not run_prover then + "\n\nHint: Try " ^ sendback learn_proverN ^ + " to learn from automatic provers." else "") else @@ -862,8 +867,9 @@ fun deps_of status th = if status = Non_Rec_Def orelse status = Rec_Def then SOME [] - else if atp then - atp_dependencies_of ctxt params prover auto_level facts all_names th + else if run_prover then + prover_dependencies_of ctxt params prover auto_level facts all_names + th |> (fn (false, _) => NONE | (true, deps) => deps) else isar_dependencies_of all_names th @@ -894,7 +900,7 @@ if not last andalso auto_level = 0 then let val num_proofs = length adds + length reps in "Learned " ^ string_of_int num_proofs ^ " " ^ - (if atp then "ATP" else "Isar") ^ " proof" ^ + (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s num_proofs ^ " in the last " ^ string_from_time commit_timeout ^ "." |> Output.urgent_message @@ -950,7 +956,7 @@ val timed_out = Time.> (Timer.checkRealTimer timer, learn_timeout) in ((reps, flops), (n, next_commit, timed_out)) end val n = - if not atp orelse null old_facts then + if not run_prover orelse null old_facts then n else let @@ -962,8 +968,8 @@ random_range 0 max_isar + (case kind_of_proof th of Isar_Proof => 0 - | ATP_Proof => 2 * max_isar - | Isar_Proof_wegen_ATP_Flop => max_isar) + | Automatic_Proof => 2 * max_isar + | Isar_Proof_wegen_Prover_Flop => max_isar) - 500 * (th |> isar_dependencies_of all_names |> Option.map length |> the_default max_dependencies) @@ -978,7 +984,7 @@ in if verbose orelse auto_level < 2 then "Learned " ^ string_of_int n ^ " nontrivial " ^ - (if atp then "ATP" else "Isar") ^ " proof" ^ plural_s n ^ + (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s n ^ (if verbose then " in " ^ string_from_time (Timer.checkRealTimer timer) else @@ -989,7 +995,7 @@ end fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained - atp = + run_prover = let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val ctxt = ctxt |> Config.put instantiate_inducts false @@ -998,17 +1004,19 @@ @{prop True} val num_facts = length facts val prover = hd provers - fun learn auto_level atp = - mash_learn_facts ctxt params prover auto_level atp infinite_timeout facts + fun learn auto_level run_prover = + mash_learn_facts ctxt params prover auto_level run_prover infinite_timeout + facts |> Output.urgent_message in - if atp then + if run_prover then ("MaShing through " ^ string_of_int num_facts ^ " fact" ^ - plural_s num_facts ^ " for ATP proofs (" ^ quote prover ^ " timeout: " ^ - string_from_time timeout ^ ").\n\nCollecting Isar proofs first..." + plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^ + " timeout: " ^ string_from_time timeout ^ + ").\n\nCollecting Isar proofs first..." |> Output.urgent_message; learn 1 false; - "Now collecting ATP proofs. This may take several hours. You can \ + "Now collecting automatic proofs. This may take several hours. You can \ \safely stop the learning process at any point." |> Output.urgent_message; learn 0 true)