author  blanchet 
Mon, 19 May 2014 23:43:53 +0200  
changeset 57005  33f3d2ea803d 
parent 53658  9e8714b4661a 
child 57172  bcc6dc6c1d1c 
permissions  rwrr 
41542  1 
""" 
2 
Test configuration descriptions for mira. 

3 
""" 

4 

5 
import os 

6 
from os import path 

7 
from glob import glob 

8 
import subprocess 

42392  9 
from datetime import datetime 
41542  10 
import re 
11 

12 
import util 

13 

42823  14 
from mira import schedule, misc 
42192  15 
from mira.environment import scheduler 
46931  16 
from mira import repositories 
42192  17 

41542  18 
# build and evaluation tools 
19 

50599  20 
DEFAULT_TIMEOUT = 2 * 60 * 60 
21 
SMLNJ_TIMEOUT = 72 * 60 * 60 

22 

50598  23 
def prepare_isabelle_repository(loc_isabelle, loc_dependency_heaps, more_settings=''): 
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset

24 

4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset

25 
# patch settings 
41542  26 
extra_settings = ''' 
27 
ISABELLE_HOME_USER="$ISABELLE_HOME/home_user" 

48785
1e384f729045
restored ISABELLE_OUTPUT etc  still relevant at least for mira.py itself
krauss
parents:
48783
diff
changeset

28 

42109  29 
Z3_NON_COMMERCIAL="yes" 
48785
1e384f729045
restored ISABELLE_OUTPUT etc  still relevant at least for mira.py itself
krauss
parents:
48783
diff
changeset

30 

50596  31 
init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/main" 
32 
init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional" 

33 
init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/nonfree" 

48182  34 

48783  35 
''' + more_settings 
41542  36 

37 
writer = open(path.join(loc_isabelle, 'etc', 'settings'), 'a') 

38 
writer.write(extra_settings) 

39 
writer.close() 

40 

41 

45164  42 
def isabelle_getenv(isabelle_home, var): 
43 

44 
_, out = env.run_process('%s/bin/isabelle' % isabelle_home, 'getenv', var) 

45 
return out.split('=', 1)[1].strip() 

46 

47 

41542  48 
def extract_isabelle_run_timing(logdata): 
49 

50 
def to_secs(h, m, s): 

51 
return (int(h) * 60 + int(m)) * 60 + int(s) 

52 
pat = r'Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time' 

42186
bb688200b949
adapted parsing of session timing (cf. e86b10c68f0b)
krauss
parents:
42140
diff
changeset

53 
pat2 = r'Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time, factor (\d+\.\d+)\)' 
41542  54 
t = dict((name, {'elapsed': to_secs(eh,em,es), 'cpu': to_secs(ch,cm,cs)}) 
55 
for name, eh, em, es, ch, cm, cs in re.findall(pat, logdata)) 

42186
bb688200b949
adapted parsing of session timing (cf. e86b10c68f0b)
krauss
parents:
42140
diff
changeset

56 
for name, threads, elapsed, cpu, gc, factor in re.findall(pat2, logdata): 
41542  57 

58 
if name not in t: 

59 
t[name] = {} 

60 

61 
t[name]['threads'] = int(threads) 

62 
t[name]['elapsed_inner'] = elapsed 

63 
t[name]['cpu_inner'] = cpu 

64 
t[name]['gc'] = gc 

42186
bb688200b949
adapted parsing of session timing (cf. e86b10c68f0b)
krauss
parents:
42140
diff
changeset

65 
t[name]['factor'] = factor 
41542  66 

67 
return t 

68 

69 

70 
def extract_isabelle_run_summary(logdata): 

71 

41894  72 
re_error = re.compile(r'^(?:make: )?\*\*\* (.*)$', re.MULTILINE) 
41542  73 
summary = '\n'.join(re_error.findall(logdata)) 
74 
if summary == '': 

75 
summary = 'ok' 

76 

77 
return summary 

78 

79 

45164  80 
def extract_image_size(isabelle_home): 
81 

82 
isabelle_output = isabelle_getenv(isabelle_home, 'ISABELLE_OUTPUT') 

50595  83 
if not path.exists(isabelle_output): 
84 
return {} 

85 

45164  86 
return dict((p, path.getsize(path.join(isabelle_output, p))) for p in os.listdir(isabelle_output) if p != "log") 
87 

