src/HOL/Mirabelle/lib/scripts/mirabelle.pl
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 51293 05b1bbae748d
child 52059 2f970c7f722b
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
     1 #
     2 # Author: Jasmin Blanchette and Sascha Boehme
     3 #
     4 # Testing tool for automated proof tools.
     5 #
     6 
     7 use File::Basename;
     8 
     9 # environment
    10 
    11 my $isabelle_home = $ENV{'ISABELLE_HOME'};
    12 my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
    13 my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
    14 my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
    15 my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
    16 my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
    17 my $be_quiet = $ENV{'MIRABELLE_QUIET'};
    18 my $user_setup_file = $ENV{'MIRABELLE_SETUP_FILE'};
    19 my $actions = $ENV{'MIRABELLE_ACTIONS'};
    20 
    21 my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
    22 
    23 
    24 # argument
    25 
    26 my $thy_file = $ARGV[0];
    27 
    28 my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
    29 my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10);
    30 my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix;
    31 my $new_thy_file = $path . "/" . $new_thy_name . $ext;
    32 
    33 
    34 # setup
    35 
    36 my $setup_file;
    37 my $setup_full_name;
    38 
    39 if (-e $user_setup_file) {
    40   $setup_file = undef;
    41   my ($name, $path, $ext) = fileparse($user_setup_file, ".thy");
    42   $setup_full_name = $path . "/" . $name;
    43 }
    44 else {
    45 
    46 my $start_line = "0";
    47 my $end_line = "~1";
    48 if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
    49   $thy_file = $1;
    50   $start_line = $2;
    51   $end_line = $3;
    52 }
    53 
    54 my $setup_thy_name = $thy_name . "_Setup";
    55 my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
    56 my $log_file = $output_path . "/" . $thy_name . ".log";
    57 
    58 my @action_files;
    59 my @action_names;
    60 foreach (split(/:/, $actions)) {
    61   if (m/([^[]*)/) {
    62     push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
    63     push @action_names, $1;
    64   }
    65 }
    66 my $tools = "";
    67 if ($#action_files >= 0) {
    68   # uniquify
    69   my $s = join ("\n", @action_files);
    70   my @action_files = split(/\n/, $s . "\n" . $s);
    71   %action_files = sort(@action_files);
    72   $tools = join("", map { "ML_file " . $_ . "\n" } (sort(keys(%action_files))));
    73 }
    74 
    75 open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
    76 
    77 print SETUP_FILE <<END;
    78 theory "$setup_thy_name"
    79 imports "$mirabelle_thy" "$mirabelle_theory"
    80 begin
    81 
    82 $tools
    83 
    84 setup {*
    85   Config.put_global Mirabelle.logfile "$log_file" #>
    86   Config.put_global Mirabelle.timeout $timeout #>
    87   Config.put_global Mirabelle.start_line $start_line #>
    88   Config.put_global Mirabelle.end_line $end_line
    89 *}
    90 
    91 END
    92 
    93 @action_list = split(/:/, $actions);
    94 
    95 foreach (reverse(@action_list)) {
    96   if (m/([^[]*)(?:\[(.*)\])?/) {
    97     my ($name, $settings_str) = ($1, $2 || "");
    98     $name =~ s/^([a-z])/\U$1/;
    99     print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
   100     my $sep = "";
   101     foreach (split(/,/, $settings_str)) {
   102       if (m/\s*([^=]*)\s*=\s*(.*)\s*/) {
   103         print SETUP_FILE "$sep(\"$1\", \"$2\")";
   104         $sep = ", ";
   105       }
   106       elsif (m/\s*(.*)\s*/) {
   107         print SETUP_FILE "$sep(\"$1\", \"\")";
   108         $sep = ", ";
   109       }
   110     }
   111     print SETUP_FILE "] *}\n";
   112   }
   113 }
   114 
   115 print SETUP_FILE "\nend";
   116 close SETUP_FILE;
   117 
   118 $setup_full_name = $output_path . "/" . $setup_thy_name;
   119 
   120 open(LOG_FILE, ">$log_file");
   121 print LOG_FILE "Run of $new_thy_file with:\n";
   122 foreach $action  (@action_list) {
   123   print LOG_FILE "  $action\n";
   124 }
   125 close(LOG_FILE);
   126 
   127 }
   128 
   129 
   130 # modify target theory file
   131 
   132 open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
   133 my @lines = <OLD_FILE>;
   134 close(OLD_FILE);
   135 
   136 my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000);
   137 
   138 my $thy_text = join("", @lines);
   139 my $old_len = length($thy_text);
   140 $thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
   141 $thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g;
   142 die "No 'imports' found" if length($thy_text) == $old_len;
   143 
   144 open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
   145 print NEW_FILE $thy_text;
   146 close(NEW_FILE);
   147 
   148 
   149 # run isabelle
   150 
   151 my $quiet = "";
   152 my $output_log = 1;
   153 if (defined $be_quiet and $be_quiet ne "") {
   154   $quiet = " > /dev/null 2>&1";
   155   $output_log = 0;
   156 }
   157 
   158 if ($output_log) { print "Mirabelle: $thy_file\n"; }
   159 
   160 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
   161   "-e 'Unsynchronized.setmp Multithreading.max_threads 1 (Unsynchronized.setmp quick_and_dirty true use_thy) \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
   162 
   163 if ($output_log) {
   164   my $outcome = ($result ? "failure" : "success");
   165   print "\nFinished:  $thy_file  [$outcome]\n";
   166 }
   167 
   168 
   169 # cleanup
   170 
   171 if (defined $setup_file) {
   172   unlink $setup_file;
   173 }
   174 unlink $new_thy_file;
   175 
   176 exit ($result ? 1 : 0);