author  blanchet 
Thu, 22 Apr 2010 10:13:02 +0200  
changeset 36284  0e24322474a4 
parent 36283  25e69e93954d 
child 36286  fa6d03d42aab 
permissions  rwrr 
32327
0971cc0b6a57
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
wenzelm
parents:
32257
diff
changeset

1 
(* Title: HOL/Tools/ATP_Manager/atp_wrapper.ML 
28592  2 
Author: Fabian Immler, TU Muenchen 
3 

4 
Wrapper functions for external ATPs. 

5 
*) 

6 

7 
signature ATP_WRAPPER = 

8 
sig 

35867  9 
type prover = ATP_Manager.prover 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

10 

35867  11 
(* hooks for problem files *) 
12 
val destdir : string Config.T 

13 
val problem_prefix : string Config.T 

14 
val measure_runtime : bool Config.T 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

15 

35867  16 
val refresh_systems_on_tptp : unit > unit 
17 
val setup : theory > theory 

28592  18 
end; 
19 

35865  20 
structure ATP_Wrapper : ATP_WRAPPER = 
28592  21 
struct 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

22 

36187  23 
open Sledgehammer_Util 
35969  24 
open Sledgehammer_Fact_Preprocessor 
35865  25 
open Sledgehammer_HOL_Clause 
26 
open Sledgehammer_Fact_Filter 

27 
open Sledgehammer_Proof_Reconstruct 

35867  28 
open ATP_Manager 
35826  29 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

30 
(** generic ATP wrapper **) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

31 

32944
ecc0705174c2
clarified File.platform_path vs. File.shell_path;
wenzelm
parents:
32942
diff
changeset

32 
(* external problem files *) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

33 

36001  34 
val (destdir, destdir_setup) = Attrib.config_string "atp_destdir" (K ""); 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

