# HG changeset patch
# User boehmes
# Date 1251919996 -7200
# Node ID 909a6447700a3d49f8dcb57d5966eca7041068c2
# Parent  1132c7c13f36994c1a3fb1e1718c76111ec94911
add report script for Mirabelle

diff -r 1132c7c13f36 -r 909a6447700a src/HOL/Mirabelle/lib/scripts/report.pl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/lib/scripts/report.pl	Wed Sep 02 21:33:16 2009 +0200
@@ -0,0 +1,69 @@
+#
+# 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_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;
+  }
+}
+
+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;
+  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 "Total time for successful sledgehammer calls: $time seconds\n\n";
+}
+
+if ($metis_calls > 0) {
+  my $percent = $metis_succeeded / $metis_calls * 100;
+  my $time = $metis_time / 1000;
+  print FILE "Total number of metis calls: $metis_calls\n";
+  print FILE "Number of successful metis calls: $metis_succeeded\n";
+  printf FILE "Percentage of successful metis calls: %.0f%%\n", $percent;
+  print FILE "Total time for successful metis calls: $time seconds\n";
+}
+
+close(FILE);