# HG changeset patch # User blanchet # Date 1283286453 -7200 # Node ID 820b8221ed48f9392eef756e6a6030317b5a37c2 # Parent da5e4f182f69c51ec6750af1776a3516de4343e3 added "blocking" option to Sledgehammer to run in synchronous mode; sometimes useful, e.g. for testing diff -r da5e4f182f69 -r 820b8221ed48 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 31 21:17:19 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 31 22:27:33 2010 +0200 @@ -13,7 +13,8 @@ type relevance_override = Sledgehammer_Fact_Filter.relevance_override type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command type params = - {debug: bool, + {blocking: bool, + debug: bool, verbose: bool, overlord: bool, atps: string list, @@ -80,7 +81,8 @@ (** problems, results, provers, etc. **) type params = - {debug: bool, + {blocking: bool, + debug: bool, verbose: bool, overlord: bool, atps: string list, @@ -362,8 +364,9 @@ fun get_prover_fun thy name = prover_fun name (get_prover thy name) -fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n - relevance_override minimize_command proof_state +fun start_prover_thread (params as {blocking, verbose, full_types, timeout, + ...}) + i n relevance_override minimize_command proof_state atp_name = let val thy = Proof.theory_of proof_state @@ -374,23 +377,25 @@ val desc = "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)); + fun run () = + let + val problem = + {subgoal = i, goal = (ctxt, (facts, goal)), + relevance_override = relevance_override, axioms = NONE} + in + prover params (minimize_command atp_name) problem |> #message + handle ERROR message => "Error: " ^ message ^ "\n" + | exn => "Internal error:\n" ^ ML_Compiler.exn_message exn ^ "\n" + end in - Async_Manager.launch das_Tool verbose birth_time death_time desc - (fn () => - let - val problem = - {subgoal = i, goal = (ctxt, (facts, goal)), - relevance_override = relevance_override, axioms = NONE} - in - prover params (minimize_command atp_name) problem |> #message - handle ERROR message => "Error: " ^ message ^ "\n" - | exn => "Internal error: \n" ^ ML_Compiler.exn_message exn ^ - "\n" - end) + if blocking then + priority (desc ^ "\n" ^ TimeLimit.timeLimit timeout run ()) + else + Async_Manager.launch das_Tool verbose birth_time death_time desc run end fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set." - | run_sledgehammer (params as {atps, ...}) i relevance_override + | run_sledgehammer (params as {blocking, atps, ...}) i relevance_override minimize_command state = case subgoal_count state of 0 => priority "No subgoal!" @@ -398,8 +403,10 @@ let val _ = kill_atps () val _ = priority "Sledgehammering..." - val _ = app (start_prover_thread params i n relevance_override - minimize_command state) atps + val _ = + (if blocking then Par_List.map else map) + (start_prover_thread params i n relevance_override + minimize_command state) atps in () end val setup = diff -r da5e4f182f69 -r 820b8221ed48 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 31 21:17:19 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 31 22:27:33 2010 +0200 @@ -49,8 +49,8 @@ val _ = priority ("Testing " ^ n_theorems (map fst axioms) ^ "...") val params = - {debug = debug, verbose = verbose, overlord = overlord, atps = atps, - full_types = full_types, explicit_apply = explicit_apply, + {blocking = true, debug = debug, verbose = verbose, overlord = overlord, + atps = atps, full_types = full_types, explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01), max_relevant = NONE, theory_relevant = NONE, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout} diff -r da5e4f182f69 -r 820b8221ed48 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 31 21:17:19 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Aug 31 22:27:33 2010 +0200 @@ -63,7 +63,8 @@ type raw_param = string * string list val default_default_params = - [("debug", "false"), + [("blocking", "false"), + ("debug", "false"), ("verbose", "false"), ("overlord", "false"), ("explicit_apply", "false"), @@ -76,7 +77,8 @@ val alias_params = [("atp", "atps")] val negated_alias_params = - [("no_debug", "debug"), + [("non_blocking", "blocking"), + ("no_debug", "debug"), ("quiet", "verbose"), ("no_overlord", "overlord"), ("partial_types", "full_types"), @@ -167,6 +169,7 @@ case lookup name of SOME "smart" => NONE | _ => SOME (lookup_int name) + val blocking = lookup_bool "blocking" val debug = lookup_bool "debug" val verbose = debug orelse lookup_bool "verbose" val overlord = lookup_bool "overlord" @@ -182,8 +185,8 @@ val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor") val timeout = lookup_time "timeout" in - {debug = debug, verbose = verbose, overlord = overlord, atps = atps, - full_types = full_types, explicit_apply = explicit_apply, + {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord, + atps = atps, full_types = full_types, explicit_apply = explicit_apply, relevance_thresholds = relevance_thresholds, max_relevant = max_relevant, theory_relevant = theory_relevant, isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor, timeout = timeout}