88 
def extract_report_data(isabelle_home, logdata): 

89 

90 
return { 

91 
'timing': extract_isabelle_run_timing(logdata), 

92 
'image_size': extract_image_size(isabelle_home) } 

93 

94 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

95 
def isabelle_build(env, case, paths, dep_paths, playground, *cmdargs, **kwargs): 
41542  96 

50599  97 
more_settings = kwargs.get('more_settings', '') 
98 
keep_results = kwargs.get('keep_results', True) 

99 
timeout = kwargs.get('timeout', DEFAULT_TIMEOUT) 

41542  100 

42114  101 
isabelle_home = paths[0] 
41542  102 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

103 
# copy over build results from dependencies 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

104 
heap_dir = path.join(isabelle_home, 'heaps') 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

105 
classes_dir = path.join(heap_dir, 'classes') 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

106 
os.makedirs(classes_dir) 
42115
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset

107 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

108 
for dep_path in dep_paths: 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

109 
subprocess.check_call(['cp', 'a'] + glob(dep_path + '/*') + [heap_dir]) 
45164  110 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

111 
subprocess.check_call(['ln', 's', classes_dir, path.join(isabelle_home, 'lib', 'classes')]) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

112 
jars = glob(path.join(classes_dir, 'ext', '*.jar')) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

113 
if jars: 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

114 
subprocess.check_call(['touch'] + jars) 
42115
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset

115 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

116 
# misc preparations 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

117 
if 'lxbroy10' in misc.hostnames(): # special settings for lxbroy10 
42823  118 
more_settings += ''' 
43334
9970a4580d13
adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
bulwahn
parents:
43153
diff
changeset

119 
ISABELLE_GHC="/usr/bin/ghc" 
42823  120 
''' 
121 

50598  122 
prepare_isabelle_repository(isabelle_home, None, more_settings=more_settings) 
42114  123 
os.chdir(isabelle_home) 
41542  124 

50600
48c0c3bc40dd
tuned "use build timeout": tuples cannot be concatenated
noschinl
parents:
50599
diff
changeset

125 
args = (['o', 'timeout=%s' % timeout] if timeout is not None else []) + list(cmdargs) 
50599  126 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

