# HG changeset patch # User blanchet # Date 1271272968 -7200 # Node ID e8db171b86432960fbf1f08b9debcea947039ea6 # Parent 0c2538afe8e8861c6f72ce35a8030d1c917a3fda# Parent 6490319b17030e252d1425ae54a5d228d61753f0 merged diff -r 0c2538afe8e8 -r e8db171b8643 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 14 19:46:36 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 14 21:22:48 2010 +0200 @@ -12,6 +12,7 @@ type params = {debug: bool, verbose: bool, + overlord: bool, atps: string list, full_types: bool, respect_no_atp: bool, @@ -64,6 +65,7 @@ type params = {debug: bool, verbose: bool, + overlord: bool, atps: string list, full_types: bool, respect_no_atp: bool, diff -r 0c2538afe8e8 -r e8db171b8643 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Apr 14 19:46:36 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Apr 14 21:22:48 2010 +0200 @@ -22,6 +22,7 @@ structure ATP_Minimal : ATP_MINIMAL = struct +open Sledgehammer_Util open Sledgehammer_Fact_Preprocessor open Sledgehammer_Proof_Reconstruct open ATP_Manager @@ -114,11 +115,12 @@ fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover timeout subgoal state filtered name_thms_pairs = let - val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ - " theorems... ") + val num_theorems = length name_thms_pairs + val _ = priority ("Testing " ^ string_of_int num_theorems ^ + " theorem" ^ plural_s num_theorems ^ "...") val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs - val {context = ctxt, facts, goal} = Proof.goal state + val {context = ctxt, facts, goal} = Proof.raw_goal state val problem = {subgoal = subgoal, goal = (ctxt, (facts, goal)), relevance_override = {add = [], del = [], only = false}, @@ -161,12 +163,17 @@ ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"]) in (SOME min_thms, metis_line i n min_names) end | (Timeout, _) => - (NONE, "Timeout: You may need to increase the time limit of " ^ - string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".") + (NONE, "Timeout: You can increase the time limit using the \"timeout\" \ + \option (e.g., \"timeout = " ^ + string_of_int (10 + msecs div 1000) ^ " s\").") | (Error, msg) => (NONE, "Error in prover: " ^ msg) | (Failure, _) => - (NONE, "Failure: No proof with the theorems supplied")) + (* Failure sometimes mean timeout, unfortunately. *) + (NONE, "Failure: No proof was found with the current time limit. You \ + \can increase the time limit using the \"timeout\" \ + \option (e.g., \"timeout = " ^ + string_of_int (10 + msecs div 1000) ^ " s\").")) handle Sledgehammer_HOL_Clause.TRIVIAL => (SOME [], metis_line i n []) | ERROR msg => (NONE, "Error: " ^ msg) diff -r 0c2538afe8e8 -r e8db171b8643 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 14 19:46:36 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 14 21:22:48 2010 +0200 @@ -65,8 +65,8 @@ else SOME "Ill-formed ATP output" | (failure :: _) => SOME failure -fun generic_prover get_facts prepare write cmd args failure_strs produce_answer - name ({full_types, ...} : params) +fun generic_prover overlord get_facts prepare write cmd args failure_strs + produce_answer name ({full_types, ...} : params) ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} : problem) = let @@ -87,11 +87,15 @@ prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy; (* path to unique problem file *) - val destdir' = Config.get ctxt destdir; + val destdir' = if overlord then getenv "ISABELLE_HOME_USER" + else Config.get ctxt destdir; val problem_prefix' = Config.get ctxt problem_prefix; fun prob_pathname nr = - let val probfile = - Path.basic (problem_prefix' ^ serial_string () ^ "_" ^ string_of_int nr) + let + val probfile = + Path.basic (problem_prefix' ^ + (if overlord then "_" ^ name else serial_string ()) + ^ "_" ^ string_of_int nr) in if destdir' = "" then File.tmp_path probfile else if File.exists (Path.explode destdir') @@ -159,11 +163,11 @@ fun generic_tptp_prover (name, {command, arguments, failure_strs, max_new_clauses, prefers_theory_const, supports_isar_proofs}) - (params as {respect_no_atp, relevance_threshold, convergence, + (params as {overlord, respect_no_atp, relevance_threshold, convergence, theory_const, higher_order, follow_defs, isar_proof, modulus, sorts, ...}) timeout = - generic_prover + generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses (the_default prefers_theory_const theory_const)) @@ -179,6 +183,8 @@ (** common provers **) +fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000 + (* Vampire *) (* NB: Vampire does not work without explicit time limit. *) @@ -186,7 +192,7 @@ val vampire_config : prover_config = {command = Path.explode "$VAMPIRE_HOME/vampire", arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^ - string_of_int (Time.toSeconds timeout)), + string_of_int (generous_to_secs timeout)), failure_strs = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"], max_new_clauses = 60, @@ -201,7 +207,7 @@ {command = Path.explode "$E_HOME/eproof", arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \ \-tAutoDev --silent --cpu-limit=" ^ - string_of_int (Time.toSeconds timeout)), + string_of_int (generous_to_secs timeout)), failure_strs = ["SZS status: Satisfiable", "SZS status Satisfiable", "SZS status: ResourceOut", "SZS status ResourceOut", @@ -217,10 +223,10 @@ fun generic_dfg_prover (name, ({command, arguments, failure_strs, max_new_clauses, prefers_theory_const, ...} : prover_config)) - (params as {respect_no_atp, relevance_threshold, convergence, + (params as {overlord, respect_no_atp, relevance_threshold, convergence, theory_const, higher_order, follow_defs, ...}) timeout = - generic_prover + generic_prover overlord (get_relevant_facts respect_no_atp relevance_threshold convergence higher_order follow_defs max_new_clauses (the_default prefers_theory_const theory_const)) @@ -233,7 +239,7 @@ {command = Path.explode "$SPASS_HOME/SPASS", arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^ " -FullRed=0 -DocProof -TimeLimit=" ^ - string_of_int (Time.toSeconds timeout)), + string_of_int (generous_to_secs timeout)), failure_strs = ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."], @@ -276,7 +282,7 @@ : prover_config) : prover_config = {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", arguments = (fn timeout => - args ^ " -t " ^ string_of_int (Time.toSeconds timeout) ^ " -s " ^ + args ^ " -t " ^ string_of_int (generous_to_secs timeout) ^ " -s " ^ the_system prover_prefix), failure_strs = remote_failure_strs @ failure_strs, max_new_clauses = max_new_clauses, diff -r 0c2538afe8e8 -r e8db171b8643 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Apr 14 19:46:36 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Apr 14 21:22:48 2010 +0200 @@ -40,6 +40,7 @@ val default_default_params = [("debug", "false"), ("verbose", "false"), + ("overlord", "false"), ("respect_no_atp", "true"), ("relevance_threshold", "50"), ("convergence", "320"), @@ -51,9 +52,12 @@ ("sorts", "false"), ("minimize_timeout", "5 s")] -val negated_params = +val alias_params = + [("atp", "atps")] +val negated_alias_params = [("no_debug", "debug"), ("quiet", "verbose"), + ("no_overlord", "overlord"), ("ignore_no_atp", "respect_no_atp"), ("partial_types", "full_types"), ("no_theory_const", "theory_const"), @@ -66,21 +70,25 @@ fun is_known_raw_param s = AList.defined (op =) default_default_params s orelse - AList.defined (op =) negated_params s orelse + AList.defined (op =) alias_params s orelse + AList.defined (op =) negated_alias_params s orelse member (op =) property_dependent_params s fun check_raw_param (s, _) = if is_known_raw_param s then () else error ("Unknown parameter: " ^ quote s ^ ".") -fun unnegate_raw_param (name, value) = - case AList.lookup (op =) negated_params name of - SOME name' => (name', case value of - ["false"] => ["true"] - | ["true"] => ["false"] - | [] => ["false"] - | _ => value) - | NONE => (name, value) +fun unalias_raw_param (name, value) = + case AList.lookup (op =) alias_params name of + SOME name' => (name', value) + | NONE => + case AList.lookup (op =) negated_alias_params name of + SOME name' => (name', case value of + ["false"] => ["true"] + | ["true"] => ["false"] + | [] => ["false"] + | _ => value) + | NONE => (name, value) structure Data = Theory_Data( type T = raw_param list @@ -88,19 +96,23 @@ val extend = I fun merge p : T = AList.merge (op =) (K true) p) -val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param +val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param fun default_raw_params thy = - [("atps", [!atps]), - ("full_types", [if !full_types then "true" else "false"]), - ("timeout", [string_of_int (!timeout) ^ " s"])] @ Data.get thy + |> fold (AList.default (op =)) + [("atps", [!atps]), + ("full_types", [if !full_types then "true" else "false"]), + ("timeout", let val timeout = !timeout in + [if timeout <= 0 then "none" + else string_of_int timeout ^ " s"] + end)] val infinity_time_in_secs = 60 * 60 * 24 * 365 val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs) fun extract_params thy default_params override_params = let - val override_params = map unnegate_raw_param override_params + val override_params = map unalias_raw_param override_params val raw_params = rev override_params @ rev default_params val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params val lookup_string = the_default "" o lookup @@ -123,6 +135,7 @@ " must be assigned an integer value.") val debug = lookup_bool "debug" val verbose = debug orelse lookup_bool "verbose" + val overlord = lookup_bool "overlord" val atps = lookup_string "atps" |> space_explode " " val full_types = lookup_bool "full_types" val respect_no_atp = lookup_bool "respect_no_atp" @@ -138,18 +151,18 @@ val timeout = lookup_time "timeout" val minimize_timeout = lookup_time "minimize_timeout" in - {debug = debug, verbose = verbose, atps = atps, full_types = full_types, - respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold, - convergence = convergence, theory_const = theory_const, - higher_order = higher_order, follow_defs = follow_defs, - isar_proof = isar_proof, modulus = modulus, sorts = sorts, - timeout = timeout, minimize_timeout = minimize_timeout} + {debug = debug, verbose = verbose, overlord = overlord, atps = atps, + full_types = full_types, respect_no_atp = respect_no_atp, + relevance_threshold = relevance_threshold, convergence = convergence, + theory_const = theory_const, higher_order = higher_order, + follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus, + sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout} end fun get_params thy = extract_params thy (default_raw_params thy) fun default_params thy = get_params thy o map (apsnd single) -fun atp_minimize_command override_params old_style_args i fact_refs state = +fun minimize override_params old_style_args i fact_refs state = let val thy = Proof.theory_of state val ctxt = Proof.context_of state @@ -174,7 +187,7 @@ get_params thy [("atps", [atp]), ("minimize_timeout", - [string_of_int (Time.toSeconds timeout) ^ " s"])] + [string_of_int (Time.toMilliseconds timeout) ^ " ms"])] val prover = (case get_prover thy atp of SOME prover => prover @@ -198,6 +211,9 @@ val delN = "del" val onlyN = "only" +fun minimizize_raw_param_name "timeout" = "minimize_timeout" + | minimizize_raw_param_name name = name + fun hammer_away override_params subcommand opt_i relevance_override state = let val thy = Proof.theory_of state @@ -207,8 +223,8 @@ sledgehammer (get_params thy override_params) (the_default 1 opt_i) relevance_override state else if subcommand = minimizeN then - atp_minimize_command override_params [] (the_default 1 opt_i) - (#add relevance_override) state + minimize (map (apfst minimizize_raw_param_name) override_params) [] + (the_default 1 opt_i) (#add relevance_override) state else if subcommand = messagesN then messages opt_i else if subcommand = available_atpsN then @@ -293,8 +309,7 @@ "minimize theorem list with external prover" K.diag (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) => Toplevel.no_timing o Toplevel.unknown_proof o - Toplevel.keep (atp_minimize_command [] args 1 fact_refs - o Toplevel.proof_of))) + Toplevel.keep (minimize [] args 1 fact_refs o Toplevel.proof_of))) val _ = OuterSyntax.improper_command "sledgehammer" diff -r 0c2538afe8e8 -r e8db171b8643 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Apr 14 19:46:36 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Wed Apr 14 21:22:48 2010 +0200 @@ -550,7 +550,7 @@ | minimize_line name xs = "To minimize the number of lemmas, try this command: " ^ Markup.markup Markup.sendback - ("sledgehammer minimize [atps = " ^ name ^ "] (" ^ + ("sledgehammer minimize [atp = " ^ name ^ "] (" ^ space_implode " " xs ^ ")") ^ ".\n" fun metis_lemma_list dfg name (result as (_, _, _, _, goal, i)) = diff -r 0c2538afe8e8 -r e8db171b8643 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Apr 14 19:46:36 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Apr 14 21:22:48 2010 +0200 @@ -6,6 +6,7 @@ signature SLEDGEHAMMER_UTIL = sig + val plural_s : int -> string val serial_commas : string -> string list -> string list val parse_bool_option : bool -> string -> string -> bool option val parse_time_option : string -> string -> Time.time option @@ -17,12 +18,7 @@ structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = struct -(* This hash function is recommended in Compilers: Principles, Techniques, and - Tools, by Aho, Sethi and Ullman. The hashpjw function, which they - particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) -fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) -fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) -fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s +fun plural_s n = if n = 1 then "" else "s" fun serial_commas _ [] = ["??"] | serial_commas _ [s] = [s] @@ -60,4 +56,11 @@ SOME (Time.fromMilliseconds msecs) end +(* This hash function is recommended in Compilers: Principles, Techniques, and + Tools, by Aho, Sethi and Ullman. The hashpjw function, which they + particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) +fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) +fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) +fun hashw_string (s:string, w) = CharVector.foldl hashw_char w s + end;