equal
deleted
inserted
replaced
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"; |