35 
(*Empty string means create files in Isabelle's temporary files directory.*) 
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

36 

a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

37 
val (problem_prefix, problem_prefix_setup) = 
36001  38 
Attrib.config_string "atp_problem_prefix" (K "prob"); 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

39 

33247  40 
val (measure_runtime, measure_runtime_setup) = 
36001  41 
Attrib.config_bool "atp_measure_runtime" (K false); 
33247  42 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

43 

35867  44 
(* prover configuration *) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

45 

32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

46 
type prover_config = 
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

47 
{command: Path.T, 
35969  48 
arguments: Time.time > string, 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

49 
known_failures: (string list * string) list, 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

50 
max_new_clauses: int, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

51 
prefers_theory_relevant: bool, 
35969  52 
supports_isar_proofs: bool}; 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

53 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

54 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

55 
(* basic template *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

56 

32458
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

57 
fun with_path cleanup after f path = 
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

58 
Exn.capture f path 
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

59 
> tap (fn _ => cleanup path) 
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

60 
> Exn.release 
32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

61 
> tap (after path); 
32458
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

62 

36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

63 
fun find_known_failure known_failures proof = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

64 
case map_filter (fn (patterns, message) => 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

65 
if exists (fn pattern => String.isSubstring pattern proof) 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

66 
patterns then 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

67 
SOME message 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

68 
else 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

69 
NONE) known_failures of 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

70 
[] => if is_proof_well_formed proof then "" 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

71 
else "Error: The ATP output is illformed." 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

72 
 (message :: _) => message 
35865  73 

36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

74 
fun generic_prover overlord get_facts prepare write_file cmd args known_failures 
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset

75 
proof_text name ({debug, full_types, explicit_apply, ...} : params) 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36265
diff
changeset

76 
minimize_command 
35969  77 
({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} 
78 
: problem) = 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

79 
let 
31750  80 
(* get clauses and prepare them for writing *) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

81 
val (ctxt, (chain_ths, th)) = goal; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

82 
val thy = ProofContext.theory_of ctxt; 
35865  83 
val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths; 
35969  84 
val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal); 
31752
19a5f1c8a844
use results of relevancefilter to determine additional clauses;
immler@in.tum.de
parents:
31751
diff
changeset

85 
val the_filtered_clauses = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

86 
(case filtered_clauses of 
35969  87 
NONE => get_facts relevance_override goal goal_cls 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

88 
 SOME fcls => fcls); 
31409
d8537ba165b5
split preparing clauses and writing problemfile;
immler@in.tum.de
parents:
31368
diff
changeset

89 
val the_axiom_clauses = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

90 
(case axiom_clauses of 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

91 
NONE => the_filtered_clauses 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

92 
 SOME axcls => axcls); 
35969  93 
val (internal_thm_names, clauses) = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

94 
prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy; 
31750  95 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

96 
(* path to unique problem file *) 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

97 
val destdir' = if overlord then getenv "ISABELLE_HOME_USER" 
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

98 
else Config.get ctxt destdir; 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

99 
val problem_prefix' = Config.get ctxt problem_prefix; 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

100 
fun prob_pathname nr = 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

101 
let 
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

102 
val probfile = 
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

103 
Path.basic (problem_prefix' ^ 
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

104 
(if overlord then "_" ^ name else serial_string ()) 
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

105 
^ "_" ^ string_of_int nr) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

106 
in 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

107 
if destdir' = "" then File.tmp_path probfile 
35570
0e30eef52d85
basic simplification of external_prover signature;
wenzelm
parents:
35010
diff
changeset

108 
else if File.exists (Path.explode destdir') 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36265
diff
changeset

109 
then Path.append (Path.explode destdir') probfile 
36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36167
diff
changeset

110 
else error ("No such directory: " ^ destdir' ^ ".") 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

111 
end; 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

112 

31750  113 
(* write out problem file and call prover *) 
33247  114 
fun cmd_line probfile = 
36284
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

115 
(if Config.get ctxt measure_runtime then 
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

116 
"TIMEFORMAT='%3U'; { time " ^ space_implode " " [File.shell_path cmd, 
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

117 
args, File.shell_path probfile] ^ " ; } 2>&1" 
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

118 
else 
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

119 
space_implode " " ["exec", File.shell_path cmd, args, 
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

120 
File.shell_path probfile, "2>&1"]) ^ 
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

121 
(if overlord then 
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

122 
"  sed 's/,/, /g'  sed 's/\\([=]\\)/ \\1 /g'  sed 's/! =/ !=/g' \ 
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

123 
\ sed 's/ / /g'" 
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

124 
else 
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

125 
"") 
32510  126 
fun split_time s = 
127 
let 

32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

128 
val split = String.tokens (fn c => str c = "\n"); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

129 
val (proof, t) = s > split > split_last > apfst cat_lines; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

130 
fun as_num f = f >> (fst o read_int); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

131 
val num = as_num (Scan.many1 Symbol.is_ascii_digit); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

132 
val digit = Scan.one Symbol.is_ascii_digit; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

133 
val num3 = as_num (digit ::: digit ::: (digit >> single)); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

134 
val time = num  Scan.$$ "."  num3 >> (fn (a, b) => a * 1000 + b); 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

135 
val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

136 
in (proof, as_time t) end; 
33247  137 
fun split_time' s = 
138 
if Config.get ctxt measure_runtime then split_time s else (s, 0) 

32458
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

139 
fun run_on probfile = 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

140 
if File.exists cmd then 
36235
61159615a0c5
added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
blanchet
parents:
36231
diff
changeset

141 
write_file full_types explicit_apply probfile clauses 
35010
d6e492cea6e4
renamed system/system_out to bash/bash_output  to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
33316
diff
changeset

142 
> pair (apfst split_time' (bash_output (cmd_line probfile))) 
36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36143
diff
changeset

143 
else error ("Bad executable: " ^ Path.implode cmd ^ "."); 
28592  144 

36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36143
diff
changeset

145 
(* If the problem file has not been exported, remove it; otherwise, export 
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36143
diff
changeset

146 
the proof file too. *) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

147 
fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE; 
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

148 
fun export probfile (((proof, _), _), _) = 
36187  149 
if destdir' = "" then 
150 
() 

151 
else 

152 
File.write (Path.explode (Path.implode probfile ^ "_proof")) 

36282
9a7c5b86a105
generate commandline in addition to timestamp in ATP output file, for debugging purposes
blanchet
parents:
36281
diff
changeset

153 
((if overlord then 
9a7c5b86a105
generate commandline in addition to timestamp in ATP output file, for debugging purposes
blanchet
parents:
36281
diff
changeset

154 
"% " ^ cmd_line probfile ^ "\n% " ^ timestamp () ^ "\n" 
9a7c5b86a105
generate commandline in addition to timestamp in ATP output file, for debugging purposes
blanchet
parents:
36281
diff
changeset

155 
else 
9a7c5b86a105
generate commandline in addition to timestamp in ATP output file, for debugging purposes
blanchet
parents:
36281
diff
changeset

156 
"") ^ proof) 
32257
bad5a99c16d8
neg_conjecture_clauses, neg_clausify_tac: proper context, eliminated METAHYPS;
wenzelm
parents:
32091
diff
changeset

157 

36231
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36223
diff
changeset

158 
val (((proof, atp_run_time_in_msecs), rc), _) = 
35570
0e30eef52d85
basic simplification of external_prover signature;
wenzelm
parents:
35010
diff
changeset

159 
with_path cleanup export run_on (prob_pathname subgoal); 
32458
de6834b20e9e
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
boehmes
parents:
32451
diff
changeset

160 

36167
c1a35be8e476
make Sledgehammer's output more debugging friendly
blanchet
parents:
36143
diff
changeset

161 
(* Check for success and print out some information on failure. *) 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

162 
val failure = find_known_failure known_failures proof; 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

163 
val success = rc = 0 andalso failure = ""; 
35969  164 
val (message, relevant_thm_names) = 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

165 
if success then 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36265
diff
changeset

166 
proof_text ctxt minimize_command proof internal_thm_names th subgoal 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

167 
else if failure <> "" then 
36284
0e24322474a4
postprocess ATP output in "overlord" mode to make it more readable
blanchet
parents:
36283
diff
changeset

168 
(failure ^ "\n", []) 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

169 
else 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

170 
("Unknown ATP error: " ^ proof ^ ".\n", []) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

171 
in 
36231
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36223
diff
changeset

172 
{success = success, message = message, 
35969  173 
relevant_thm_names = relevant_thm_names, 
174 
atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof, 

175 
internal_thm_names = internal_thm_names, 

176 
filtered_clauses = the_filtered_clauses} 

32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

177 
end; 
28592  178 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

179 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

180 
(* generic TPTPbased provers *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

181 

35865  182 
fun generic_tptp_prover 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

183 
(name, {command, arguments, known_failures, max_new_clauses, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

184 
prefers_theory_relevant, supports_isar_proofs}) 
36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

185 
(params as {debug, overlord, respect_no_atp, relevance_threshold, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

186 
convergence, theory_relevant, higher_order, follow_defs, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

187 
isar_proof, modulus, sorts, ...}) 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36265
diff
changeset

188 
minimize_command timeout = 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

189 
generic_prover overlord 
36058
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

190 
(get_relevant_facts respect_no_atp relevance_threshold convergence 
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

191 
higher_order follow_defs max_new_clauses 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

192 
(the_default prefers_theory_relevant theory_relevant)) 
36222
0e3e49bd658d
don't use readable names if proof reconstruction is needed, because it uses the structure of names
blanchet
parents:
36220
diff
changeset

193 
(prepare_clauses higher_order false) 
36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

194 
(write_tptp_file (debug andalso overlord andalso not isar_proof)) command 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

195 
(arguments timeout) known_failures 
36283
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36282
diff
changeset

196 
(proof_text (supports_isar_proofs andalso isar_proof) debug modulus sorts) 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36265
diff
changeset

197 
name params minimize_command 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

198 

35969  199 
fun tptp_prover name p = (name, generic_tptp_prover (name, p)); 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

200 

32941
72d48e333b77
eliminated extraneous wrapping of public records;
wenzelm
parents:
32936
diff
changeset

201 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

202 
(** common provers **) 
28592  203 

36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

204 
fun generous_to_secs time = (Time.toMilliseconds time + 999) div 1000 
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

205 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

206 
(* Vampire *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

207 

35969  208 
(* NB: Vampire does not work without explicit time limit. *) 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

209 

35969  210 
val vampire_config : prover_config = 
211 
{command = Path.explode "$VAMPIRE_HOME/vampire", 

212 
arguments = (fn timeout => "output_syntax tptp mode casc t " ^ 

36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

213 
string_of_int (generous_to_secs timeout)), 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

214 
known_failures = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

215 
[(["Satisfiability detected", "CANNOT PROVE"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

216 
"The ATP problem is unprovable."), 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

217 
(["Refutation not found"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

218 
"The ATP failed to determine the problem's status.")], 
35969  219 
max_new_clauses = 60, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

220 
prefers_theory_relevant = false, 
35969  221 
supports_isar_proofs = true} 
222 
val vampire = tptp_prover "vampire" vampire_config 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

223 

28592  224 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

225 
(* E prover *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

226 

35969  227 
val e_config : prover_config = 
228 
{command = Path.explode "$E_HOME/eproof", 

229 
arguments = (fn timeout => "tstpin tstpout l5 xAutoDev \ 

230 
\tAutoDev silent cpulimit=" ^ 

36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

231 
string_of_int (generous_to_secs timeout)), 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

232 
known_failures = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

233 
[(["SZS status: Satisfiable", "SZS status Satisfiable"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

234 
"The ATP problem is unprovable."), 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

235 
(["SZS status: ResourceOut", "SZS status ResourceOut"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

236 
"The ATP ran out of resources."), 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

237 
(["# Cannot determine problem status"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

238 
"The ATP failed to determine the problem's status.")], 
35969  239 
max_new_clauses = 100, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

240 
prefers_theory_relevant = false, 
35969  241 
supports_isar_proofs = true} 
242 
val e = tptp_prover "e" e_config 

28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

243 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

244 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

245 
(* SPASS *) 
28592  246 

35865  247 
fun generic_dfg_prover 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

248 
(name, ({command, arguments, known_failures, max_new_clauses, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

249 
prefers_theory_relevant, ...} : prover_config)) 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

250 
(params as {overlord, respect_no_atp, relevance_threshold, convergence, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

251 
theory_relevant, higher_order, follow_defs, ...}) 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36265
diff
changeset

252 
minimize_command timeout = 
36143
6490319b1703
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
blanchet
parents:
36142
diff
changeset

253 
generic_prover overlord 
36058
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

254 
(get_relevant_facts respect_no_atp relevance_threshold convergence 
8256d5a185bd
added "respect_no_atp" and "convergence" options to Sledgehammer;
blanchet
parents:
36001
diff
changeset

255 
higher_order follow_defs max_new_clauses 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

256 
(the_default prefers_theory_relevant theory_relevant)) 
35969  257 
(prepare_clauses higher_order true) write_dfg_file command 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36265
diff
changeset

258 
(arguments timeout) known_failures (K metis_proof_text) 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36265
diff
changeset

259 
name params minimize_command 
32869
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

260 

36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

261 
fun dfg_prover name p = (name, generic_dfg_prover (name, p)) 
32869
159309603edc
recovered support for Spass: reenabled writing problems in DFG format
boehmes
parents:
32864
diff
changeset

262 

36219
16670b4f0baa
set SPASS option on the commandline, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset

263 
(* The "VarWeight=3" option helps the higherorder problems, probably by 
16670b4f0baa
set SPASS option on the commandline, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset

264 
counteracting the presence of "hAPP". *) 
36059  265 
val spass_config : prover_config = 
35969  266 
{command = Path.explode "$SPASS_HOME/SPASS", 
267 
arguments = (fn timeout => "Auto SOS=1 PGiven=0 PProblem=0 Splits=0" ^ 

36219
16670b4f0baa
set SPASS option on the commandline, so that it doesn't vanish when moving to TPTP format
blanchet
parents:
36190
diff
changeset

268 
" FullRed=0 DocProof VarWeight=3 TimeLimit=" ^ 
36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

269 
string_of_int (generous_to_secs timeout)), 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

270 
known_failures = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

271 
[(["SPASS beiseite: Completion found."], "The ATP problem is unprovable."), 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

272 
(["SPASS beiseite: Ran out of time."], "The ATP timed out."), 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

273 
(["SPASS beiseite: Maximal number of loops exceeded."], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

274 
"The ATP hit its loop limit.")], 
35969  275 
max_new_clauses = 40, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

276 
prefers_theory_relevant = true, 
36059  277 
supports_isar_proofs = false} 
36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

278 
val spass = dfg_prover "spass" spass_config 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

279 

3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

280 
(* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

281 
supports only the DFG syntax. As soon as all Isabelle repository/snapshot 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

282 
users have upgraded to 3.7, we can kill "spass" (and all DFG support in 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

283 
Sledgehammer) and rename "spass_tptp" "spass". *) 
35969  284 

36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

285 
(* FIXME: Change the error message below to point to the Isabelle download 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

286 
page once the package is there (around the Isabelle2010 release). *) 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

287 

36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

288 
val spass_tptp_config = 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

289 
{command = #command spass_config, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

290 
arguments = prefix "TPTP " o #arguments spass_config, 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

291 
known_failures = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

292 
#known_failures spass_config @ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

293 
[(["unrecognized option `TPTP'", "Unrecognized option TPTP"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

294 
"Warning: Sledgehammer requires a more recent version of SPASS with \ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

295 
\support for the TPTP syntax. To install it, download and untar the \ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

296 
\package \"http://isabelle.in.tum.de/~blanchet/spass3.7.tgz\" and add \ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

297 
\the \"spass3.7\" directory's full path to \"" ^ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

298 
Path.implode (Path.expand (Path.appends 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

299 
(Path.variable "ISABELLE_HOME_USER" :: 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

300 
map Path.basic ["etc", "components"]))) ^ 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

301 
"\" on a line of its own.")], 
36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

302 
max_new_clauses = #max_new_clauses spass_config, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

303 
prefers_theory_relevant = #prefers_theory_relevant spass_config, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

304 
supports_isar_proofs = #supports_isar_proofs spass_config} 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

305 
val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

306 

fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

307 
(* remote prover invocation via SystemOnTPTP *) 
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

308 

32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

309 
val systems = Synchronized.var "atp_wrapper_systems" ([]: string list); 
31835  310 

311 
fun get_systems () = 

312 
let 

35969  313 
val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" w" 
31835  314 
in 
35969  315 
if rc <> 0 then 
316 
error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer) 

317 
else 

318 
split_lines answer 

31835  319 
end; 
320 

35867  321 
fun refresh_systems_on_tptp () = 
322 
Synchronized.change systems (fn _ => get_systems ()); 

31835  323 

324 
fun get_system prefix = Synchronized.change_result systems (fn systems => 

32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

325 
(if null systems then get_systems () else systems) 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

326 
> `(find_first (String.isPrefix prefix))); 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

327 

32948  328 
fun the_system prefix = 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

329 
(case get_system prefix of 
35826  330 
NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP") 
32942
b6711ec9de26
misc tuning and recovery of Isabelle coding style;
wenzelm
parents:
32941
diff
changeset

331 
 SOME sys => sys); 
31835  332 

36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

333 
val remote_known_failures = 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

334 
[(["Remotescript could not extract proof"], 
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

335 
"Error: The remote ATP proof is illformed.")] 
35865  336 

36059  337 
fun remote_prover_config prover_prefix args 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

338 
({known_failures, max_new_clauses, prefers_theory_relevant, ...} 
36059  339 
: prover_config) : prover_config = 
35969  340 
{command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP", 
341 
arguments = (fn timeout => 

36142
f5e15e9aae10
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
blanchet
parents:
36064
diff
changeset

342 
args ^ " t " ^ string_of_int (generous_to_secs timeout) ^ " s " ^ 
35969  343 
the_system prover_prefix), 
36265
41c9e755e552
distinguish between the different ATP errors in the user interface;
blanchet
parents:
36264
diff
changeset

344 
known_failures = remote_known_failures @ known_failures, 
35969  345 
max_new_clauses = max_new_clauses, 
36220
f3655a3ae1ab
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
blanchet
parents:
36219
diff
changeset

346 
prefers_theory_relevant = prefers_theory_relevant, 
35969  347 
supports_isar_proofs = false} 
28596
fcd463a6b6de
tuned interfaces  plain prover function, without thread;
wenzelm
parents:
28592
diff
changeset

348 

35969  349 
val remote_vampire = 
350 
tptp_prover "remote_vampire" 

36059  351 
(remote_prover_config "Vampire9" "" vampire_config) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

352 

35969  353 
val remote_e = 
36059  354 
tptp_prover "remote_e" (remote_prover_config "EP" "" e_config) 
32864
a226f29d4bdc
reorganized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
boehmes
parents:
32740
diff
changeset

355 

35969  356 
val remote_spass = 
36059  357 
tptp_prover "remote_spass" (remote_prover_config "SPASS" "x" spass_config) 
28592  358 

36264
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

359 
val provers = [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, 
3c2490917710
added "spass_tptp" prover, which requires SPASS x.y > 3.0;
blanchet
parents:
36235
diff
changeset

360 
remote_e] 
35867  361 
val prover_setup = fold add_prover provers 
362 

363 
val setup = 

364 
destdir_setup 

365 
#> problem_prefix_setup 

366 
#> measure_runtime_setup 

367 
#> prover_setup; 

368 

28592  369 
end; 