# HG changeset patch # User boehmes # Date 1251806999 -7200 # Node ID 1ad7d4fc0954fd86d6500a4e832b6567406d2484 # Parent 3e6f5365971ef557b7479b0a0bdac99a677c244a Mirabelle: added preliminary documentation, Mirabelle: removed option "verbose", Mirabelle: actions need to limit their execution time themselves, sledgehammer: do not report chained facts diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML Tue Sep 01 14:09:59 2009 +0200 @@ -9,12 +9,12 @@ val logfile : string Config.T val timeout : int Config.T - val verbose : bool Config.T val start_line : int Config.T val end_line : int Config.T val goal_thm_of : Proof.state -> thm - val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool + val can_apply : Time.time -> (Proof.context -> int -> tactic) -> + Proof.state -> bool val theorems_in_proof_term : Thm.thm -> Thm.thm list val theorems_of_sucessful_proof : Toplevel.state option -> Thm.thm list val get_setting : (string * string) list -> string * string -> string @@ -38,7 +38,8 @@ (* Mirabelle core *) -type action = {pre: Proof.state, post: Toplevel.state option} -> string option +type action = Time.time -> {pre: Proof.state, post: Toplevel.state option} -> + string option structure Actions = TheoryDataFun ( @@ -53,11 +54,10 @@ val (logfile, setup1) = Attrib.config_string "mirabelle_logfile" "" val (timeout, setup2) = Attrib.config_int "mirabelle_timeout" 30 -val (verbose, setup3) = Attrib.config_bool "mirabelle_verbose" true -val (start_line, setup4) = Attrib.config_int "mirabelle_start_line" 0 -val (end_line, setup5) = Attrib.config_int "mirabelle_end_line" ~1 +val (start_line, setup3) = Attrib.config_int "mirabelle_start_line" 0 +val (end_line, setup4) = Attrib.config_int "mirabelle_end_line" ~1 -val setup = setup1 #> setup2 #> setup3 #> setup4 #> setup5 +val setup = setup1 #> setup2 #> setup3 #> setup4 local @@ -67,17 +67,15 @@ (* FIXME: with multithreading and parallel proofs enabled, we might need to encapsulate this inside a critical section *) -fun verbose_msg verbose msg = if verbose then SOME msg else NONE - -fun with_time_limit (verb, secs) f x = TimeLimit.timeLimit secs f x - handle TimeLimit.TimeOut => verbose_msg verb "time out" - | ERROR msg => verbose_msg verb ("error: " ^ msg) +fun capture_exns f x = + let + fun f' x = f x + handle TimeLimit.TimeOut => SOME "time out" + | ERROR msg => SOME ("error: " ^ msg) + in (case try f' x of NONE => SOME "exception" | SOME msg => msg) end -fun capture_exns verb f x = - (case try f x of NONE => verbose_msg verb "exception" | SOME msg => msg) - -fun apply_action (c as (verb, _)) st (name, action) = - Option.map (pair name) (capture_exns verb (with_time_limit c action) st) +fun apply_action timeout st (name, action) = + Option.map (pair name) (capture_exns (action timeout) st) fun in_range _ _ NONE = true | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r)) @@ -104,13 +102,12 @@ val thy = Proof.theory_of pre val pos = Toplevel.pos_of tr val name = Toplevel.name_of tr - val verb = Config.get_thy thy verbose - val secs = Time.fromSeconds (Config.get_thy thy timeout) + val timeout = Time.fromSeconds (Config.get_thy thy timeout) val st = {pre=pre, post=post} in Actions.get thy |> Symtab.dest - |> only_within_range thy pos (map_filter (apply_action (verb, secs) st)) + |> only_within_range thy pos (map_filter (apply_action timeout st)) |> (fn [] => () | msgs => log thy (pretty_print pos name msgs)) end @@ -131,10 +128,12 @@ val goal_thm_of = snd o snd o Proof.get_goal -fun can_apply tac st = - let val (ctxt, (facts, goal)) = Proof.get_goal st +fun can_apply timeout tac st = + let + val (ctxt, (facts, goal)) = Proof.get_goal st + val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt) in - (case Seq.pull (HEADGOAL (Method.insert_tac facts THEN' tac ctxt) goal) of + (case TimeLimit.timeLimit timeout (Seq.pull o full_tac) goal of SOME (thm, _) => true | NONE => false) end diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML Tue Sep 01 14:09:59 2009 +0200 @@ -5,8 +5,8 @@ structure Mirabelle_Arith : MIRABELLE_ACTION = struct -fun arith_action {pre=st, ...} = - if Mirabelle.can_apply Arith_Data.arith_tac st +fun arith_action timeout {pre=st, ...} = + if Mirabelle.can_apply timeout Arith_Data.arith_tac st then SOME "succeeded" else NONE diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML Tue Sep 01 14:09:59 2009 +0200 @@ -5,7 +5,7 @@ structure Mirabelle_Metis : MIRABELLE_ACTION = struct -fun metis_action {pre, post} = +fun metis_action timeout {pre, post} = let val thms = Mirabelle.theorems_of_sucessful_proof post val names = map Thm.get_name thms @@ -14,7 +14,7 @@ fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts) in - (if Mirabelle.can_apply metis pre then "succeeded" else "failed") + (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |> suffix (" (" ^ commas names ^ ")") |> SOME end diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML Tue Sep 01 14:09:59 2009 +0200 @@ -5,11 +5,12 @@ structure Mirabelle_Quickcheck : MIRABELLE_ACTION = struct -fun quickcheck_action args {pre=st, ...} = +fun quickcheck_action limit args {pre=st, ...} = let val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst + val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1 in - (case Quickcheck.quickcheck (filter has_valid_key args) 1 st of + (case TimeLimit.timeLimit limit quickcheck st of NONE => SOME "no counterexample" | SOME _ => SOME "counterexample found") end diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_refute.ML Tue Sep 01 14:09:59 2009 +0200 @@ -7,13 +7,14 @@ (* FIXME: -fun refute_action args {pre=st, ...} = +fun refute_action args timeout {pre=st, ...} = let val subgoal = 0 val thy = Proof.theory_of st val thm = goal_thm_of st - val _ = Refute.refute_subgoal thy args thm subgoal + val refute = Refute.refute_subgoal thy args thm + val _ = TimeLimit.timeLimit timeout refute subgoal in val writ_log = Substring.full (the (Symtab.lookup tab "writeln")) val warn_log = Substring.full (the (Symtab.lookup tab "warning")) diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Sep 01 14:09:59 2009 +0200 @@ -29,7 +29,7 @@ val keepK = "keep" val metisK = "metis" -fun sledgehammer_action args {pre=st, ...} = +fun sledgehammer_action args timeout {pre=st, ...} = let val prover_name = AList.lookup (op =) args proverK @@ -38,7 +38,7 @@ val thy = Proof.theory_of st val prover = the (AtpManager.get_prover prover_name thy) - val timeout = AtpManager.get_timeout () + val atp_timeout = AtpManager.get_timeout () (* run sledgehammer *) fun init NONE = !AtpWrapper.destdir @@ -51,8 +51,9 @@ fun done path = AtpWrapper.destdir := path fun sh _ = let + val atp = prover atp_timeout NONE NONE prover_name 1 val (success, (message, thm_names), _, _, _) = - prover timeout NONE NONE prover_name 1 (Proof.get_goal st) + TimeLimit.timeLimit timeout atp (Proof.get_goal st) in (success, message, SOME thm_names) end handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME []) | ERROR msg => (false, "error: " ^ msg, NONE) @@ -63,7 +64,7 @@ fun get_thms ctxt = maps (thms_of_name ctxt) fun metis thms ctxt = MetisTools.metis_tac ctxt thms fun apply_metis thms = "\nApplying metis with these theorems: " ^ - (if Mirabelle.can_apply (metis thms) st + (if Mirabelle.can_apply timeout (metis thms) st then "success" else "failure") val msg = if not (AList.defined (op =) args metisK) then "" diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/Mirabelle/doc/options.txt --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Mirabelle/doc/options.txt Tue Sep 01 14:09:59 2009 +0200 @@ -0,0 +1,6 @@ +Options for sledgehammer: + + * prover=NAME: name of the external prover to call + * keep=PATH: path where to keep temporary files created by sledgehammer + * metis=X: apply metis with the theorems found by sledgehammer (X may be any + non-empty string) diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/Mirabelle/etc/settings --- a/src/HOL/Tools/Mirabelle/etc/settings Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/etc/settings Tue Sep 01 14:09:59 2009 +0200 @@ -4,6 +4,5 @@ MIRABELLE_THEORY=Main MIRABELLE_OUTPUT_PATH=/tmp/mirabelle MIRABELLE_TIMEOUT=30 -MIRABELLE_VERBOSE=false ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle Tue Sep 01 14:09:59 2009 +0200 @@ -25,7 +25,6 @@ echo " -L LOGIC parent logic to use (default $ISABELLE_LOGIC)" echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" echo " -O DIR output directory for test data (default $out)" - echo " -v be verbose" echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" echo echo " Apply the given actions (i.e., automated proof tools)" @@ -47,7 +46,7 @@ # options -while getopts "L:T:O:vt:?" OPT +while getopts "L:T:O:t:?" OPT do case "$OPT" in L) @@ -59,9 +58,6 @@ O) MIRABELLE_OUTPUT_PATH="$OPTARG" ;; - v) - MIRABELLE_VERBOSE="true" - ;; t) MIRABELLE_TIMEOUT="$OPTARG" ;; diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl Tue Sep 01 14:09:59 2009 +0200 @@ -13,7 +13,6 @@ my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; -my $verbose = $ENV{'MIRABELLE_VERBOSE'}; my $timeout = $ENV{'MIRABELLE_TIMEOUT'}; my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; @@ -66,7 +65,6 @@ setup {* Config.put_thy Mirabelle.logfile "$log_file" #> Config.put_thy Mirabelle.timeout $timeout #> - Config.put_thy Mirabelle.verbose $verbose #> Config.put_thy Mirabelle.start_line $start_line #> Config.put_thy Mirabelle.end_line $end_line *} diff -r 3e6f5365971e -r 1ad7d4fc0954 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Mon Aug 31 19:28:37 2009 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Tue Sep 01 14:09:59 2009 +0200 @@ -557,7 +557,7 @@ in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^ (if used_conj then "" else "\nWarning: Goal is provable because context is inconsistent."), - lemmas) + nochained lemmas) end; (* === Extracting structured Isar-proof === *)