--- a/src/HOL/IsaMakefile Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/IsaMakefile Mon Sep 07 11:44:12 2009 +0100
@@ -1124,7 +1124,7 @@
HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
-$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/MirabelleTest.thy \
+$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy \
Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML Mirabelle/ROOT.ML \
Mirabelle/Tools/mirabelle_arith.ML \
Mirabelle/Tools/mirabelle_metis.ML \
--- a/src/HOL/MetisExamples/set.thy Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/MetisExamples/set.thy Mon Sep 07 11:44:12 2009 +0100
@@ -238,7 +238,7 @@
lemma (*singleton_example_2:*)
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_eq)
+by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
lemma singleton_example_2:
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
@@ -275,8 +275,8 @@
apply (metis emptyE)
apply (metis insert_iff singletonE)
apply (metis insertCI singletonE zless_le)
-apply (metis insert_iff singletonE)
-apply (metis insert_iff singletonE)
+apply (metis Collect_def Collect_mem_eq)
+apply (metis Collect_def Collect_mem_eq)
apply (metis DiffE)
apply (metis pair_in_Id_conv)
done
--- a/src/HOL/Mirabelle/MirabelleTest.thy Mon Sep 07 10:04:17 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: MirabelleTest.thy
- Author: Sascha Boehme
-*)
-
-header {* Simple test theory for Mirabelle actions *}
-
-theory MirabelleTest
-imports Main Mirabelle
-uses
- "Tools/mirabelle_arith.ML"
- "Tools/mirabelle_metis.ML"
- "Tools/mirabelle_quickcheck.ML"
- "Tools/mirabelle_refute.ML"
- "Tools/mirabelle_sledgehammer.ML"
-begin
-
-(*
- only perform type-checking of the actions,
- any reasonable test would be too complicated
-*)
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Mon Sep 07 11:44:12 2009 +0100
@@ -0,0 +1,22 @@
+(* Title: Mirabelle_Test.thy
+ Author: Sascha Boehme
+*)
+
+header {* Simple test theory for Mirabelle actions *}
+
+theory Mirabelle_Test
+imports Main Mirabelle
+uses
+ "Tools/mirabelle_arith.ML"
+ "Tools/mirabelle_metis.ML"
+ "Tools/mirabelle_quickcheck.ML"
+ "Tools/mirabelle_refute.ML"
+ "Tools/mirabelle_sledgehammer.ML"
+begin
+
+(*
+ only perform type-checking of the actions,
+ any reasonable test would be too complicated
+*)
+
+end
--- a/src/HOL/Mirabelle/ROOT.ML Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Mirabelle/ROOT.ML Mon Sep 07 11:44:12 2009 +0100
@@ -1,1 +1,1 @@
-use_thy "MirabelleTest";
+use_thy "Mirabelle_Test";
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Mon Sep 07 11:44:12 2009 +0100
@@ -12,8 +12,11 @@
val setup : theory -> theory
(* core *)
+ type init_action
+ type done_action
+ type run_action
type action
- val catch : string -> action -> action
+ val catch : (int -> string) -> run_action -> run_action
val register : action -> theory -> theory
val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
unit
@@ -47,12 +50,16 @@
(* Mirabelle core *)
-type action = {pre: Proof.state, post: Toplevel.state option,
+
+type init_action = int -> theory -> theory
+type done_action = int -> {last: Toplevel.state, log: string -> unit} -> unit
+type run_action = int -> {pre: Proof.state, post: Toplevel.state option,
timeout: Time.time, log: string -> unit} -> unit
+type action = init_action * run_action * done_action
structure Actions = TheoryDataFun
(
- type T = action list
+ type T = (int * run_action * done_action) list
val empty = []
val copy = I
val extend = I
@@ -63,11 +70,17 @@
fun app_with f g x = (g x; ())
handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ())
-fun catch tag f (st as {log, ...}) =
- let fun log_exn e = log (tag ^ "exception:\n" ^ General.exnMessage e)
- in app_with log_exn f st end
+fun catch tag f id (st as {log, ...}) =
+ let fun log_exn e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
+ in app_with log_exn (f id) st end
-val register = Actions.map o cons
+fun register (init, run, done) thy =
+ let val id = length (Actions.get thy) + 1
+ in
+ thy
+ |> init id
+ |> Actions.map (cons (id, run, done))
+ end
local
@@ -82,7 +95,7 @@
fun apply_actions thy info (pre, post, time) actions =
let
fun apply f = f {pre=pre, post=post, timeout=time, log=log thy}
- fun run f = (apply f; log_sep thy)
+ fun run (id, run, _) = (apply (run id); log_sep thy)
in (log thy info; log_sep thy; List.app run actions) end
fun in_range _ _ NONE = true
@@ -94,7 +107,7 @@
in
-fun basic_hook tr pre post =
+fun run_actions tr pre post =
let
val thy = Proof.theory_of pre
val pos = Toplevel.pos_of tr
@@ -108,6 +121,16 @@
only_within_range thy pos (apply_actions thy info st) (Actions.get thy)
end
+fun done_actions st =
+ let
+ val thy = Toplevel.theory_of st
+ val _ = log thy "\n\n";
+ in
+ thy
+ |> Actions.get
+ |> List.app (fn (id, _, done) => done id {last=st, log=log thy})
+ end
+
end
val whitelist = ["apply", "by", "proof"]
@@ -116,7 +139,9 @@
(* FIXME: might require wrapping into "interruptible" *)
if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
member (op =) whitelist (Toplevel.name_of tr)
- then basic_hook tr (Toplevel.proof_of pre) (SOME post)
+ then run_actions tr (Toplevel.proof_of pre) (SOME post)
+ else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post
+ then done_actions pre
else () (* FIXME: add theory_hook here *)
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Mon Sep 07 11:44:12 2009 +0100
@@ -5,12 +5,17 @@
structure Mirabelle_Arith : MIRABELLE_ACTION =
struct
-fun arith_action {pre, timeout, log, ...} =
+fun arith_tag id = "#" ^ string_of_int id ^ " arith: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id {pre, timeout, log, ...} =
if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
- then log "arith: succeeded"
+ then log (arith_tag id ^ "succeeded")
else ()
- handle TimeLimit.TimeOut => log "arith: time out"
+ handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout")
-fun invoke _ = Mirabelle.register (Mirabelle.catch "arith: " arith_action)
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Mon Sep 07 11:44:12 2009 +0100
@@ -5,7 +5,12 @@
structure Mirabelle_Metis : MIRABELLE_ACTION =
struct
-fun metis_action {pre, post, timeout, log} =
+fun metis_tag id = "#" ^ string_of_int id ^ " metis: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id {pre, post, timeout, log} =
let
val thms = Mirabelle.theorems_of_sucessful_proof post
val names = map Thm.get_name thms
@@ -16,12 +21,13 @@
fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
in
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
- |> prefix "metis: "
+ |> prefix (metis_tag id)
|> add_info
|> log
end
- handle TimeLimit.TimeOut => log "metis: time out"
+ handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
+ | ERROR msg => log (metis_tag id ^ "error: " ^ msg)
-fun invoke _ = Mirabelle.register (Mirabelle.catch "metis: " metis_action)
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Mon Sep 07 11:44:12 2009 +0100
@@ -5,18 +5,24 @@
structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
struct
-fun quickcheck_action args {pre, timeout, log, ...} =
+fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run args id {pre, timeout, log, ...} =
let
val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
in
(case TimeLimit.timeLimit timeout quickcheck pre of
- NONE => log "quickcheck: no counterexample"
- | SOME _ => log "quickcheck: counterexample found")
+ NONE => log (qc_tag id ^ "no counterexample")
+ | SOME _ => log (qc_tag id ^ "counterexample found"))
end
- handle TimeLimit.TimeOut => log "quickcheck: time out"
+ handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout")
+ | ERROR msg => log (qc_tag id ^ "error: " ^ msg)
fun invoke args =
- Mirabelle.register (Mirabelle.catch "quickcheck: " (quickcheck_action args))
+ Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done)
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Mon Sep 07 11:44:12 2009 +0100
@@ -27,7 +27,7 @@
else SOME "real counterexample (bug?)"
else
if Substring.isSubstring "time limit" writ_log
- then SOME "no counterexample (time out)"
+ then SOME "no counterexample (timeout)"
else if Substring.isSubstring "Search terminated" writ_log
then SOME "no counterexample (normal termination)"
else SOME "no counterexample (unknown)"
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 07 11:44:12 2009 +0100
@@ -5,6 +5,167 @@
structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
struct
+val proverK = "prover"
+val keepK = "keep"
+val metisK = "metis"
+val full_typesK = "full_types"
+val minimizeK = "minimize"
+val minimize_timeoutK = "minimize_timeout"
+
+fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
+fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
+fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): "
+
+val separator = "-----"
+
+
+datatype data = Data of {
+ sh_calls: int,
+ sh_success: int,
+ sh_time: int,
+ metis_calls: int,
+ metis_success: int,
+ metis_time: int,
+ metis_timeout: int }
+
+fun make_data (sh_calls, sh_success, sh_time, metis_calls, metis_success,
+ metis_time, metis_timeout) =
+ Data {sh_calls=sh_calls, sh_success=sh_success, sh_time=sh_time,
+ metis_calls=metis_calls, metis_success=metis_success,
+ metis_time=metis_time, metis_timeout=metis_timeout}
+
+fun map_data f (Data {sh_calls, sh_success, sh_time, metis_calls,
+ metis_success, metis_time, metis_timeout}) =
+ make_data (f (sh_calls, sh_success, sh_time, metis_calls, metis_success,
+ metis_time, metis_timeout))
+
+val empty_data = make_data (0, 0, 0, 0, 0, 0, 0)
+
+val inc_sh_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
+ metis_success, metis_time, metis_timeout) => (sh_calls + 1, sh_success,
+ sh_time, metis_calls, metis_success, metis_time, metis_timeout))
+
+val inc_sh_success = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
+ metis_success, metis_time, metis_timeout) => (sh_calls, sh_success + 1,
+ sh_time, metis_calls, metis_success, metis_time, metis_timeout))
+
+fun inc_sh_time t = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
+ metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
+ sh_time + t, metis_calls, metis_success, metis_time, metis_timeout))
+
+val inc_metis_calls = map_data (fn (sh_calls, sh_success, sh_time, metis_calls,
+ metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
+ sh_time, metis_calls + 1, metis_success, metis_time, metis_timeout))
+
+val inc_metis_success = map_data (fn (sh_calls, sh_success, sh_time,
+ metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
+ sh_success, sh_time, metis_calls, metis_success + 1, metis_time,
+ metis_timeout))
+
+fun inc_metis_time t = map_data (fn (sh_calls, sh_success, sh_time,
+ metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
+ sh_success, sh_time, metis_calls, metis_success, metis_time + t,
+ metis_timeout))
+
+val inc_metis_timeout = map_data (fn (sh_calls, sh_success, sh_time,
+ metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
+ sh_success, sh_time, metis_calls, metis_success, metis_time,
+ metis_timeout + 1))
+
+
+local
+
+val str = string_of_int
+val str3 = Real.fmt (StringCvt.FIX (SOME 3))
+fun percentage a b = string_of_int (a * 100 div b)
+fun time t = Real.fromInt t / 1000.0
+fun avg_time t n =
+ if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
+
+fun log_sh_data log sh_calls sh_success sh_time =
+ (log ("Total number of sledgehammer calls: " ^ str sh_calls);
+ log ("Number of successful sledgehammer calls: " ^ str sh_success);
+ log ("Success rate: " ^ percentage sh_success sh_calls ^ "%");
+ log ("Total time for successful sledgehammer calls: " ^ str3 (time sh_time));
+ log ("Average time for successful sledgehammer calls: " ^
+ str3 (avg_time sh_time sh_success)))
+
+fun log_metis_data log sh_success metis_calls metis_success metis_time
+ metis_timeout =
+ (log ("Total number of metis calls: " ^ str metis_calls);
+ log ("Number of successful metis calls: " ^ str metis_success);
+ log ("Number of metis timeouts: " ^ str metis_timeout);
+ log ("Number of metis exceptions: " ^
+ str (sh_success - metis_success - metis_timeout));
+ log ("Success rate: " ^ percentage metis_success sh_success ^ "%");
+ log ("Total time for successful metis calls: " ^ str3 (time metis_time));
+ log ("Average time for successful metis calls: " ^
+ str3 (avg_time metis_time metis_success)))
+
+in
+
+fun log_data id log (Data {sh_calls, sh_success, sh_time, metis_calls,
+ metis_success, metis_time, metis_timeout}) =
+ if sh_calls > 0
+ then
+ (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
+ log_sh_data log sh_calls sh_success sh_time;
+ log "";
+ if metis_calls > 0 then log_metis_data log sh_success metis_calls
+ metis_success metis_time metis_timeout else ())
+ else ()
+
+end
+
+
+(* Warning: we implicitly assume single-threaded execution here! *)
+val data = ref ([] : (int * data) list)
+
+fun init id thy = (change data (cons (id, empty_data)); thy)
+fun done id {log, ...} =
+ AList.lookup (op =) (!data) id
+ |> Option.map (log_data id log)
+ |> K ()
+
+fun change_data id f = (change data (AList.map_entry (op =) id f); ())
+
+
+fun get_atp thy args =
+ AList.lookup (op =) args proverK
+ |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
+ |> (fn name => (name, the (AtpManager.get_prover name thy)))
+
+local
+
+fun safe init done f x =
+ let
+ val y = init x
+ val z = Exn.capture f y
+ val _ = done y
+ in Exn.release z end
+
+fun init_sh NONE = !AtpWrapper.destdir
+ | init_sh (SOME path) =
+ let
+ (* Warning: we implicitly assume single-threaded execution here! *)
+ val old = !AtpWrapper.destdir
+ val _ = AtpWrapper.destdir := path
+ in old end
+
+fun done_sh path = AtpWrapper.destdir := path
+
+fun run_sh (prover_name, prover) timeout st _ =
+ let
+ val atp = prover (Time.toSeconds timeout) NONE NONE prover_name 1
+ val ((success, (message, thm_names), atp_time, _, _, _), sh_time) =
+ Mirabelle.cpu_time atp (Proof.get_goal st)
+ in
+ if success then (message, SOME (atp_time, sh_time, thm_names))
+ else (message, NONE)
+ end
+ handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, 0, []))
+ | ERROR msg => ("error: " ^ msg, NONE)
+
fun thms_of_name ctxt name =
let
val lex = OuterKeyword.get_lexicons
@@ -18,100 +179,95 @@
|> Source.exhaust
end
-fun safe init done f x =
- let
- val y = init x
- val z = Exn.capture f y
- val _ = done y
- in Exn.release z end
-
-val proverK = "prover"
-val keepK = "keep"
-val metisK = "metis"
-val full_typesK = "full_types"
-
-val sh_tag = "sledgehammer: "
-val metis_tag = "metis (sledgehammer): "
-
-
-local
-
-fun init NONE = !AtpWrapper.destdir
- | init (SOME path) =
- let
- (* Warning: we implicitly assume single-threaded execution here! *)
- val old = !AtpWrapper.destdir
- val _ = AtpWrapper.destdir := path
- in old end
-
-fun done path = AtpWrapper.destdir := path
-
-fun run prover_name timeout st _ =
- let
- val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st))
- val atp_timeout = AtpManager.get_timeout ()
- val atp = prover atp_timeout NONE NONE prover_name 1
- val (success, (message, thm_names), time, _, _, _) =
- TimeLimit.timeLimit timeout atp (Proof.get_goal st)
- in if success then (message, SOME (time, thm_names)) else (message, NONE) end
- handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, []))
- | TimeLimit.TimeOut => ("time out", NONE)
- | ERROR msg => ("error: " ^ msg, NONE)
-
in
-fun run_sledgehammer args thm_names {pre=st, timeout, log, ...} =
+fun run_sledgehammer args named_thms id {pre=st, timeout, log, ...} =
let
- val prover_name =
- AList.lookup (op =) args proverK
- |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
+ val _ = change_data id inc_sh_calls
+ val atp as (prover_name, _) = get_atp (Proof.theory_of st) args
val dir = AList.lookup (op =) args keepK
- val (msg, result) = safe init done (run prover_name timeout st) dir
- val _ =
- if is_some result
- then log (sh_tag ^ "succeeded (" ^ string_of_int (fst (the result)) ^
- ") [" ^ prover_name ^ "]:\n" ^ msg)
- else log (sh_tag ^ "failed: " ^ msg)
- in change thm_names (K (Option.map snd result)) end
+ val (msg, result) = safe init_sh done_sh (run_sh atp timeout st) dir
+ in
+ (case result of
+ SOME (atp_time, sh_time, names) =>
+ let
+ val _ = change_data id inc_sh_success
+ val _ = change_data id (inc_sh_time (atp_time + sh_time))
+
+ fun get_thms name = (name, thms_of_name (Proof.context_of st) name)
+ val _ = named_thms := SOME (map get_thms names)
+ in
+ log (sh_tag id ^ "succeeded (" ^ string_of_int atp_time ^ "+" ^
+ string_of_int sh_time ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
+ end
+ | NONE => log (sh_tag id ^ "failed: " ^ msg))
+ end
end
-fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
- | with_time false t = "failed (" ^ string_of_int t ^ ")"
-
-fun run_metis args thm_names {pre=st, timeout, log, ...} =
+fun run_minimize args named_thms id {pre=st, log, ...} =
let
- fun get_thms ctxt = maps (thms_of_name ctxt)
- fun metis thms ctxt = MetisTools.metis_tac ctxt thms
- fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
- fun timed_metis thms =
- uncurry with_time (Mirabelle.cpu_time apply_metis thms)
- handle TimeLimit.TimeOut => "time out"
- | ERROR msg => "error: " ^ msg
- fun log_metis s = log (metis_tag ^ s)
+ val (prover_name, prover) = get_atp (Proof.theory_of st) args
+ val minimize = AtpMinimal.minimalize prover prover_name
+ val timeout =
+ AList.lookup (op =) args minimize_timeoutK
+ |> Option.map (fst o read_int o explode)
+ |> the_default 5
+ val _ = log separator
in
- if not (AList.defined (op =) args metisK) then ()
- else if is_none (!thm_names) then ()
- else
- log "-----"
- |> K (these (!thm_names))
- |> get_thms (Proof.context_of st)
- |> timed_metis
- |> log_metis
+ (case minimize timeout st (these (!named_thms)) of
+ (SOME named_thms', msg) =>
+ if length named_thms' = length (these (!named_thms))
+ then log (minimize_tag id ^ "already minimal")
+ else
+ (named_thms := SOME named_thms';
+ log (minimize_tag id ^ "succeeded:\n" ^ msg))
+ | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg))
end
-fun sledgehammer_action args (st as {log, ...}) =
+fun run_metis args named_thms id {pre=st, timeout, log, ...} =
let
- val thm_names = ref (NONE : string list option)
- val _ = Mirabelle.catch sh_tag (run_sledgehammer args thm_names) st
- val _ = Mirabelle.catch metis_tag (run_metis args thm_names) st
+ fun metis thms ctxt = MetisTools.metis_tac ctxt thms
+ fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
+
+ fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
+ | with_time (true, t) = (change_data id inc_metis_success;
+ change_data id (inc_metis_time t);
+ "succeeded (" ^ string_of_int t ^ ")")
+ fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
+ handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout")
+ | ERROR msg => "error: " ^ msg
+
+ val _ = log separator
+ val _ = change_data id inc_metis_calls
+ in
+ maps snd named_thms
+ |> timed_metis
+ |> log o prefix (metis_tag id)
+ end
+
+
+fun sledgehammer_action args id (st as {log, ...}) =
+ let
+ val named_thms = ref (NONE : (string * thm list) list option)
+
+ fun if_enabled k f =
+ if AList.defined (op =) args k andalso is_some (!named_thms)
+ then f id st else ()
+
+ val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st
+ val _ = if_enabled minimizeK
+ (Mirabelle.catch minimize_tag (run_minimize args named_thms))
+ val _ = if_enabled metisK
+ (Mirabelle.catch metis_tag (run_metis args (these (!named_thms))))
in () end
fun invoke args =
let
+ val args = (metisK,"yes") :: args; (* always enable metis *)
val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
- in Mirabelle.register (sledgehammer_action args) end
+ in Mirabelle.register (init, sledgehammer_action args, done) end
end
--- a/src/HOL/Mirabelle/doc/options.txt Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Mirabelle/doc/options.txt Mon Sep 07 11:44:12 2009 +0100
@@ -2,6 +2,7 @@
* 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)
- * full_types=X: turn on full-typed encoding (X may be any non-empty string)
+ * full_types: enable full-typed encoding
+ * minimize: enable minimization of theorem set found by sledgehammer
+ * minimize_timeout: timeout for each minimization step
+ * metis: apply metis with the theorems found by sledgehammer
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Mon Sep 07 11:44:12 2009 +0100
@@ -26,14 +26,18 @@
echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
echo " -O DIR output directory for test data (default $out)"
echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
+ echo " -q be quiet (suppress output of Isabelle process)"
echo
echo " Apply the given actions (i.e., automated proof tools)"
echo " at all proof steps in the given theory files."
echo
echo " ACTIONS is a colon-separated list of actions, where each action is"
- echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
+ echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:"
print_action_names
echo
+ echo " A list of available OPTIONs can be found here:"
+ echo " $MIRABELLE_HOME/doc/options.txt"
+ echo
echo " FILES is a list of theory files, where each file is either NAME.thy"
echo " or NAME.thy[START:END] and START and END are numbers indicating the"
echo " range the given actions are to be applied."
@@ -46,7 +50,7 @@
# options
-while getopts "L:T:O:t:?" OPT
+while getopts "L:T:O:t:q?" OPT
do
case "$OPT" in
L)
@@ -61,15 +65,20 @@
t)
MIRABELLE_TIMEOUT="$OPTARG"
;;
+ q)
+ MIRABELLE_QUIET="true"
+ ;;
\?)
usage
;;
esac
done
+export MIRABELLE_QUIET
+
shift $(($OPTIND - 1))
-ACTIONS="$1"
+export MIRABELLE_ACTIONS="$1"
shift
@@ -83,6 +92,6 @@
for FILE in "$@"
do
- perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
+ perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE"
done
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Mon Sep 07 11:44:12 2009 +0100
@@ -14,15 +14,15 @@
my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
+my $be_quiet = $ENV{'MIRABELLE_QUIET'};
+my $actions = $ENV{'MIRABELLE_ACTIONS'};
my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
# arguments
-my $actions = $ARGV[0];
-
-my $thy_file = $ARGV[1];
+my $thy_file = $ARGV[0];
my $start_line = "0";
my $end_line = "~1";
if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
@@ -82,6 +82,10 @@
print SETUP_FILE "$sep(\"$1\", \"$2\")";
$sep = ", ";
}
+ elsif (m/\s*(.*)\s*/) {
+ print SETUP_FILE "$sep(\"$1\", \"\")";
+ $sep = ", ";
+ }
}
print SETUP_FILE "] *}\n";
}
@@ -122,15 +126,17 @@
}
close(LOG_FILE);
-my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
- "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
-
+my $quiet = "";
+if (defined $be_quiet and $be_quiet ne "") {
+ $quiet = " > /dev/null 2>&1";
+}
-# produce report
+print "Mirabelle: $thy_file\n" if ($quiet ne "");
-if ($result == 0) {
- system "perl -w \"$mirabelle_home/lib/scripts/report.pl\" \"$log_file\"";
-}
+my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
+ "-e 'use \"$root_file\";' -q $mirabelle_logic" . $quiet;
+
+print "Finished: $thy_file\n" if ($quiet ne "");
# cleanup
--- a/src/HOL/Mirabelle/lib/scripts/report.pl Mon Sep 07 10:04:17 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-#
-# Author: Sascha Boehme
-#
-# Reports for Mirabelle
-#
-
-my $log_file = $ARGV[0];
-
-open(FILE, "<$log_file") || die "Cannot open file '$log_file'";
-my @lines = <FILE>;
-close(FILE);
-
-my $unhandled = 0;
-
-my $sh_calls = 0;
-my $sh_succeeded = 0;
-my $sh_time = 0;
-
-my $metis_calls = 0;
-my $metis_succeeded = 0;
-my $metis_timeout = 0;
-my $metis_time = 0;
-
-foreach (@lines) {
- if (m/^unhandled exception/) {
- $unhandled++;
- }
- if (m/^sledgehammer:/) {
- $sh_calls++;
- }
- if (m/^sledgehammer: succeeded \(([0-9]+)\)/) {
- $sh_succeeded++;
- $sh_time += $1;
- }
- if (m/^metis \(sledgehammer\):/) {
- $metis_calls++;
- }
- if (m/^metis \(sledgehammer\): succeeded \(([0-9]+)\)/) {
- $metis_succeeded++;
- $metis_time += $1;
- }
- if (m/^metis \(sledgehammer\): time out/) {
- $metis_timeout++;
- }
-}
-
-open(FILE, ">>$log_file") || die "Cannot open file '$log_file'";
-
-print FILE "\n\n\n";
-
-if ($unhandled > 0) {
- print FILE "Number of unhandled exceptions: $unhandled\n\n";
-}
-
-if ($sh_calls > 0) {
- my $percent = $sh_succeeded / $sh_calls * 100;
- my $time = $sh_time / 1000;
- my $avg_time = $time / $sh_succeeded;
- print FILE "Total number of sledgehammer calls: $sh_calls\n";
- print FILE "Number of successful sledgehammer calls: $sh_succeeded\n";
- printf FILE "Success rate: %.0f%%\n", $percent;
- printf FILE "Total time for successful sledgehammer calls: %.3f seconds\n", $time;
- printf FILE "Average time for successful sledgehammer calls: %.3f seconds\n\n", $avg_time;
-}
-
-if ($metis_calls > 0) {
- my $percent = $metis_succeeded / $metis_calls * 100;
- my $time = $metis_time / 1000;
- my $avg_time = $time / $metis_succeeded;
- my $metis_exc = $sh_succeeded - $metis_succeeded - $metis_timeout;
- print FILE "Total number of metis calls: $metis_calls\n";
- print FILE "Number of successful metis calls: $metis_succeeded\n";
- print FILE "Number of metis timeouts: $metis_timeout\n";
- print FILE "Number of metis exceptions: $metis_exc\n";
- printf FILE "Success rate: %.0f%%\n", $percent;
- printf FILE "Total time for successful metis calls: %.3f seconds\n", $time;
- printf FILE "Average time for successful metis calls: %.3f seconds\n", $avg_time;
-}
-
-close(FILE);
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Sep 07 10:04:17 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Mon Sep 07 11:44:12 2009 +0100
@@ -4,7 +4,13 @@
Minimalization of theorem list for metis by using an external automated theorem prover
*)
-structure AtpMinimal: sig end =
+signature ATP_MINIMAL =
+sig
+ val minimalize: AtpManager.prover -> string -> int -> Proof.state ->
+ (string * thm list) list -> (string * thm list) list option * string
+end
+
+structure AtpMinimal: ATP_MINIMAL =
struct
(* output control *)
@@ -103,8 +109,7 @@
fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
let
val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
- val name_thm_pairs =
- flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) ths) name_thms_pairs)
+ val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val _ = debug_fn (fn () => print_names name_thm_pairs)
val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
val (result, proof) =
@@ -130,6 +135,7 @@
val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
fun test_thms filtered thms =
case test_thms_fun filtered thms of (Success _, _) => true | _ => false
+ val answer' = pair and answer'' = pair NONE
in
(* try prove first to check result and get used theorems *)
(case test_thms_fun NONE name_thms_pairs of
@@ -141,25 +147,26 @@
filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
else
name_thms_pairs
- val min_thms = (minimal (test_thms (SOME filtered)) to_use)
+ val min_thms = if null to_use then []
+ else minimal (test_thms (SOME filtered)) to_use
val min_names = order_unique (map fst min_thms)
val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
val _ = debug_fn (fn () => print_names min_thms)
in
- answer ("Try this command: " ^
+ answer' (SOME min_thms) ("Try this command: " ^
Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
end
| (Timeout, _) =>
- answer ("Timeout: You may need to increase the time limit of " ^
+ answer'' ("Timeout: You may need to increase the time limit of " ^
Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ")
| (Error, msg) =>
- answer ("Error in prover: " ^ msg)
+ answer'' ("Error in prover: " ^ msg)
| (Failure, _) =>
- answer "Failure: No proof with the theorems supplied")
+ answer'' "Failure: No proof with the theorems supplied")
handle ResHolClause.TOO_TRIVIAL =>
- answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ answer' (SOME []) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg =>
- answer ("Error: " ^ msg)
+ answer'' ("Error: " ^ msg)
end
@@ -204,8 +211,9 @@
SOME prover => prover
| NONE => error ("Unknown prover: " ^ quote prover_name)
val name_thms_pairs = get_thms (Proof.context_of state) thm_names
+ fun print_answer (_, msg) = answer msg
in
- minimalize prover prover_name time_limit state name_thms_pairs
+ print_answer (minimalize prover prover_name time_limit state name_thms_pairs)
end
val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []