propagate mirabelle failures properly;
authorkrauss
Mon Mar 21 12:43:25 2011 +0100 (2011-03-21)
changeset 42034a77df5241959
parent 42033 60350051ef93
child 42035 fb155c75072d
propagate mirabelle failures properly;
flatten obscure return code semantics of Perl system command to 0/1
src/HOL/Mirabelle/lib/Tools/mirabelle
src/HOL/Mirabelle/lib/scripts/mirabelle.pl
     1.1 --- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Mon Mar 21 12:43:23 2011 +0100
     1.2 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Mon Mar 21 12:43:25 2011 +0100
     1.3 @@ -56,6 +56,12 @@
     1.4    exit 1
     1.5  }
     1.6  
     1.7 +function fail()
     1.8 +{
     1.9 +  echo "$1" >&2
    1.10 +  exit 2
    1.11 +}
    1.12 +
    1.13  
    1.14  ## process command line
    1.15  
    1.16 @@ -103,6 +109,6 @@
    1.17  
    1.18  for FILE in "$@"
    1.19  do
    1.20 -  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE"
    1.21 +  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed."
    1.22  done
    1.23  
     2.1 --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 12:43:23 2011 +0100
     2.2 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Mar 21 12:43:25 2011 +0100
     2.3 @@ -118,7 +118,7 @@
     2.4  
     2.5  my $root_file = "$output_path/ROOT_$thy_name.ML";
     2.6  open(ROOT_FILE, ">$root_file") || die "Cannot create file '$root_file'";
     2.7 -print ROOT_FILE "use_thy \"$path/$new_thy_name\";\n";
     2.8 +print ROOT_FILE "use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n";
     2.9  close(ROOT_FILE);
    2.10  
    2.11  
    2.12 @@ -150,4 +150,4 @@
    2.13  unlink $setup_file;
    2.14  unlink $new_thy_file;
    2.15  
    2.16 -exit $result;
    2.17 +exit ($result ? 1 : 0);