src/HOL/Mirabelle/lib/scripts/mirabelle.pl
changeset 54717 42c209a6c225
parent 52059 2f970c7f722b
child 62282 45adb8dc84e1
equal deleted inserted replaced
54713:6666fc0b9ebc 54717:42c209a6c225
   156 }
   156 }
   157 
   157 
   158 if ($output_log) { print "Mirabelle: $thy_file\n"; }
   158 if ($output_log) { print "Mirabelle: $thy_file\n"; }
   159 
   159 
   160 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
   160 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
   161   "-o quick_and_dirty -e 'Unsynchronized.setmp Multithreading.max_threads 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
   161   "-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
   162 
   162 
   163 if ($output_log) {
   163 if ($output_log) {
   164   my $outcome = ($result ? "failure" : "success");
   164   my $outcome = ($result ? "failure" : "success");
   165   print "\nFinished:  $thy_file  [$outcome]\n";
   165   print "\nFinished:  $thy_file  [$outcome]\n";
   166 }
   166 }