127 
# invoke build tool 
50599  128 
(return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', 's', 'v', *args) 
41542  129 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

130 
# collect report 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

131 
return (return_code == 0, extract_isabelle_run_summary(log), 
49175
eab51f249c70
option for discarding build results, enabled in particular for Isabelle_makeall
krauss
parents:
48848
diff
changeset

132 
extract_report_data(isabelle_home, log), {'log': log}, heap_dir if keep_results else None) 
41542  133 

134 

43689  135 

136 
# Isabelle configurations 

137 

138 
@configuration(repos = [Isabelle], deps = []) 

139 
def Pure(*args): 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

140 
"""Pure Image""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

141 
return isabelle_build(*(args + ("b", "Pure"))) 
43689  142 

41542  143 
@configuration(repos = [Isabelle], deps = [(Pure, [0])]) 
144 
def HOL(*args): 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

145 
"""HOL Image""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

146 
return isabelle_build(*(args + ("b", "HOL"))) 
41542  147 

46934  148 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
149 
def HOL_Library(*args): 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

150 
"""HOL Library""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

151 
return isabelle_build(*(args + ("b", "HOLLibrary"))) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

152 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

153 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
48688  154 
def HOLCF(*args): 
48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

155 
"""HOLCF""" 
48688  156 
return isabelle_build(*(args + ("b", "HOLCF"))) 
46934  157 

158 
@configuration(repos = [Isabelle], deps = [(Pure, [0])]) 

159 
def ZF(*args): 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

160 
"""HOLCF""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

161 
return isabelle_build(*(args + ("b", "ZF"))) 
46934  162 

163 

47895  164 
settings64=''' 
50593  165 
# enforce 64 bit, overriding smart detection 
166 
ML_PLATFORM="$ISABELLE_PLATFORM64" 

167 
ML_HOME="$(dirname $ML_HOME)/$ML_PLATFORM" 

47895  168 
''' 
169 

47897  170 
@configuration(repos = [Isabelle], deps = []) 
41542  171 
def Isabelle_makeall(*args): 
48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

172 
"""Build all sessions""" 
49175
eab51f249c70
option for discarding build results, enabled in particular for Isabelle_makeall
krauss
parents:
48848
diff
changeset

173 
return isabelle_build(*(args + ("j", "6", "o", "threads=4", "a")), more_settings=settings64, keep_results=False) 
46934  174 

46931  175 

41542  176 
# Mutabelle configurations 
177 

178 
def invoke_mutabelle(theory, env, case, paths, dep_paths, playground): 

179 

180 
"""Mutant testing for counterexample generators in Isabelle""" 

181 

182 
(loc_isabelle,) = paths 

183 
(dep_isabelle,) = dep_paths 

43152
6c4e021dec06
adding more settings to mira's mutabelle configuration
bulwahn
parents:
42948
diff
changeset

184 
more_settings = ''' 
43153
cbb748ccf81b
changing the mira setting again for the mutabelle configuration
bulwahn
parents:
43152
diff
changeset

185 
ISABELLE_GHC="/usr/bin/ghc" 
43152
6c4e021dec06
adding more settings to mira's mutabelle configuration
bulwahn
parents:
42948
diff
changeset

186 
''' 
50598  187 
prepare_isabelle_repository(loc_isabelle, dep_isabelle, more_settings = more_settings) 
41542  188 
os.chdir(loc_isabelle) 
189 

190 
(return_code, log) = env.run_process('bin/isabelle', 

191 
'mutabelle', 'O', playground, theory) 

192 

193 
try: 

194 
mutabelle_log = util.readfile(path.join(playground, 'log')) 

195 
except IOError: 

196 
mutabelle_log = '' 

197 

42472  198 
mutabelle_data = dict( 
199 
(tool, {'counterexample': c, 'no_counterexample': n, 'timeout': t, 'error': e}) 

200 
for tool, c, n, t, e in re.findall(r'(\S+)\s+: C: (\d+) N: (\d+) T: (\d+) E: (\d+)', log)) 

201 

41542  202 
return (return_code == 0 and mutabelle_log != '', extract_isabelle_run_summary(log), 
42472  203 
{'mutabelle_results': {theory: mutabelle_data}}, 
41652  204 
{'log': log, 'mutabelle_log': mutabelle_log}, None) 
41542  205 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

206 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  207 
def Mutabelle_Relation(*args): 
208 
"""Mutabelle regression suite on Relation theory""" 

209 
return invoke_mutabelle('Relation', *args) 

210 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

211 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  212 
def Mutabelle_List(*args): 
213 
"""Mutabelle regression suite on List theory""" 

214 
return invoke_mutabelle('List', *args) 

215 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

216 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  217 
def Mutabelle_Set(*args): 
218 
"""Mutabelle regression suite on Set theory""" 

219 
return invoke_mutabelle('Set', *args) 

220 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

221 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  222 
def Mutabelle_Map(*args): 
223 
"""Mutabelle regression suite on Map theory""" 

224 
return invoke_mutabelle('Map', *args) 

225 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

226 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  227 
def Mutabelle_Divides(*args): 
228 
"""Mutabelle regression suite on Divides theory""" 

229 
return invoke_mutabelle('Divides', *args) 

230 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

231 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  232 
def Mutabelle_MacLaurin(*args): 
233 
"""Mutabelle regression suite on MacLaurin theory""" 

234 
return invoke_mutabelle('MacLaurin', *args) 

235 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

236 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  237 
def Mutabelle_Fun(*args): 
238 
"""Mutabelle regression suite on Fun theory""" 

239 
return invoke_mutabelle('Fun', *args) 

42040  240 

42393  241 
mutabelle_confs = 'Mutabelle_Relation Mutabelle_List Mutabelle_Set Mutabelle_Map Mutabelle_Divides Mutabelle_MacLaurin Mutabelle_Fun'.split(' ') 
242 

243 
@scheduler() 

244 
def mutabelle_scheduler(env): 

245 
"""Scheduler for Mutabelle.""" 

246 
return schedule.age_scheduler(env, 'Isabelle', mutabelle_confs) 

42040  247 

47896  248 

42040  249 
# Judgement Day configurations 
250 

42095  251 
judgement_day_provers = ('e', 'spass', 'vampire', 'z3', 'cvc3', 'yices') 
42040  252 

253 
def judgement_day(base_path, theory, opts, env, case, paths, dep_paths, playground): 

254 
"""Judgement Day regression suite""" 

255 

256 
isa = paths[0] 

257 
dep_path = dep_paths[0] 

258 

259 
os.chdir(path.join(playground, '..', base_path)) # Mirabelle requires specific cwd 

50594
3f794789df0e
removed obsolete parameter for contrib dir; hardcoding is not a problem
krauss
parents:
50593
diff
changeset

260 
prepare_isabelle_repository(isa, dep_path) 
42040  261 

262 
output = {} 

263 
success_rates = {} 

264 
some_success = False 

265 

266 
for atp in judgement_day_provers: 

267 

268 
log_dir = path.join(playground, 'mirabelle_log_' + atp) 

269 
os.makedirs(log_dir) 

270 

271 
cmd = ('%s/bin/isabelle mirabelle q O %s sledgehammer[prover=%s,%s] %s.thy' 

272 
% (isa, log_dir, atp, opts, theory)) 

273 

274 
os.system(cmd) 

275 
output[atp] = util.readfile(path.join(log_dir, theory + '.log')) 

276 

277 
percentages = list(re.findall(r'Success rate: (\d+)%', output[atp])) 

278 
if len(percentages) == 2: 

279 
success_rates[atp] = { 

280 
'sledgehammer': int(percentages[0]), 

281 
'metis': int(percentages[1])} 

282 
if success_rates[atp]['sledgehammer'] > 0: 

283 
some_success = True 

284 
else: 

285 
success_rates[atp] = {} 

286 

287 

288 
data = {'success_rates': success_rates} 

289 
raw_attachments = dict((atp + "_output", output[atp]) for atp in judgement_day_provers) 

290 
# FIXME: summary? 

291 
return (some_success, '', data, raw_attachments, None) 

292 

293 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

294 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
42040  295 
def JD_NS(*args): 
296 
"""Judgement Day regression suite NS""" 

297 
return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args) 

