# HG changeset patch # User blanchet # Date 1271272933 -7200 # Node ID 6490319b17030e252d1425ae54a5d228d61753f0 # Parent f5e15e9aae10df54e81445636c8b087125a7e1cd added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture diff -r f5e15e9aae10 -r 6490319b1703 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 14 18:23:51 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Wed Apr 14 21:22:13 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 f5e15e9aae10 -r 6490319b1703 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Apr 14 18:23:51 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Apr 14 21:22:13 2010 +0200 @@ -120,7 +120,7 @@ " 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}, diff -r f5e15e9aae10 -r 6490319b1703 src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 14 18:23:51 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Wed Apr 14 21:22:13 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)) @@ -219,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)) diff -r f5e15e9aae10 -r 6490319b1703 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Apr 14 18:23:51 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Apr 14 21:22:13 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"), @@ -56,6 +57,7 @@ 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"), @@ -133,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" @@ -148,12 +151,12 @@ 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)