author | blanchet |
Wed, 20 Feb 2013 09:58:28 +0100 | |
changeset 51195 | d995fae02981 |
parent 50600 | 48c0c3bc40dd |
child 53658 | 9e8714b4661a |
permissions | -rw-r--r-- |
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", "HOL-Library"))) |
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; hard-coding 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 |
48443 | 327 |
ML_HOME="/home/smlnj/110.74/bin" |
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/.arch-n-opsys" 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 |