298 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

299 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
42040  300 
def JD_FTA(*args): 
301 
"""Judgement Day regression suite FTA""" 

302 
return judgement_day('Isabelle/src/HOL/Library', 'Fundamental_Theorem_Algebra', 'prover_timeout=10', *args) 

303 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

304 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
42040  305 
def JD_Hoare(*args): 
306 
"""Judgement Day regression suite Hoare""" 

42058
1eda69f0b9a8
moved some configurations to AFP, and fixed others
krauss
parents:
42040
diff
changeset

307 
return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args) 
42040  308 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

309 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
42040  310 
def JD_SN(*args): 
311 
"""Judgement Day regression suite SN""" 

42058
1eda69f0b9a8
moved some configurations to AFP, and fixed others
krauss
parents:
42040
diff
changeset

312 
return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args) 
42040  313 

42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

314 

42192  315 
JD_confs = 'JD_NS JD_FTA JD_Hoare JD_SN JD_Arrow JD_FFT JD_Jinja JD_QE JD_S2S'.split(' ') 
316 

317 
@scheduler() 

42197  318 
def judgement_day_scheduler(env): 
42192  319 
"""Scheduler for Judgement Day.""" 
320 
return schedule.age_scheduler(env, 'Isabelle', JD_confs) 

321 

322 

42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

323 
# SML/NJ 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

324 

b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

325 
smlnj_settings = ''' 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

326 
ML_SYSTEM=smlnj 
53658  327 
ML_HOME="/home/smlnj/110.76/bin" 
48443  328 
ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024" 
42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

329 
ML_PLATFORM=$(eval $("$ML_HOME/.archnopsys" 2>/dev/null); echo "$HEAP_SUFFIX") 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

330 
''' 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

331 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

332 
@configuration(repos = [Isabelle], deps = [(Pure, [0])]) 
42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

333 
def SML_HOL(*args): 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

334 
"""HOL image built with SML/NJ""" 
50599  335 
return isabelle_build(*(args + ("b", "HOL")), more_settings=smlnj_settings, timeout=SMLNJ_TIMEOUT) 
42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

336 

b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

337 
@configuration(repos = [Isabelle], deps = []) 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

338 
def SML_makeall(*args): 
48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

339 
"""SML/NJ build of all possible sessions""" 
50599  340 
return isabelle_build(*(args + ("j", "3", "a")), more_settings=smlnj_settings, timeout=SMLNJ_TIMEOUT) 
48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

341 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

342 