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
|
haftmann@41790
|
9 |
import re
|
haftmann@41790
|
10 |
|
haftmann@41790
|
11 |
import util
|
haftmann@41790
|
12 |
|
haftmann@41790
|
13 |
|
haftmann@41790
|
14 |
# build and evaluation tools
|
haftmann@41790
|
15 |
|
krauss@42977
|
16 |
def prepare_isabelle_repository(loc_isabelle, loc_contrib, loc_dependency_heaps, parallelism = True, more_settings=''):
|
haftmann@41790
|
17 |
|
haftmann@41790
|
18 |
loc_contrib = path.expanduser(loc_contrib)
|
haftmann@41790
|
19 |
if not path.exists(loc_contrib):
|
haftmann@41790
|
20 |
raise IOError('Bad file: %s' % loc_contrib)
|
haftmann@41790
|
21 |
subprocess.check_call(['ln', '-s', loc_contrib, '%s/contrib' % loc_isabelle])
|
haftmann@41790
|
22 |
|
haftmann@41790
|
23 |
contributed_components = path.join(loc_isabelle, 'Admin', 'contributed_components')
|
haftmann@41790
|
24 |
if path.exists(contributed_components):
|
haftmann@41790
|
25 |
components = []
|
haftmann@41790
|
26 |
for component in util.readfile_lines(contributed_components):
|
haftmann@41790
|
27 |
loc_component = path.join(loc_isabelle, component)
|
haftmann@41790
|
28 |
if path.exists(loc_component):
|
haftmann@41790
|
29 |
components.append(loc_component)
|
haftmann@41790
|
30 |
writer = open(path.join(loc_isabelle, 'etc', 'components'), 'a')
|
haftmann@41790
|
31 |
for component in components:
|
haftmann@41790
|
32 |
writer.write(component + '\n')
|
haftmann@41790
|
33 |
writer.close()
|
haftmann@41790
|
34 |
|
haftmann@41790
|
35 |
if loc_dependency_heaps:
|
haftmann@41790
|
36 |
isabelle_path = loc_dependency_heaps + '/$ISABELLE_IDENTIFIER:$ISABELLE_OUTPUT'
|
haftmann@41790
|
37 |
else:
|
haftmann@41790
|
38 |
isabelle_path = '$ISABELLE_OUTPUT'
|
haftmann@41790
|
39 |
|
haftmann@41790
|
40 |
if parallelism:
|
haftmann@41790
|
41 |
parallelism_options = '-M max'
|
haftmann@41790
|
42 |
else:
|
haftmann@41790
|
43 |
parallelism_options = '-M 1 -q 0'
|
haftmann@41790
|
44 |
|
haftmann@41790
|
45 |
extra_settings = '''
|
haftmann@41790
|
46 |
ISABELLE_HOME_USER="$ISABELLE_HOME/home_user"
|
haftmann@41790
|
47 |
ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
|
haftmann@41790
|
48 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
|
haftmann@41790
|
49 |
ISABELLE_PATH="%s"
|
haftmann@41790
|
50 |
|
haftmann@41790
|
51 |
ISABELLE_USEDIR_OPTIONS="$ISABELLE_USEDIR_OPTIONS %s -t true -v true -d pdf -g true -i true"
|
krauss@42973
|
52 |
Z3_NON_COMMERCIAL="yes"
|
krauss@42977
|
53 |
%s
|
krauss@42977
|
54 |
''' % (isabelle_path, parallelism_options, more_settings)
|
haftmann@41790
|
55 |
|
haftmann@41790
|
56 |
writer = open(path.join(loc_isabelle, 'etc', 'settings'), 'a')
|
haftmann@41790
|
57 |
writer.write(extra_settings)
|
haftmann@41790
|
58 |
writer.close()
|
haftmann@41790
|
59 |
|
haftmann@41790
|
60 |
|
haftmann@41790
|
61 |
def extract_isabelle_run_timing(logdata):
|
haftmann@41790
|
62 |
|
haftmann@41790
|
63 |
def to_secs(h, m, s):
|
haftmann@41790
|
64 |
return (int(h) * 60 + int(m)) * 60 + int(s)
|
haftmann@41790
|
65 |
pat = r'Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time'
|
krauss@43057
|
66 |
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
|
67 |
t = dict((name, {'elapsed': to_secs(eh,em,es), 'cpu': to_secs(ch,cm,cs)})
|
haftmann@41790
|
68 |
for name, eh, em, es, ch, cm, cs in re.findall(pat, logdata))
|
krauss@43057
|
69 |
for name, threads, elapsed, cpu, gc, factor in re.findall(pat2, logdata):
|
haftmann@41790
|
70 |
|
haftmann@41790
|
71 |
if name not in t:
|
haftmann@41790
|
72 |
t[name] = {}
|
haftmann@41790
|
73 |
|
haftmann@41790
|
74 |
t[name]['threads'] = int(threads)
|
haftmann@41790
|
75 |
t[name]['elapsed_inner'] = elapsed
|
haftmann@41790
|
76 |
t[name]['cpu_inner'] = cpu
|
haftmann@41790
|
77 |
t[name]['gc'] = gc
|
krauss@43057
|
78 |
t[name]['factor'] = factor
|
haftmann@41790
|
79 |
|
haftmann@41790
|
80 |
return t
|
haftmann@41790
|
81 |
|
haftmann@41790
|
82 |
|
haftmann@41790
|
83 |
def extract_isabelle_run_summary(logdata):
|
haftmann@41790
|
84 |
|
krauss@42765
|
85 |
re_error = re.compile(r'^(?:make: )?\*\*\* (.*)$', re.MULTILINE)
|
haftmann@41790
|
86 |
summary = '\n'.join(re_error.findall(logdata))
|
haftmann@41790
|
87 |
if summary == '':
|
haftmann@41790
|
88 |
summary = 'ok'
|
haftmann@41790
|
89 |
|
haftmann@41790
|
90 |
return summary
|
haftmann@41790
|
91 |
|
haftmann@41790
|
92 |
|
haftmann@41790
|
93 |
def isabelle_usedir(env, isa_path, isabelle_usedir_opts, base_image, dir_name):
|
haftmann@41790
|
94 |
|
haftmann@41790
|
95 |
return env.run_process('%s/bin/isabelle' % isa_path, 'usedir',
|
haftmann@41790
|
96 |
isabelle_usedir_opts, base_image, dir_name)
|
haftmann@41790
|
97 |
|
haftmann@41790
|
98 |
|
haftmann@41790
|
99 |
def isabelle_dependency_only(env, case, paths, dep_paths, playground):
|
haftmann@41790
|
100 |
|
krauss@42978
|
101 |
isabelle_home = paths[0]
|
krauss@42978
|
102 |
result = path.join(isabelle_home, 'heaps')
|
haftmann@41790
|
103 |
os.makedirs(result)
|
haftmann@41790
|
104 |
for dep_path in dep_paths:
|
haftmann@41790
|
105 |
subprocess.check_call(['cp', '-R'] + glob(dep_path + '/*') + [result])
|
haftmann@41790
|
106 |
|
haftmann@41790
|
107 |
return (True, 'ok', {}, {}, result)
|
haftmann@41790
|
108 |
|
haftmann@41790
|
109 |
|
krauss@42977
|
110 |
def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground, more_settings=''):
|
haftmann@41790
|
111 |
|
krauss@42978
|
112 |
isabelle_home = paths[0]
|
haftmann@41790
|
113 |
dep_path = dep_paths[0]
|
krauss@42984
|
114 |
prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, more_settings=more_settings)
|
krauss@42978
|
115 |
os.chdir(path.join(isabelle_home, 'src', subdir))
|
haftmann@41790
|
116 |
|
krauss@42978
|
117 |
(return_code, log) = isabelle_usedir(env, isabelle_home, '-b', base, img)
|
haftmann@41790
|
118 |
|
krauss@42978
|
119 |
result = path.join(isabelle_home, 'heaps')
|
haftmann@41790
|
120 |
return (return_code == 0, extract_isabelle_run_summary(log),
|
haftmann@41790
|
121 |
{'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
|
haftmann@41790
|
122 |
|
haftmann@41790
|
123 |
|
krauss@43011
|
124 |
def isabelle_make(subdir, env, case, paths, dep_paths, playground, more_settings='', target='all', keep_results=False):
|
krauss@42979
|
125 |
|
krauss@42979
|
126 |
isabelle_home = paths[0]
|
krauss@42979
|
127 |
dep_path = dep_paths[0] if dep_paths else None
|
krauss@42979
|
128 |
prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, more_settings=more_settings)
|
krauss@42979
|
129 |
os.chdir(path.join(isabelle_home, subdir))
|
krauss@42979
|
130 |
|
krauss@42979
|
131 |
(return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', '-k', target)
|
krauss@42979
|
132 |
|
krauss@43011
|
133 |
result = path.join(isabelle_home, 'heaps') if keep_results else None
|
krauss@42979
|
134 |
return (return_code == 0, extract_isabelle_run_summary(log),
|
krauss@43011
|
135 |
{'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
|
krauss@42979
|
136 |
|
krauss@42979
|
137 |
|
krauss@42985
|
138 |
def isabelle_makeall(env, case, paths, dep_paths, playground, more_settings='', target='all', make_options=()):
|
haftmann@41790
|
139 |
|
krauss@42978
|
140 |
isabelle_home = paths[0]
|
krauss@42979
|
141 |
dep_path = dep_paths[0] if dep_paths else None
|
krauss@42978
|
142 |
prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, more_settings=more_settings)
|
krauss@42978
|
143 |
os.chdir(isabelle_home)
|
haftmann@41790
|
144 |
|
krauss@42985
|
145 |
(return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'makeall', '-k', *(make_options + (target,)))
|
haftmann@41790
|
146 |
|
haftmann@41790
|
147 |
return (return_code == 0, extract_isabelle_run_summary(log),
|
haftmann@41790
|
148 |
{'timing': extract_isabelle_run_timing(log)}, {'log': log}, None)
|
haftmann@41790
|
149 |
|
haftmann@41790
|
150 |
|
haftmann@41790
|
151 |
# Isabelle configurations
|
haftmann@41790
|
152 |
|
haftmann@41790
|
153 |
@configuration(repos = [Isabelle], deps = [])
|
haftmann@41790
|
154 |
def Pure(env, case, paths, dep_paths, playground):
|
haftmann@41790
|
155 |
"""Pure image"""
|
haftmann@41790
|
156 |
|
krauss@42978
|
157 |
isabelle_home = paths[0]
|
krauss@42978
|
158 |
prepare_isabelle_repository(isabelle_home, env.settings.contrib, '')
|
krauss@42978
|
159 |
os.chdir(path.join(isabelle_home, 'src', 'Pure'))
|
haftmann@41790
|
160 |
|
krauss@42978
|
161 |
(return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure')
|
haftmann@41790
|
162 |
|
krauss@42978
|
163 |
result = path.join(isabelle_home, 'heaps')
|
haftmann@41790
|
164 |
return (return_code == 0, extract_isabelle_run_summary(log),
|
haftmann@41790
|
165 |
{'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
|
haftmann@41790
|
166 |
|
haftmann@41790
|
167 |
@configuration(repos = [Isabelle], deps = [(Pure, [0])])
|
haftmann@41790
|
168 |
def FOL(*args):
|
haftmann@41790
|
169 |
"""FOL image"""
|
haftmann@41790
|
170 |
return build_isabelle_image('FOL', 'Pure', 'FOL', *args)
|
haftmann@41790
|
171 |
|
haftmann@41790
|
172 |
@configuration(repos = [Isabelle], deps = [(Pure, [0])])
|
haftmann@41790
|
173 |
def HOL(*args):
|
haftmann@41790
|
174 |
"""HOL image"""
|
haftmann@41790
|
175 |
return build_isabelle_image('HOL', 'Pure', 'HOL', *args)
|
haftmann@41790
|
176 |
|
haftmann@41790
|
177 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
178 |
def HOL_HOLCF(*args):
|
haftmann@41790
|
179 |
"""HOL-HOLCF image"""
|
haftmann@41790
|
180 |
return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args)
|
haftmann@41790
|
181 |
|
haftmann@41790
|
182 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
183 |
def HOL_Nominal(*args):
|
haftmann@41790
|
184 |
"""HOL-Nominal image"""
|
haftmann@41790
|
185 |
return build_isabelle_image('HOL/Nominal', 'HOL', 'HOL-Nominal', *args)
|
haftmann@41790
|
186 |
|
haftmann@41790
|
187 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
188 |
def HOL_Word(*args):
|
haftmann@41790
|
189 |
"""HOL-Word image"""
|
haftmann@41790
|
190 |
return build_isabelle_image('HOL/Word', 'HOL', 'HOL-Word', *args)
|
haftmann@41790
|
191 |
|
haftmann@41790
|
192 |
@configuration(repos = [Isabelle], deps = [
|
haftmann@41790
|
193 |
(HOL, [0]),
|
haftmann@41790
|
194 |
(HOL_HOLCF, [0]),
|
haftmann@41790
|
195 |
(HOL_Nominal, [0]),
|
haftmann@41790
|
196 |
(HOL_Word, [0])
|
haftmann@41790
|
197 |
])
|
haftmann@41790
|
198 |
def AFP_images(*args):
|
haftmann@41790
|
199 |
"""Isabelle images needed for the AFP"""
|
haftmann@41790
|
200 |
return isabelle_dependency_only(*args)
|
haftmann@41790
|
201 |
|
haftmann@41790
|
202 |
@configuration(repos = [Isabelle], deps = [
|
haftmann@41790
|
203 |
(AFP_images, [0])
|
haftmann@41790
|
204 |
])
|
haftmann@41790
|
205 |
def Isabelle_makeall(*args):
|
haftmann@41790
|
206 |
"""Isabelle makeall"""
|
haftmann@41790
|
207 |
return isabelle_makeall(*args)
|
haftmann@41790
|
208 |
|
haftmann@41790
|
209 |
|
haftmann@41790
|
210 |
# Mutabelle configurations
|
haftmann@41790
|
211 |
|
haftmann@41790
|
212 |
def invoke_mutabelle(theory, env, case, paths, dep_paths, playground):
|
haftmann@41790
|
213 |
|
haftmann@41790
|
214 |
"""Mutant testing for counterexample generators in Isabelle"""
|
haftmann@41790
|
215 |
|
haftmann@41790
|
216 |
(loc_isabelle,) = paths
|
haftmann@41790
|
217 |
(dep_isabelle,) = dep_paths
|
haftmann@41790
|
218 |
prepare_isabelle_repository(loc_isabelle, env.settings.contrib, dep_isabelle)
|
haftmann@41790
|
219 |
os.chdir(loc_isabelle)
|
haftmann@41790
|
220 |
|
haftmann@41790
|
221 |
(return_code, log) = env.run_process('bin/isabelle',
|
haftmann@41790
|
222 |
'mutabelle', '-O', playground, theory)
|
haftmann@41790
|
223 |
|
haftmann@41790
|
224 |
try:
|
haftmann@41790
|
225 |
mutabelle_log = util.readfile(path.join(playground, 'log'))
|
haftmann@41790
|
226 |
except IOError:
|
haftmann@41790
|
227 |
mutabelle_log = ''
|
haftmann@41790
|
228 |
|
haftmann@41790
|
229 |
return (return_code == 0 and mutabelle_log != '', extract_isabelle_run_summary(log),
|
haftmann@42521
|
230 |
{'timing': extract_isabelle_run_timing(log)},
|
haftmann@42521
|
231 |
{'log': log, 'mutabelle_log': mutabelle_log}, None)
|
haftmann@41790
|
232 |
|
haftmann@41790
|
233 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
234 |
def Mutabelle_Relation(*args):
|
haftmann@41790
|
235 |
"""Mutabelle regression suite on Relation theory"""
|
haftmann@41790
|
236 |
return invoke_mutabelle('Relation', *args)
|
haftmann@41790
|
237 |
|
haftmann@41790
|
238 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
239 |
def Mutabelle_List(*args):
|
haftmann@41790
|
240 |
"""Mutabelle regression suite on List theory"""
|
haftmann@41790
|
241 |
return invoke_mutabelle('List', *args)
|
haftmann@41790
|
242 |
|
haftmann@41790
|
243 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
244 |
def Mutabelle_Set(*args):
|
haftmann@41790
|
245 |
"""Mutabelle regression suite on Set theory"""
|
haftmann@41790
|
246 |
return invoke_mutabelle('Set', *args)
|
haftmann@41790
|
247 |
|
haftmann@41790
|
248 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
249 |
def Mutabelle_Map(*args):
|
haftmann@41790
|
250 |
"""Mutabelle regression suite on Map theory"""
|
haftmann@41790
|
251 |
return invoke_mutabelle('Map', *args)
|
haftmann@41790
|
252 |
|
haftmann@41790
|
253 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
254 |
def Mutabelle_Divides(*args):
|
haftmann@41790
|
255 |
"""Mutabelle regression suite on Divides theory"""
|
haftmann@41790
|
256 |
return invoke_mutabelle('Divides', *args)
|
haftmann@41790
|
257 |
|
haftmann@41790
|
258 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
259 |
def Mutabelle_MacLaurin(*args):
|
haftmann@41790
|
260 |
"""Mutabelle regression suite on MacLaurin theory"""
|
haftmann@41790
|
261 |
return invoke_mutabelle('MacLaurin', *args)
|
haftmann@41790
|
262 |
|
haftmann@41790
|
263 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
haftmann@41790
|
264 |
def Mutabelle_Fun(*args):
|
haftmann@41790
|
265 |
"""Mutabelle regression suite on Fun theory"""
|
haftmann@41790
|
266 |
return invoke_mutabelle('Fun', *args)
|
krauss@42910
|
267 |
|
krauss@42910
|
268 |
|
krauss@42910
|
269 |
# Judgement Day configurations
|
krauss@42910
|
270 |
|
krauss@42959
|
271 |
judgement_day_provers = ('e', 'spass', 'vampire', 'z3', 'cvc3', 'yices')
|
krauss@42910
|
272 |
|
krauss@42910
|
273 |
def judgement_day(base_path, theory, opts, env, case, paths, dep_paths, playground):
|
krauss@42910
|
274 |
"""Judgement Day regression suite"""
|
krauss@42910
|
275 |
|
krauss@42910
|
276 |
isa = paths[0]
|
krauss@42910
|
277 |
dep_path = dep_paths[0]
|
krauss@42910
|
278 |
|
krauss@42910
|
279 |
os.chdir(path.join(playground, '..', base_path)) # Mirabelle requires specific cwd
|
krauss@42910
|
280 |
prepare_isabelle_repository(isa, env.settings.contrib, dep_path)
|
krauss@42910
|
281 |
|
krauss@42910
|
282 |
output = {}
|
krauss@42910
|
283 |
success_rates = {}
|
krauss@42910
|
284 |
some_success = False
|
krauss@42910
|
285 |
|
krauss@42910
|
286 |
for atp in judgement_day_provers:
|
krauss@42910
|
287 |
|
krauss@42910
|
288 |
log_dir = path.join(playground, 'mirabelle_log_' + atp)
|
krauss@42910
|
289 |
os.makedirs(log_dir)
|
krauss@42910
|
290 |
|
krauss@42910
|
291 |
cmd = ('%s/bin/isabelle mirabelle -q -O %s sledgehammer[prover=%s,%s] %s.thy'
|
krauss@42910
|
292 |
% (isa, log_dir, atp, opts, theory))
|
krauss@42910
|
293 |
|
krauss@42910
|
294 |
os.system(cmd)
|
krauss@42910
|
295 |
output[atp] = util.readfile(path.join(log_dir, theory + '.log'))
|
krauss@42910
|
296 |
|
krauss@42910
|
297 |
percentages = list(re.findall(r'Success rate: (\d+)%', output[atp]))
|
krauss@42910
|
298 |
if len(percentages) == 2:
|
krauss@42910
|
299 |
success_rates[atp] = {
|
krauss@42910
|
300 |
'sledgehammer': int(percentages[0]),
|
krauss@42910
|
301 |
'metis': int(percentages[1])}
|
krauss@42910
|
302 |
if success_rates[atp]['sledgehammer'] > 0:
|
krauss@42910
|
303 |
some_success = True
|
krauss@42910
|
304 |
else:
|
krauss@42910
|
305 |
success_rates[atp] = {}
|
krauss@42910
|
306 |
|
krauss@42910
|
307 |
|
krauss@42910
|
308 |
data = {'success_rates': success_rates}
|
krauss@42910
|
309 |
raw_attachments = dict((atp + "_output", output[atp]) for atp in judgement_day_provers)
|
krauss@42910
|
310 |
# FIXME: summary?
|
krauss@42910
|
311 |
return (some_success, '', data, raw_attachments, None)
|
krauss@42910
|
312 |
|
krauss@42910
|
313 |
|
krauss@42910
|
314 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
krauss@42910
|
315 |
def JD_NS(*args):
|
krauss@42910
|
316 |
"""Judgement Day regression suite NS"""
|
krauss@42910
|
317 |
return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
|
krauss@42910
|
318 |
|
krauss@42910
|
319 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
krauss@42910
|
320 |
def JD_FTA(*args):
|
krauss@42910
|
321 |
"""Judgement Day regression suite FTA"""
|
krauss@42910
|
322 |
return judgement_day('Isabelle/src/HOL/Library', 'Fundamental_Theorem_Algebra', 'prover_timeout=10', *args)
|
krauss@42910
|
323 |
|
krauss@42910
|
324 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
krauss@42910
|
325 |
def JD_Hoare(*args):
|
krauss@42910
|
326 |
"""Judgement Day regression suite Hoare"""
|
krauss@42913
|
327 |
return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args)
|
krauss@42910
|
328 |
|
krauss@42910
|
329 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])])
|
krauss@42910
|
330 |
def JD_SN(*args):
|
krauss@42910
|
331 |
"""Judgement Day regression suite SN"""
|
krauss@42913
|
332 |
return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
|
krauss@42910
|
333 |
|
krauss@42980
|
334 |
|
krauss@42980
|
335 |
# SML/NJ
|
krauss@42980
|
336 |
|
krauss@42980
|
337 |
smlnj_settings = '''
|
krauss@42980
|
338 |
ML_SYSTEM=smlnj
|
krauss@42980
|
339 |
ML_HOME="/home/smlnj/110.72/bin"
|
krauss@42980
|
340 |
ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
|
krauss@42980
|
341 |
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
|
krauss@42980
|
342 |
'''
|
krauss@42980
|
343 |
|
krauss@42980
|
344 |
@configuration(repos = [Isabelle], deps = [])
|
krauss@42980
|
345 |
def SML_HOL(*args):
|
krauss@42980
|
346 |
"""HOL image built with SML/NJ"""
|
krauss@43011
|
347 |
return isabelle_make('src/HOL', *args, more_settings=smlnj_settings, target='HOL', keep_results=True)
|
krauss@42980
|
348 |
|
krauss@42980
|
349 |
@configuration(repos = [Isabelle], deps = [])
|
krauss@42980
|
350 |
def SML_makeall(*args):
|
krauss@42980
|
351 |
"""Makeall built with SML/NJ"""
|
krauss@43002
|
352 |
return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3'))
|