--- a/src/HOL/IsaMakefile Fri Sep 04 15:18:35 2009 +0200
+++ b/src/HOL/IsaMakefile Fri Sep 04 15:19:51 2009 +0200
@@ -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/Mirabelle/MirabelleTest.thy Fri Sep 04 15:18:35 2009 +0200
+++ /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 Fri Sep 04 15:19:51 2009 +0200
@@ -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 Fri Sep 04 15:18:35 2009 +0200
+++ b/src/HOL/Mirabelle/ROOT.ML Fri Sep 04 15:19:51 2009 +0200
@@ -1,1 +1,1 @@
-use_thy "MirabelleTest";
+use_thy "Mirabelle_Test";
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Fri Sep 04 15:18:35 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Fri Sep 04 15:19:51 2009 +0200
@@ -9,7 +9,7 @@
if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
then log "arith: succeeded"
else ()
- handle TimeLimit.TimeOut => log "arith: time out"
+ handle TimeLimit.TimeOut => log "arith: timeout"
fun invoke _ = Mirabelle.register (Mirabelle.catch "arith: " arith_action)
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 04 15:18:35 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 04 15:19:51 2009 +0200
@@ -20,7 +20,7 @@
|> add_info
|> log
end
- handle TimeLimit.TimeOut => log "metis: time out"
+ handle TimeLimit.TimeOut => log "metis: timeout"
fun invoke _ = Mirabelle.register (Mirabelle.catch "metis: " metis_action)
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Fri Sep 04 15:18:35 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Fri Sep 04 15:19:51 2009 +0200
@@ -14,7 +14,7 @@
NONE => log "quickcheck: no counterexample"
| SOME _ => log "quickcheck: counterexample found")
end
- handle TimeLimit.TimeOut => log "quickcheck: time out"
+ handle TimeLimit.TimeOut => log "quickcheck: timeout"
fun invoke args =
Mirabelle.register (Mirabelle.catch "quickcheck: " (quickcheck_action args))
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Fri Sep 04 15:18:35 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Fri Sep 04 15:19:51 2009 +0200
@@ -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 Fri Sep 04 15:18:35 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Sep 04 15:19:51 2009 +0200
@@ -55,7 +55,7 @@
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)
+ | TimeLimit.TimeOut => ("timeout", NONE)
| ERROR msg => ("error: " ^ msg, NONE)
in
@@ -87,7 +87,7 @@
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"
+ handle TimeLimit.TimeOut => "timeout"
| ERROR msg => "error: " ^ msg
fun log_metis s = log (metis_tag ^ s)
in
--- a/src/HOL/Mirabelle/lib/scripts/report.pl Fri Sep 04 15:18:35 2009 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/report.pl Fri Sep 04 15:19:51 2009 +0200
@@ -18,7 +18,7 @@
my $metis_calls = 0;
my $metis_succeeded = 0;
-my $metis_time_out = 0;
+my $metis_timeout = 0;
my $metis_time = 0;
foreach (@lines) {
@@ -39,8 +39,8 @@
$metis_succeeded++;
$metis_time += $1;
}
- if (m/^metis \(sledgehammer\): time out/) {
- $metis_time_out++;
+ if (m/^metis \(sledgehammer\): timeout/) {
+ $metis_timeout++;
}
}
@@ -57,8 +57,8 @@
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 "Percentage of successful sledgehammer calls: %.0f%%\n", $percent;
+ 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;
}
@@ -67,10 +67,12 @@
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 time outs: $metis_time_out\n";
- printf FILE "Percentage of successful metis calls: %.0f%%\n", $percent;
+ 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;
}