haftmann@41790
|
1 |
"""
|
haftmann@41790
|
2 |
Test configuration descriptions for mira.
|
haftmann@41790
|
3 |
"""
|
haftmann@41790
|
4 |
|
haftmann@41790
|
5 |
import os
|
haftmann@41790
|
6 |
from os import path
|
haftmann@41790
|
7 |
from glob import glob
|
haftmann@41790
|
8 |
import subprocess
|
krauss@43255
|
9 |
from datetime import datetime
|
haftmann@41790
|
10 |
import re
|
haftmann@41790
|
11 |
|
haftmann@41790
|
12 |
import util
|
haftmann@41790
|
13 |
|
krauss@43694
|
14 |
from mira import schedule, misc
|
krauss@43063
|
15 |
from mira.environment import scheduler
|
haftmann@47791
|
16 |
from mira import repositories
|
krauss@43063
|
17 |
|
haftmann@41790
|
18 |
# build and evaluation tools
|
haftmann@41790
|
19 |
|
krauss@51614
|
20 |
DEFAULT_TIMEOUT = 2 * 60 * 60
|
krauss@51614
|
21 |
SMLNJ_TIMEOUT = 72 * 60 * 60
|
krauss@51614
|
22 |
|
krauss@51613
|
23 |
def prepare_isabelle_repository(loc_isabelle, loc_dependency_heaps, more_settings=''):
|
krauss@43692
|
24 |
|
krauss@43692
|
25 |
# patch settings
|
haftmann@41790
|
26 |
extra_settings = '''
|
haftmann@41790
|
27 |
ISABELLE_HOME_USER="$ISABELLE_HOME/home_user"
|
krauss@49800
|
28 |
|
krauss@42973
|
29 |
Z3_NON_COMMERCIAL="yes"
|
krauss@49800
|
30 |
|
krauss@51611
|
31 |
init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/main"
|
krauss@51611
|
32 |
init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/optional"
|
krauss@51611
|
33 |
init_components "/home/isabelle/contrib" "$ISABELLE_HOME/Admin/components/nonfree"
|
haftmann@49197
|
34 |
|
krauss@49798
|
35 |
''' + more_settings
|
haftmann@41790
|
36 |
|
haftmann@41790
|
37 |
writer = open(path.join(loc_isabelle, 'etc', 'settings'), 'a')
|
haftmann@41790
|
38 |
writer.write(extra_settings)
|
haftmann@41790
|
39 |
writer.close()
|
haftmann@41790
|
40 |
|
haftmann@41790
|
41 |
|
krauss@46035
|
42 |
def isabelle_getenv(isabelle_home, var):
|
krauss@46035
|
43 |
|
krauss@46035
|
44 |
_, out = env.run_process('%s/bin/isabelle' % isabelle_home, 'getenv', var)
|
krauss@46035
|
45 |
return out.split('=', 1)[1].strip()
|
krauss@46035
|
46 |
|
krauss@46035
|
47 |
|
haftmann@41790
|
48 |
def extract_isabelle_run_timing(logdata):
|
haftmann@41790
|
49 |
|
haftmann@41790
|
50 |
def to_secs(h, m, s):
|
haftmann@41790
|
51 |
return (int(h) * 60 + int(m)) * 60 + int(s)
|
haftmann@41790
|
52 |
pat = r'Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time'
|
krauss@43057
|
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+)\)'
|
haftmann@41790
|
54 |
t = dict((name, {'elapsed': to_secs(eh,em,es), 'cpu': to_secs(ch,cm,cs)})
|
haftmann@41790
|
55 |
for name, eh, em, es, ch, cm, cs in re.findall(pat, logdata))
|
krauss@43057
|
56 |
for name, threads, elapsed, cpu, gc, factor in re.findall(pat2, logdata):
|
haftmann@41790
|
57 |
|
haftmann@41790
|
58 |
if name not in t:
|
haftmann@41790
|
59 |
t[name] = {}
|
haftmann@41790
|
60 |
|
haftmann@41790
|
61 |
t[name]['threads'] = int(threads)
|
haftmann@41790
|
62 |
t[name]['elapsed_inner'] = elapsed
|
haftmann@41790
|
63 |
t[name]['cpu_inner'] = cpu
|
haftmann@41790
|
64 |
t[name]['gc'] = gc
|
krauss@43057
|
65 |
t[name]['factor'] = factor
|
haftmann@41790
|
66 |
|
haftmann@41790
|
67 |
return t
|
haftmann@41790
|
68 |
|
haftmann@41790
|
69 |
|
haftmann@41790
|
70 |
def extract_isabelle_run_summary(logdata):
|
haftmann@41790
|
71 |
|
krauss@42765
|
72 |
re_error = re.compile(r'^(?:make: )?\*\*\* (.*)$', re.MULTILINE)
|
haftmann@41790
|
73 |
summary = '\n'.join(re_error.findall(logdata))
|
haftmann@41790
|
74 |
if summary == '':
|
haftmann@41790
|
75 |
summary = 'ok'
|
haftmann@41790
|
76 |
|
haftmann@41790
|
77 |
return summary
|
haftmann@41790
|
78 |
|
haftmann@41790
|
79 |
|
krauss@46035
|
80 |
def extract_image_size(isabelle_home):
|
krauss@46035
|
81 |
|
krauss@46035
|
82 |
isabelle_output = isabelle_getenv(isabelle_home, 'ISABELLE_OUTPUT')
|
krauss@51610
|
83 |
if not path.exists(isabelle_output):
|
krauss@51610
|
84 |
return {}
|
krauss@51610
|
85 |
|
krauss@46035
|
86 |
return dict((p, path.getsize(path.join(isabelle_output, p))) for p in os.listdir(isabelle_output) if p != "log")
|
krauss@46035
|
87 |
|
krauss@46035
|
88 |
def extract_report_data(isabelle_home, logdata):
|
krauss@46035
|
89 |
|
krauss@46035
|
90 |
return {
|
krauss@46035
|
91 |
'timing': extract_isabelle_run_timing(logdata),
|
krauss@46035
|
92 |
'image_size': extract_image_size(isabelle_home) }
|
krauss@46035
|
93 |
|
krauss@46035
|
94 |
|
krauss@49701
|
95 |
def isabelle_build(env, case, paths, dep_paths, playground, *cmdargs, **kwargs):
|
krauss@43255
|
96 |
|
krauss@51614
|
97 |
more_settings = kwargs.get('more_settings', '')
|
krauss@51614
|
98 |
keep_results = kwargs.get('keep_results', True)
|
krauss@51614
|
99 |
timeout = kwargs.get('timeout', DEFAULT_TIMEOUT)
|
haftmann@41790
|
100 |
|
krauss@42978
|
101 |
isabelle_home = paths[0]
|
krauss@49701
|
102 |
|
krauss@49701
|
103 |
# copy over build results from dependencies
|
krauss@49701
|
104 |
heap_dir = path.join(isabelle_home, 'heaps')
|
krauss@49701
|
105 |
classes_dir = path.join(heap_dir, 'classes')
|
krauss@49701
|
106 |
os.makedirs(classes_dir)
|
krauss@49701
|
107 |
|
haftmann@41790
|
108 |
for dep_path in dep_paths:
|
krauss@49701
|
109 |
subprocess.check_call(['cp', '-a'] + glob(dep_path + '/*') + [heap_dir])
|
haftmann@41790
|
110 |
|
krauss@49701
|
111 |
subprocess.check_call(['ln', '-s', classes_dir, path.join(isabelle_home, 'lib', 'classes')])
|
krauss@49701
|
112 |
jars = glob(path.join(classes_dir, 'ext', '*.jar'))
|
krauss@49701
|
113 |
if jars:
|
krauss@49701
|
114 |
subprocess.check_call(['touch'] + jars)
|
haftmann@41790
|
115 |
|
krauss@49701
|
116 |
# misc preparations
|
krauss@49701
|
117 |
if 'lxbroy10' in misc.hostnames(): # special settings for lxbroy10
|
krauss@43694
|
118 |
more_settings += '''
|
bulwahn@44191
|
119 |
ISABELLE_GHC="/usr/bin/ghc"
|
krauss@43694
|
120 |
'''
|
krauss@43694
|
121 |
|
krauss@51613
|
122 |
prepare_isabelle_repository(isabelle_home, None, more_settings=more_settings)
|
krauss@42978
|
123 |
os.chdir(isabelle_home)
|
haftmann@41790
|
124 |
|
noschinl@51615
|
125 |
args = (['-o', 'timeout=%s' % timeout] if timeout is not None else []) + list(cmdargs)
|
krauss@51614
|
126 |
|
krauss@49701
|
127 |
# invoke build tool
|
krauss@51614
|
128 |
(return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', '-s', '-v', *args)
|
haftmann@41790
|
129 |
|
krauss@49701
|
130 |
# collect report
|
haftmann@41790
|
131 |
return (return_code == 0, extract_isabelle_run_summary(log),
|
krauss@50190
|
132 |
extract_report_data(isabelle_home, log), {'log': log}, heap_dir if keep_results else None)
|
haftmann@41790
|
133 |
|
haftmann@41790
|
134 |
|
krauss@44555
|
135 |
|
krauss@44555
|
136 |
# Isabelle configurations
|
krauss@44555
|
137 |
|
krauss@44555
|
138 |
@configuration(repos = [Isabelle], deps = [])
|
krauss@44555
|
139 |
def Pure(*args):
|
krauss@49701
|
140 |
"""Pure Image"""
|
krauss@49701
|
141 |
return isabelle_build(*(args + ("-b", "Pure")))
|
krauss@44555
|
142 |
|
haftmann@41790
|
143 |
@configuration(repos = [Isabelle], deps = [(Pure, [0])])
|
haftmann@41790
|
144 |
def HOL(*args):
|
krauss@49701
|
145 |
"""HOL Image"""
|
krauss@49701
|
146 |
return isabelle_build(*(args + ("-b", "HOL")))
|
haftmann@41790
|
147 |
|
haftmann@47794
|
148 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@47794
|
149 |
def HOL_Library(*args):
|
krauss@49701
|
150 |
"""HOL Library"""
|
krauss@49701
|
151 |
return isabelle_build(*(args + ("-b", "HOL-Library")))
|
krauss@49701
|
152 |
|
krauss@49701
|
153 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
krauss@49703
|
154 |
def HOLCF(*args):
|
krauss@49701
|
155 |
"""HOLCF"""
|
krauss@49703
|
156 |
return isabelle_build(*(args + ("-b", "HOLCF")))
|
haftmann@47794
|
157 |
|
haftmann@47794
|
158 |
@configuration(repos = [Isabelle], deps = [(Pure, [0])])
|
haftmann@47794
|
159 |
def ZF(*args):
|
krauss@49701
|
160 |
"""HOLCF"""
|
krauss@49701
|
161 |
return isabelle_build(*(args + ("-b", "ZF")))
|
haftmann@47794
|
162 |
|
haftmann@47794
|
163 |
|
bulwahn@48910
|
164 |
settings64='''
|
krauss@51608
|
165 |
# enforce 64 bit, overriding smart detection
|
krauss@51608
|
166 |
ML_PLATFORM="$ISABELLE_PLATFORM64"
|
krauss@51608
|
167 |
ML_HOME="$(dirname $ML_HOME)/$ML_PLATFORM"
|
bulwahn@48910
|
168 |
'''
|
bulwahn@48910
|
169 |
|
bulwahn@48912
|
170 |
@configuration(repos = [Isabelle], deps = [])
|
haftmann@41790
|
171 |
def Isabelle_makeall(*args):
|
krauss@49701
|
172 |
"""Build all sessions"""
|
krauss@50190
|
173 |
return isabelle_build(*(args + ("-j", "6", "-o", "threads=4", "-a")), more_settings=settings64, keep_results=False)
|
haftmann@47794
|
174 |
|
haftmann@47791
|
175 |
|
haftmann@41790
|
176 |
# Mutabelle configurations
|
haftmann@41790
|
177 |
|
haftmann@41790
|
178 |
def invoke_mutabelle(theory, env, case, paths, dep_paths, playground):
|
haftmann@41790
|
179 |
|
haftmann@41790
|
180 |
"""Mutant testing for counterexample generators in Isabelle"""
|
haftmann@41790
|
181 |
|
haftmann@41790
|
182 |
(loc_isabelle,) = paths
|
haftmann@41790
|
183 |
(dep_isabelle,) = dep_paths
|
bulwahn@43993
|
184 |
more_settings = '''
|
bulwahn@43994
|
185 |
ISABELLE_GHC="/usr/bin/ghc"
|
bulwahn@43993
|
186 |
'''
|
krauss@51613
|
187 |
prepare_isabelle_repository(loc_isabelle, dep_isabelle, more_settings = more_settings)
|
haftmann@41790
|
188 |
os.chdir(loc_isabelle)
|
haftmann@41790
|
189 |
|
haftmann@41790
|
190 |
(return_code, log) = env.run_process('bin/isabelle',
|
haftmann@41790
|
191 |
'mutabelle', '-O', playground, theory)
|
haftmann@41790
|
192 |
|
haftmann@41790
|
193 |
try:
|
haftmann@41790
|
194 |
mutabelle_log = util.readfile(path.join(playground, 'log'))
|
haftmann@41790
|
195 |
except IOError:
|
haftmann@41790
|
196 |
mutabelle_log = ''
|
haftmann@41790
|
197 |
|
krauss@43343
|
198 |
mutabelle_data = dict(
|
krauss@43343
|
199 |
(tool, {'counterexample': c, 'no_counterexample': n, 'timeout': t, 'error': e})
|
krauss@43343
|
200 |
for tool, c, n, t, e in re.findall(r'(\S+)\s+: C: (\d+) N: (\d+) T: (\d+) E: (\d+)', log))
|
krauss@43343
|
201 |
|
haftmann@41790
|
202 |
return (return_code == 0 and mutabelle_log != '', extract_isabelle_run_summary(log),
|
krauss@43343
|
203 |
{'mutabelle_results': {theory: mutabelle_data}},
|
haftmann@42521
|
204 |
{'log': log, 'mutabelle_log': mutabelle_log}, None)
|
haftmann@41790
|
205 |
|
krauss@43789
|
206 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
207 |
def Mutabelle_Relation(*args):
|
haftmann@41790
|
208 |
"""Mutabelle regression suite on Relation theory"""
|
haftmann@41790
|
209 |
return invoke_mutabelle('Relation', *args)
|
haftmann@41790
|
210 |
|
krauss@43789
|
211 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
212 |
def Mutabelle_List(*args):
|
haftmann@41790
|
213 |
"""Mutabelle regression suite on List theory"""
|
haftmann@41790
|
214 |
return invoke_mutabelle('List', *args)
|
haftmann@41790
|
215 |
|
krauss@43789
|
216 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
217 |
def Mutabelle_Set(*args):
|
haftmann@41790
|
218 |
"""Mutabelle regression suite on Set theory"""
|
haftmann@41790
|
219 |
return invoke_mutabelle('Set', *args)
|
haftmann@41790
|
220 |
|
krauss@43789
|
221 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
222 |
def Mutabelle_Map(*args):
|
haftmann@41790
|
223 |
"""Mutabelle regression suite on Map theory"""
|
haftmann@41790
|
224 |
return invoke_mutabelle('Map', *args)
|
haftmann@41790
|
225 |
|
krauss@43789
|
226 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
227 |
def Mutabelle_Divides(*args):
|
haftmann@41790
|
228 |
"""Mutabelle regression suite on Divides theory"""
|
haftmann@41790
|
229 |
return invoke_mutabelle('Divides', *args)
|
haftmann@41790
|
230 |
|
krauss@43789
|
231 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
232 |
def Mutabelle_MacLaurin(*args):
|
haftmann@41790
|
233 |
"""Mutabelle regression suite on MacLaurin theory"""
|
haftmann@41790
|
234 |
return invoke_mutabelle('MacLaurin', *args)
|
haftmann@41790
|
235 |
|
krauss@43789
|
236 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
237 |
def Mutabelle_Fun(*args):
|
haftmann@41790
|
238 |
"""Mutabelle regression suite on Fun theory"""
|
haftmann@41790
|
239 |
return invoke_mutabelle('Fun', *args)
|
krauss@42910
|
240 |
|
krauss@43256
|
241 |
mutabelle_confs = 'Mutabelle_Relation Mutabelle_List Mutabelle_Set Mutabelle_Map Mutabelle_Divides Mutabelle_MacLaurin Mutabelle_Fun'.split(' ')
|
krauss@43256
|
242 |
|
krauss@43256
|
243 |
@scheduler()
|
krauss@43256
|
244 |
def mutabelle_scheduler(env):
|
krauss@43256
|
245 |
"""Scheduler for Mutabelle."""
|
krauss@43256
|
246 |
return schedule.age_scheduler(env, 'Isabelle', mutabelle_confs)
|
krauss@42910
|
247 |
|
bulwahn@48911
|
248 |
|
krauss@42910
|
249 |
# Judgement Day configurations
|
krauss@42910
|
250 |
|
krauss@42959
|
251 |
judgement_day_provers = ('e', 'spass', 'vampire', 'z3', 'cvc3', 'yices')
|
krauss@42910
|
252 |
|
krauss@42910
|
253 |
def judgement_day(base_path, theory, opts, env, case, paths, dep_paths, playground):
|
krauss@42910
|
254 |
"""Judgement Day regression suite"""
|
krauss@42910
|
255 |
|
krauss@42910
|
256 |
isa = paths[0]
|
krauss@42910
|
257 |
dep_path = dep_paths[0]
|
krauss@42910
|
258 |
|
krauss@42910
|
259 |
os.chdir(path.join(playground, '..', base_path)) # Mirabelle requires specific cwd
|
krauss@51609
|
260 |
prepare_isabelle_repository(isa, dep_path)
|
krauss@42910
|
261 |
|
krauss@42910
|
262 |
output = {}
|
krauss@42910
|
263 |
success_rates = {}
|
krauss@42910
|
264 |
some_success = False
|
krauss@42910
|
265 |
|
krauss@42910
|
266 |
for atp in judgement_day_provers:
|
krauss@42910
|
267 |
|
krauss@42910
|
268 |
log_dir = path.join(playground, 'mirabelle_log_' + atp)
|
krauss@42910
|
269 |
os.makedirs(log_dir)
|
krauss@42910
|
270 |
|
krauss@42910
|
271 |
cmd = ('%s/bin/isabelle mirabelle -q -O %s sledgehammer[prover=%s,%s] %s.thy'
|
krauss@42910
|
272 |
% (isa, log_dir, atp, opts, theory))
|
krauss@42910
|
273 |
|
krauss@42910
|
274 |
os.system(cmd)
|
krauss@42910
|
275 |
output[atp] = util.readfile(path.join(log_dir, theory + '.log'))
|
krauss@42910
|
276 |
|
krauss@42910
|
277 |
percentages = list(re.findall(r'Success rate: (\d+)%', output[atp]))
|
krauss@42910
|
278 |
if len(percentages) == 2:
|
krauss@42910
|
279 |
success_rates[atp] = {
|
krauss@42910
|
280 |
'sledgehammer': int(percentages[0]),
|
krauss@42910
|
281 |
'metis': int(percentages[1])}
|
krauss@42910
|
282 |
if success_rates[atp]['sledgehammer'] > 0:
|
krauss@42910
|
283 |
some_success = True
|
krauss@42910
|
284 |
else:
|
krauss@42910
|
285 |
success_rates[atp] = {}
|
krauss@42910
|
286 |
|
krauss@42910
|
287 |
|
krauss@42910
|
288 |
data = {'success_rates': success_rates}
|
krauss@42910
|
289 |
raw_attachments = dict((atp + "_output", output[atp]) for atp in judgement_day_provers)
|
krauss@42910
|
290 |
# FIXME: summary?
|
krauss@42910
|
291 |
return (some_success, '', data, raw_attachments, None)
|
krauss@42910
|
292 |
|
krauss@42910
|
293 |
|
krauss@43789
|
294 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
krauss@42910
|
295 |
def JD_NS(*args):
|
krauss@42910
|
296 |
"""Judgement Day regression suite NS"""
|
krauss@42910
|
297 |
return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
|
krauss@42910
|
298 |
|
krauss@43789
|
299 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
krauss@42910
|
300 |
def JD_FTA(*args):
|
krauss@42910
|
301 |
"""Judgement Day regression suite FTA"""
|
krauss@42910
|
302 |
return judgement_day('Isabelle/src/HOL/Library', 'Fundamental_Theorem_Algebra', 'prover_timeout=10', *args)
|
krauss@42910
|
303 |
|
krauss@43789
|
304 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
krauss@42910
|
305 |
def JD_Hoare(*args):
|
krauss@42910
|
306 |
"""Judgement Day regression suite Hoare"""
|
krauss@42913
|
307 |
return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args)
|
krauss@42910
|
308 |
|
krauss@43789
|
309 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
krauss@42910
|
310 |
def JD_SN(*args):
|
krauss@42910
|
311 |
"""Judgement Day regression suite SN"""
|
krauss@42913
|
312 |
return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
|
krauss@42910
|
313 |
|
krauss@42980
|
314 |
|
krauss@43063
|
315 |
JD_confs = 'JD_NS JD_FTA JD_Hoare JD_SN JD_Arrow JD_FFT JD_Jinja JD_QE JD_S2S'.split(' ')
|
krauss@43063
|
316 |
|
krauss@43063
|
317 |
@scheduler()
|
krauss@43068
|
318 |
def judgement_day_scheduler(env):
|
krauss@43063
|
319 |
"""Scheduler for Judgement Day."""
|
krauss@43063
|
320 |
return schedule.age_scheduler(env, 'Isabelle', JD_confs)
|
krauss@43063
|
321 |
|
krauss@43063
|
322 |
|
krauss@42980
|
323 |
# SML/NJ
|
krauss@42980
|
324 |
|
krauss@42980
|
325 |
smlnj_settings = '''
|
krauss@42980
|
326 |
ML_SYSTEM=smlnj
|
wenzelm@54795
|
327 |
ML_HOME="/home/smlnj/110.76/bin"
|
wenzelm@49458
|
328 |
ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
|
krauss@42980
|
329 |
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
|
krauss@42980
|
330 |
'''
|
krauss@42980
|
331 |
|
krauss@49701
|
332 |
@configuration(repos = [Isabelle], deps = [(Pure, [0])])
|
krauss@42980
|
333 |
def SML_HOL(*args):
|
krauss@42980
|
334 |
"""HOL image built with SML/NJ"""
|
krauss@51614
|
335 |
return isabelle_build(*(args + ("-b", "HOL")), more_settings=smlnj_settings, timeout=SMLNJ_TIMEOUT)
|
krauss@42980
|
336 |
|
krauss@42980
|
337 |
@configuration(repos = [Isabelle], deps = [])
|
krauss@42980
|
338 |
def SML_makeall(*args):
|
krauss@49701
|
339 |
"""SML/NJ build of all possible sessions"""
|
krauss@51614
|
340 |
return isabelle_build(*(args + ("-j", "3", "-a")), more_settings=smlnj_settings, timeout=SMLNJ_TIMEOUT)
|
krauss@44765
|
341 |
|
krauss@49701
|
342 |
|