Mirabelle appears to work better in single-threaded mode;
authorwenzelm
Mon, 24 Sep 2012 15:37:58 +0200
changeset 505643b0a60eee56e
parent 50563 8192dc55bda9
child 50565 0a82e98fd4a3
Mirabelle appears to work better in single-threaded mode;
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
     1.1 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Sep 24 14:22:07 2012 +0200
     1.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Sep 24 15:37:58 2012 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4  if ($output_log) { print "Mirabelle: $thy_file\n"; }
     1.5  
     1.6  my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
     1.7 -  "-e 'Unsynchronized.setmp quick_and_dirty true use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
     1.8 +  "-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;
     1.9  
    1.10  if ($output_log) {
    1.11    my $outcome = ($result ? "failure" : "success");