# HG changeset patch
# User haftmann
# Date 1252070391 -7200
# Node ID 4942abb40a55d5c6d5fd9b2839d00bcdb90a036a
# Parent  e3c4e337196c5bbd1d529a3a69c72689e0d1d616# Parent  e9644b497e1cb3f2e62aa1e4eef6e479c46129ed
merged

diff -r e9644b497e1c -r 4942abb40a55 src/HOL/IsaMakefile
--- 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 \
diff -r e9644b497e1c -r 4942abb40a55 src/HOL/Mirabelle/MirabelleTest.thy
--- 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
diff -r e9644b497e1c -r 4942abb40a55 src/HOL/Mirabelle/Mirabelle_Test.thy
--- /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
diff -r e9644b497e1c -r 4942abb40a55 src/HOL/Mirabelle/ROOT.ML
--- 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";
diff -r e9644b497e1c -r 4942abb40a55 src/HOL/Mirabelle/Tools/mirabelle_arith.ML
--- 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)
 
diff -r e9644b497e1c -r 4942abb40a55 src/HOL/Mirabelle/Tools/mirabelle_metis.ML
--- 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)
 
diff -r e9644b497e1c -r 4942abb40a55 src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
--- 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))
diff -r e9644b497e1c -r 4942abb40a55 src/HOL/Mirabelle/Tools/mirabelle_refute.ML
--- 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)"
diff -r e9644b497e1c -r 4942abb40a55 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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
diff -r e9644b497e1c -r 4942abb40a55 src/HOL/Mirabelle/lib/scripts/report.pl
--- 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;
 }