src/HOL/Mirabelle/lib/scripts/mirabelle.pl
changeset 66156 f54c32c413a9
parent 62779 7737e26cd3c6
equal deleted inserted replaced
66155:2463cba9f18f 66156:f54c32c413a9
     8 
     8 
     9 # environment
     9 # environment
    10 
    10 
    11 my $isabelle_home = $ENV{'ISABELLE_HOME'};
    11 my $isabelle_home = $ENV{'ISABELLE_HOME'};
    12 my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
    12 my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
       
    13 my $mirabelle_dir = $ENV{'MIRABELLE_DIR'};
    13 my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
    14 my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
    14 my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
    15 my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
    15 my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
    16 my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
    16 my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
    17 my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
    17 my $be_quiet = $ENV{'MIRABELLE_QUIET'};
    18 my $be_quiet = $ENV{'MIRABELLE_QUIET'};
   158 
   159 
   159 if ($output_log) { print "Mirabelle: $thy_file\n"; }
   160 if ($output_log) { print "Mirabelle: $thy_file\n"; }
   160 
   161 
   161 my $cmd =
   162 my $cmd =
   162   "isabelle process -o quick_and_dirty -o threads=1" .
   163   "isabelle process -o quick_and_dirty -o threads=1" .
   163   " -T \"$path/$new_thy_name\" -l $mirabelle_logic" . $quiet;
   164   " -T \"$path/$new_thy_name\" " .
       
   165   ($mirabelle_dir ? "-d " . $mirabelle_dir . " " : "") .
       
   166   "-l $mirabelle_logic" . $quiet;
   164 my $result = system "bash", "-c", $cmd;
   167 my $result = system "bash", "-c", $cmd;
   165 
   168 
   166 if ($output_log) {
   169 if ($output_log) {
   167   my $outcome = ($result ? "failure" : "success");
   170   my $outcome = ($result ? "failure" : "success");
   168   print "\nFinished:  $thy_file  [$outcome]\n";
   171   print "\nFinished:  $thy_file  [$outcome]\n";