# HG changeset patch
# User boehmes
# Date 1344328084 -7200
# Node ID d408ff0abf2381527534bf0d1217054e7940f0f6
# Parent  e1752ccccc34921ea87b09749608ad0dd3ee127d
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)

diff -r e1752ccccc34 -r d408ff0abf23 src/HOL/Mirabelle/lib/Tools/mirabelle
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Aug 07 10:28:04 2012 +0200
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Aug 07 10:28:04 2012 +0200
@@ -32,6 +32,7 @@
   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 "    -S FILE      user-provided setup file (no actions required)"
   echo
   echo "  Apply the given actions (i.e., automated proof tools)"
   echo "  at all proof steps in the given theory files."
@@ -63,7 +64,9 @@
 
 [ $# -eq 0 ] && usage
 
-while getopts "L:T:O:t:q?" OPT
+MIRABELLE_SETUP_FILE=
+
+while getopts "L:T:O:t:S:q?" OPT
 do
   case "$OPT" in
     L)
@@ -78,6 +81,9 @@
     t)
       MIRABELLE_TIMEOUT="$OPTARG"
       ;;
+    S)
+      MIRABELLE_SETUP_FILE="$OPTARG"
+      ;;
     q)
       MIRABELLE_QUIET="true"
       ;;
@@ -87,6 +93,7 @@
   esac
 done
 
+export MIRABELLE_SETUP_FILE
 export MIRABELLE_QUIET
 
 shift $(($OPTIND - 1))
diff -r e1752ccccc34 -r d408ff0abf23 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Aug 07 10:28:04 2012 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Aug 07 10:28:04 2012 +0200
@@ -15,14 +15,34 @@
 my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
 my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
 my $be_quiet = $ENV{'MIRABELLE_QUIET'};
+my $user_setup_file = $ENV{'MIRABELLE_SETUP_FILE'};
 my $actions = $ENV{'MIRABELLE_ACTIONS'};
 
 my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
 
 
-# arguments
+# argument
 
 my $thy_file = $ARGV[0];
+
+my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
+my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10);
+my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix;
+my $new_thy_file = $path . "/" . $new_thy_name . $ext;
+
+
+# setup
+
+my $setup_file;
+my $setup_full_name;
+
+if (-e $user_setup_file) {
+  $setup_file = undef;
+  my ($name, $path, $ext) = fileparse($user_setup_file, ".thy");
+  $setup_full_name = $path . "/" . $name;
+}
+else {
+
 my $start_line = "0";
 my $end_line = "~1";
 if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
@@ -30,13 +50,6 @@
   $start_line = $2;
   $end_line = $3;
 }
-my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
-my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10);
-my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix;
-my $new_thy_file = $path . "/" . $new_thy_name . $ext;
-
-
-# setup
 
 my $setup_thy_name = $thy_name . "_Setup";
 my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
@@ -101,6 +114,17 @@
 print SETUP_FILE "\nend";
 close SETUP_FILE;
 
+$setup_full_name = $output_path . "/" . $setup_thy_name;
+
+open(LOG_FILE, ">$log_file");
+print LOG_FILE "Run of $new_thy_file with:\n";
+foreach $action  (@action_list) {
+  print LOG_FILE "  $action\n";
+}
+close(LOG_FILE);
+
+}
+
 
 # modify target theory file
 
@@ -108,8 +132,7 @@
 my @lines = <OLD_FILE>;
 close(OLD_FILE);
 
-my $setup_import =
-  substr("\"$output_path\/$setup_thy_name\"" . (" " x 1000), 0, 1000);
+my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000);
 
 my $thy_text = join("", @lines);
 my $old_len = length($thy_text);
@@ -124,13 +147,6 @@
 
 # run isabelle
 
-open(LOG_FILE, ">$log_file");
-print LOG_FILE "Run of $new_thy_file with:\n";
-foreach $action  (@action_list) {
-  print LOG_FILE "  $action\n";
-}
-close(LOG_FILE);
-
 my $quiet = "";
 my $output_log = 1;
 if (defined $be_quiet and $be_quiet ne "") {
@@ -143,12 +159,17 @@
 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
   "-e 'Unsynchronized.setmp quick_and_dirty true use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
 
-if ($output_log) { print "Finished:  $thy_file\n"; }
+if ($output_log) {
+  my $outcome = ($result ? "failure" : "success");
+  print "\nFinished:  $thy_file  [$outcome]\n";
+}
 
 
 # cleanup
 
-unlink $setup_file;
+if (defined $setup_file) {
+  unlink $setup_file;
+}
 unlink $new_thy_file;
 
 exit ($result ? 1 : 0);