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