author | wenzelm |
Thu, 11 Feb 2016 22:05:12 +0100 | |
changeset 62282 | 45adb8dc84e1 |
parent 54717 | 42c209a6c225 |
child 62475 | 43e64c770f28 |
permissions | -rw-r--r-- |
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 | 17 |
my $be_quiet = $ENV{'MIRABELLE_QUIET'}; |
48703
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
18 |
my $user_setup_file = $ENV{'MIRABELLE_SETUP_FILE'}; |
32521 | 19 |
my $actions = $ENV{'MIRABELLE_ACTIONS'}; |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
20 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
21 |
my $mirabelle_thy = $mirabelle_home . "/Mirabelle"; |
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 |
|
48703
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
24 |
# argument |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
25 |
|
32521 | 26 |
my $thy_file = $ARGV[0]; |
48703
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
27 |
|
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
28 |
my ($thy_name, $path, $ext) = fileparse($thy_file, ".thy"); |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
29 |
my $rand_suffix = join('', map { ('a'..'z')[rand(26)] } 1 .. 10); |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
30 |
my $new_thy_name = $thy_name . "_Mirabelle_" . $rand_suffix; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
31 |
my $new_thy_file = $path . "/" . $new_thy_name . $ext; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
32 |
|
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
33 |
|
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
34 |
# setup |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
35 |
|
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
36 |
my $setup_file; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
37 |
my $setup_full_name; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
38 |
|
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
39 |
if (-e $user_setup_file) { |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
40 |
$setup_file = undef; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
41 |
my ($name, $path, $ext) = fileparse($user_setup_file, ".thy"); |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
42 |
$setup_full_name = $path . "/" . $name; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
43 |
} |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
44 |
else { |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
45 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
46 |
my $start_line = "0"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
47 |
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
|
48 |
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
|
49 |
$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
|
50 |
$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
|
51 |
$end_line = $3; |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
52 |
} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
53 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
54 |
my $setup_thy_name = $thy_name . "_Setup"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
55 |
my $setup_file = $output_path . "/" . $setup_thy_name . ".thy"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
56 |
my $log_file = $output_path . "/" . $thy_name . ".log"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
57 |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
58 |
my @action_files; |
32396 | 59 |
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
|
60 |
foreach (split(/:/, $actions)) { |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
61 |
if (m/([^[]*)/) { |
47730 | 62 |
push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\""; |
32396 | 63 |
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
|
64 |
} |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
65 |
} |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
66 |
my $tools = ""; |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
67 |
if ($#action_files >= 0) { |
38895 | 68 |
# uniquify |
69 |
my $s = join ("\n", @action_files); |
|
70 |
my @action_files = split(/\n/, $s . "\n" . $s); |
|
71 |
%action_files = sort(@action_files); |
|
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
49549
diff
changeset
|
72 |
$tools = join("", map { "ML_file " . $_ . "\n" } (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
|
73 |
} |
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
74 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
75 |
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
|
76 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
77 |
print SETUP_FILE <<END; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
78 |
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
|
79 |
imports "$mirabelle_thy" "$mirabelle_theory" |
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
49549
diff
changeset
|
80 |
begin |
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
49549
diff
changeset
|
81 |
|
32385
594890623c46
split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL)
boehmes
parents:
32383
diff
changeset
|
82 |
$tools |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
83 |
|
46824
1257c80988cd
added Mirabelle action info in its log file; tuned;
sultana
parents:
42070
diff
changeset
|
84 |
setup {* |
37378 | 85 |
Config.put_global Mirabelle.logfile "$log_file" #> |
86 |
Config.put_global Mirabelle.timeout $timeout #> |
|
87 |
Config.put_global Mirabelle.start_line $start_line #> |
|
88 |
Config.put_global Mirabelle.end_line $end_line |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
89 |
*} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
90 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
91 |
END |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
92 |
|
46824
1257c80988cd
added Mirabelle action info in its log file; tuned;
sultana
parents:
42070
diff
changeset
|
93 |
@action_list = split(/:/, $actions); |
1257c80988cd
added Mirabelle action info in its log file; tuned;
sultana
parents:
42070
diff
changeset
|
94 |
|
1257c80988cd
added Mirabelle action info in its log file; tuned;
sultana
parents:
42070
diff
changeset
|
95 |
foreach (reverse(@action_list)) { |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
96 |
if (m/([^[]*)(?:\[(.*)\])?/) { |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
97 |
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
|
98 |
$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
|
99 |
print SETUP_FILE "setup {* Mirabelle_$name.invoke ["; |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
100 |
my $sep = ""; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
101 |
foreach (split(/,/, $settings_str)) { |
41361
d1e4a20911cb
better parsing of options, in case the value has '='
blanchet
parents:
38898
diff
changeset
|
102 |
if (m/\s*([^=]*)\s*=\s*(.*)\s*/) { |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
103 |
print SETUP_FILE "$sep(\"$1\", \"$2\")"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
104 |
$sep = ", "; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
105 |
} |
32522
1b70db55c811
Mirabelle: command-line action options may either be key=value or just key
boehmes
parents:
32521
diff
changeset
|
106 |
elsif (m/\s*(.*)\s*/) { |
46824
1257c80988cd
added Mirabelle action info in its log file; tuned;
sultana
parents:
42070
diff
changeset
|
107 |
print SETUP_FILE "$sep(\"$1\", \"\")"; |
1257c80988cd
added Mirabelle action info in its log file; tuned;
sultana
parents:
42070
diff
changeset
|
108 |
$sep = ", "; |
32522
1b70db55c811
Mirabelle: command-line action options may either be key=value or just key
boehmes
parents:
32521
diff
changeset
|
109 |
} |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
110 |
} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
111 |
print SETUP_FILE "] *}\n"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
112 |
} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
113 |
} |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
114 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
115 |
print SETUP_FILE "\nend"; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
116 |
close SETUP_FILE; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
117 |
|
48703
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
118 |
$setup_full_name = $output_path . "/" . $setup_thy_name; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
119 |
|
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
120 |
open(LOG_FILE, ">$log_file"); |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
121 |
print LOG_FILE "Run of $new_thy_file with:\n"; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
122 |
foreach $action (@action_list) { |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
123 |
print LOG_FILE " $action\n"; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
124 |
} |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
125 |
close(LOG_FILE); |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
126 |
|
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
127 |
} |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
128 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
129 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
130 |
# modify target theory file |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
131 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
132 |
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
|
133 |
my @lines = <OLD_FILE>; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
134 |
close(OLD_FILE); |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
135 |
|
48703
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
136 |
my $setup_import = substr("\"$setup_full_name\"" . (" " x 1000), 0, 1000); |
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
|
137 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
138 |
my $thy_text = join("", @lines); |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
139 |
my $old_len = length($thy_text); |
32395 | 140 |
$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
|
141 |
$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
|
142 |
die "No 'imports' found" if length($thy_text) == $old_len; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
143 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
144 |
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
|
145 |
print NEW_FILE $thy_text; |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
146 |
close(NEW_FILE); |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
147 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
148 |
|
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
149 |
# run isabelle |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
150 |
|
32521 | 151 |
my $quiet = ""; |
42070 | 152 |
my $output_log = 1; |
32521 | 153 |
if (defined $be_quiet and $be_quiet ne "") { |
154 |
$quiet = " > /dev/null 2>&1"; |
|
42070 | 155 |
$output_log = 0; |
32521 | 156 |
} |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
157 |
|
42070 | 158 |
if ($output_log) { print "Mirabelle: $thy_file\n"; } |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
159 |
|
62282
45adb8dc84e1
invoke perl system with explicit list -- to avoid extra /bin/sh and thus evade potential conflict of /bin/sh -> dash with bash on Debian/Ubuntu;
wenzelm
parents:
54717
diff
changeset
|
160 |
my $cmd = |
45adb8dc84e1
invoke perl system with explicit list -- to avoid extra /bin/sh and thus evade potential conflict of /bin/sh -> dash with bash on Debian/Ubuntu;
wenzelm
parents:
54717
diff
changeset
|
161 |
"\"$ENV{'ISABELLE_PROCESS'}\" " . |
45adb8dc84e1
invoke perl system with explicit list -- to avoid extra /bin/sh and thus evade potential conflict of /bin/sh -> dash with bash on Debian/Ubuntu;
wenzelm
parents:
54717
diff
changeset
|
162 |
"-o quick_and_dirty -e 'Multithreading.max_threads_setmp 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . |
45adb8dc84e1
invoke perl system with explicit list -- to avoid extra /bin/sh and thus evade potential conflict of /bin/sh -> dash with bash on Debian/Ubuntu;
wenzelm
parents:
54717
diff
changeset
|
163 |
$quiet; |
45adb8dc84e1
invoke perl system with explicit list -- to avoid extra /bin/sh and thus evade potential conflict of /bin/sh -> dash with bash on Debian/Ubuntu;
wenzelm
parents:
54717
diff
changeset
|
164 |
my $result = system "bash", "-c", $cmd; |
32521 | 165 |
|
48703
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
166 |
if ($output_log) { |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
167 |
my $outcome = ($result ? "failure" : "success"); |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
168 |
print "\nFinished: $thy_file [$outcome]\n"; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
169 |
} |
32498
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
170 |
|
1132c7c13f36
Mirabelle: actions are responsible for handling exceptions,
boehmes
parents:
32496
diff
changeset
|
171 |
|
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
172 |
# cleanup |
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
173 |
|
48703
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
174 |
if (defined $setup_file) { |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
175 |
unlink $setup_file; |
d408ff0abf23
extended Mirabelle to support user-provided setup files which contain the configuration for a Mirabelle run (avoids some layers of scripts and reduces the complexity of the overall Mirabelle setup)
boehmes
parents:
47732
diff
changeset
|
176 |
} |
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
|
177 |
unlink $new_thy_file; |
32382
98674ac811c4
Mirabelle tool script conforming to standard Isabelle tool interface,
boehmes
parents:
diff
changeset
|
178 |
|
42034 | 179 |
exit ($result ? 1 : 0); |