src/HOL/Mirabelle/lib/scripts/mirabelle.pl
author blanchet
Tue, 24 Apr 2012 13:56:13 +0200
changeset 47728 6ee015f6ea4b
parent 47712 81c3c4e01263
child 47732 503efdb07566
permissions -rw-r--r--
reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
     1
#
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
     2
# Author: Jasmin Blanchette and Sascha Boehme
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
     3
#
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
     4
# Testing tool for automated proof tools.
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
     5
#
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
     6
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
     7
use File::Basename;
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
     8
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
     9
# environment
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    10
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    11
my $isabelle_home = $ENV{'ISABELLE_HOME'};
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    12
my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    13
my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    14
my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    15
my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    16
my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32498
diff changeset
    17
my $be_quiet = $ENV{'MIRABELLE_QUIET'};
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32498
diff changeset
    18
my $actions = $ENV{'MIRABELLE_ACTIONS'};
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    19
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    20
my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    21
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    22
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    23
# arguments
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    24
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32498
diff changeset
    25
my $thy_file = $ARGV[0];
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    26
my $start_line = "0";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    27
my $end_line = "~1";
32454
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32434
diff changeset
    28
if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32434
diff changeset
    29
  $thy_file = $1;
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32434
diff changeset
    30
  $start_line = $2;
a1a5589207ad Mirabelle: proper parsing of theorem names found by sledgehammer, respecting test intervals given along with file names
boehmes
parents: 32434
diff changeset
    31
  $end_line = $3;
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    32
}
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    33
my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy");
42038
626fcf4a803e fixed perl error
krauss
parents: 42037
diff changeset
    34
my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10);
42033
60350051ef93 mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)
krauss
parents: 41361
diff changeset
    35
my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix;
60350051ef93 mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)
krauss
parents: 41361
diff changeset
    36
my $new_thy_file = $path . "/" . $new_thy_name . $ext;
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    37
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    38
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    39
# setup
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    40
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    41
my $setup_thy_name = $thy_name . "_Setup";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    42
my $setup_file = $output_path . "/" . $setup_thy_name . ".thy";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    43
my $log_file = $output_path . "/" . $thy_name . ".log";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    44
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    45
my @action_files;
32396
e756600502cc keep the modified (tested) theory,
boehmes
parents: 32395
diff changeset
    46
my @action_names;
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    47
foreach (split(/:/, $actions)) {
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    48
  if (m/([^[]*)/) {
47477
3fabf352243e renamed mirabelle Tools directory to Actions, to make consistent with 'usage' description;
sultana
parents: 46824
diff changeset
    49
    push @action_files, "\"$mirabelle_home/Actions/mirabelle_$1.ML\"";
32396
e756600502cc keep the modified (tested) theory,
boehmes
parents: 32395
diff changeset
    50
    push @action_names, $1;
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    51
  }
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    52
}
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    53
my $tools = "";
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    54
if ($#action_files >= 0) {
38895
ec417f748064 deal with duplicates
blanchet
parents: 37378
diff changeset
    55
  # uniquify
ec417f748064 deal with duplicates
blanchet
parents: 37378
diff changeset
    56
  my $s = join ("\n", @action_files);
ec417f748064 deal with duplicates
blanchet
parents: 37378
diff changeset
    57
  my @action_files = split(/\n/, $s . "\n" . $s);
ec417f748064 deal with duplicates
blanchet
parents: 37378
diff changeset
    58
  %action_files = sort(@action_files);
ec417f748064 deal with duplicates
blanchet
parents: 37378
diff changeset
    59
  $tools = "uses " . join(" ", sort(keys(%action_files)));
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    60
}
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    61
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    62
open(SETUP_FILE, ">$setup_file") || die "Could not create file '$setup_file'";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    63
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    64
print SETUP_FILE <<END;
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    65
theory "$setup_thy_name"
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    66
imports "$mirabelle_thy" "$mirabelle_theory"
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    67
$tools
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    68
begin
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    69
46824
1257c80988cd added Mirabelle action info in its log file; tuned;
sultana
parents: 42070
diff changeset
    70
setup {*
37378
5449c9aafdca Adapted Mirabelle script (cf. f60e4dd6d76f)
krauss
parents: 32522
diff changeset
    71
  Config.put_global Mirabelle.logfile "$log_file" #>
5449c9aafdca Adapted Mirabelle script (cf. f60e4dd6d76f)
krauss
parents: 32522
diff changeset
    72
  Config.put_global Mirabelle.timeout $timeout #>
5449c9aafdca Adapted Mirabelle script (cf. f60e4dd6d76f)
krauss
parents: 32522
diff changeset
    73
  Config.put_global Mirabelle.start_line $start_line #>
5449c9aafdca Adapted Mirabelle script (cf. f60e4dd6d76f)
krauss
parents: 32522
diff changeset
    74
  Config.put_global Mirabelle.end_line $end_line
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    75
*}
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    76
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    77
END
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    78
46824
1257c80988cd added Mirabelle action info in its log file; tuned;
sultana
parents: 42070
diff changeset
    79
@action_list = split(/:/, $actions);
1257c80988cd added Mirabelle action info in its log file; tuned;
sultana
parents: 42070
diff changeset
    80
1257c80988cd added Mirabelle action info in its log file; tuned;
sultana
parents: 42070
diff changeset
    81
foreach (reverse(@action_list)) {
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    82
  if (m/([^[]*)(?:\[(.*)\])?/) {
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    83
    my ($name, $settings_str) = ($1, $2 || "");
32385
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    84
    $name =~ s/^([a-z])/\U$1/;
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents: 32383
diff changeset
    85
    print SETUP_FILE "setup {* Mirabelle_$name.invoke [";
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    86
    my $sep = "";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    87
    foreach (split(/,/, $settings_str)) {
41361
d1e4a20911cb better parsing of options, in case the value has '='
blanchet
parents: 38898
diff changeset
    88
      if (m/\s*([^=]*)\s*=\s*(.*)\s*/) {
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    89
        print SETUP_FILE "$sep(\"$1\", \"$2\")";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    90
        $sep = ", ";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    91
      }
32522
1b70db55c811 Mirabelle: command-line action options may either be key=value or just key
boehmes
parents: 32521
diff changeset
    92
      elsif (m/\s*(.*)\s*/) {
46824
1257c80988cd added Mirabelle action info in its log file; tuned;
sultana
parents: 42070
diff changeset
    93
        print SETUP_FILE "$sep(\"$1\", \"\")";
1257c80988cd added Mirabelle action info in its log file; tuned;
sultana
parents: 42070
diff changeset
    94
        $sep = ", ";
32522
1b70db55c811 Mirabelle: command-line action options may either be key=value or just key
boehmes
parents: 32521
diff changeset
    95
      }
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    96
    }
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    97
    print SETUP_FILE "] *}\n";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    98
  }
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
    99
}
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   100
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   101
print SETUP_FILE "\nend";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   102
close SETUP_FILE;
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   103
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   104
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   105
# modify target theory file
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   106
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   107
open(OLD_FILE, "<$thy_file") || die "Cannot open file '$thy_file'";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   108
my @lines = <OLD_FILE>;
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   109
close(OLD_FILE);
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   110
47728
6ee015f6ea4b reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path
blanchet
parents: 47712
diff changeset
   111
my $setup_import =
6ee015f6ea4b reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path
blanchet
parents: 47712
diff changeset
   112
  substr("\"$output_path\/$setup_thy_name\"" . (" " x 1000), 0, 1000);
6ee015f6ea4b reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path
blanchet
parents: 47712
diff changeset
   113
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   114
my $thy_text = join("", @lines);
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   115
my $old_len = length($thy_text);
32395
9692b0714295 do not introduce additional newlines
boehmes
parents: 32385
diff changeset
   116
$thy_text =~ s/(theory\s+)\"?$thy_name\"?/$1"$new_thy_name"/g;
47728
6ee015f6ea4b reintroduce file offsets in Mirabelle output, but make sure they are not influenced by the length of the path
blanchet
parents: 47712
diff changeset
   117
$thy_text =~ s/(imports)(\s+)/$1 $setup_import$2/g;
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   118
die "No 'imports' found" if length($thy_text) == $old_len;
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   119
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   120
open(NEW_FILE, ">$new_thy_file") || die "Cannot create file '$new_thy_file'";
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   121
print NEW_FILE $thy_text;
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   122
close(NEW_FILE);
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   123
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   124
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   125
# run isabelle
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   126
32396
e756600502cc keep the modified (tested) theory,
boehmes
parents: 32395
diff changeset
   127
open(LOG_FILE, ">$log_file");
e756600502cc keep the modified (tested) theory,
boehmes
parents: 32395
diff changeset
   128
print LOG_FILE "Run of $new_thy_file with:\n";
46824
1257c80988cd added Mirabelle action info in its log file; tuned;
sultana
parents: 42070
diff changeset
   129
foreach $action  (@action_list) {
1257c80988cd added Mirabelle action info in its log file; tuned;
sultana
parents: 42070
diff changeset
   130
  print LOG_FILE "  $action\n";
32396
e756600502cc keep the modified (tested) theory,
boehmes
parents: 32395
diff changeset
   131
}
e756600502cc keep the modified (tested) theory,
boehmes
parents: 32395
diff changeset
   132
close(LOG_FILE);
e756600502cc keep the modified (tested) theory,
boehmes
parents: 32395
diff changeset
   133
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32498
diff changeset
   134
my $quiet = "";
42070
d3404f32328a really be quiet
boehmes
parents: 42038
diff changeset
   135
my $output_log = 1;
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32498
diff changeset
   136
if (defined $be_quiet and $be_quiet ne "") {
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32498
diff changeset
   137
  $quiet = " > /dev/null 2>&1";
42070
d3404f32328a really be quiet
boehmes
parents: 42038
diff changeset
   138
  $output_log = 0;
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32498
diff changeset
   139
}
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   140
42070
d3404f32328a really be quiet
boehmes
parents: 42038
diff changeset
   141
if ($output_log) { print "Mirabelle: $thy_file\n"; }
32498
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   142
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32498
diff changeset
   143
my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
47712
81c3c4e01263 run Mirabelle in quick and dirty mode
blanchet
parents: 47477
diff changeset
   144
  "-e 'Unsynchronized.setmp quick_and_dirty true use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
32521
f20cc66b2c74 added initialization and cleanup of actions,
boehmes
parents: 32498
diff changeset
   145
42070
d3404f32328a really be quiet
boehmes
parents: 42038
diff changeset
   146
if ($output_log) { print "Finished:  $thy_file\n"; }
32498
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   147
1132c7c13f36 Mirabelle: actions are responsible for handling exceptions,
boehmes
parents: 32496
diff changeset
   148
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   149
# cleanup
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   150
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   151
unlink $setup_file;
42033
60350051ef93 mirabelle: create modified theory file in original location, to ensure that its dependencies can be found (cf. aa8dce9ab8a9)
krauss
parents: 41361
diff changeset
   152
unlink $new_thy_file;
32382
98674ac811c4 Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff changeset
   153
42034
a77df5241959 propagate mirabelle failures properly;
krauss
parents: 42033
diff changeset
   154
exit ($result ? 1 : 0);