author | haftmann |
Sat, 23 Jun 2012 20:34:21 +0200 | |
changeset 48149 | 9cb0abdf7c07 |
parent 47897 | 9d978604aee4 |
child 48155 | 1a6fa9b8140c |
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 |
|
42392 | 13 |
from util import Lazy |
41542 | 14 |
|
42392 | 15 |
from mira.report import Report, Report_Content |
16 |
from mira.case import Case |
|
17 |
from mira.tools import tool |
|
42823 | 18 |
from mira import schedule, misc |
42192 | 19 |
from mira.environment import scheduler |
46931 | 20 |
from mira import repositories |
42192 | 21 |
|
41542 | 22 |
# build and evaluation tools |
23 |
||
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
24 |
default_usedir_options = "$ISABELLE_USEDIR_OPTIONS -d pdf -g true -i true -t true" |
41542 | 25 |
|
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
26 |
def prepare_isabelle_repository(loc_isabelle, loc_contrib, loc_dependency_heaps, |
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
27 |
usedir_options=default_usedir_options, more_settings=''): |
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
28 |
|
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
29 |
# prepare components |
41542 | 30 |
loc_contrib = path.expanduser(loc_contrib) |
31 |
if not path.exists(loc_contrib): |
|
32 |
raise IOError('Bad file: %s' % loc_contrib) |
|
33 |
subprocess.check_call(['ln', '-s', loc_contrib, '%s/contrib' % loc_isabelle]) |
|
34 |
||
48149 | 35 |
components = path.join(loc_isabelle, 'Admin', 'components.common') |
36 |
if path.exists(components): |
|
41542 | 37 |
components = [] |
48149 | 38 |
for component in util.readfile_lines(components): |
41542 | 39 |
loc_component = path.join(loc_isabelle, component) |
40 |
if path.exists(loc_component): |
|
41 |
components.append(loc_component) |
|
42 |
writer = open(path.join(loc_isabelle, 'etc', 'components'), 'a') |
|
43 |
for component in components: |
|
44 |
writer.write(component + '\n') |
|
45 |
writer.close() |
|
46 |
||
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
47 |
# provide existing dependencies |
41542 | 48 |
if loc_dependency_heaps: |
49 |
isabelle_path = loc_dependency_heaps + '/$ISABELLE_IDENTIFIER:$ISABELLE_OUTPUT' |
|
50 |
else: |
|
51 |
isabelle_path = '$ISABELLE_OUTPUT' |
|
52 |
||
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
53 |
# patch settings |
41542 | 54 |
extra_settings = ''' |
55 |
ISABELLE_HOME_USER="$ISABELLE_HOME/home_user" |
|
56 |
ISABELLE_OUTPUT="$ISABELLE_HOME/heaps" |
|
57 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info" |
|
58 |
ISABELLE_PATH="%s" |
|
59 |
||
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
60 |
ISABELLE_USEDIR_OPTIONS="%s" |
47190 | 61 |
|
42109 | 62 |
Z3_NON_COMMERCIAL="yes" |
47190 | 63 |
|
42113 | 64 |
%s |
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
65 |
''' % (isabelle_path, usedir_options, more_settings) |
41542 | 66 |
|
67 |
writer = open(path.join(loc_isabelle, 'etc', 'settings'), 'a') |
|
68 |
writer.write(extra_settings) |
|
69 |
writer.close() |
|
70 |
||
71 |
||
45164 | 72 |
def isabelle_getenv(isabelle_home, var): |
73 |
||
74 |
_, out = env.run_process('%s/bin/isabelle' % isabelle_home, 'getenv', var) |
|
75 |
return out.split('=', 1)[1].strip() |
|
76 |
||
77 |
||
41542 | 78 |
def extract_isabelle_run_timing(logdata): |
79 |
||
80 |
def to_secs(h, m, s): |
|
81 |
return (int(h) * 60 + int(m)) * 60 + int(s) |
|
82 |
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
|
83 |
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 | 84 |
t = dict((name, {'elapsed': to_secs(eh,em,es), 'cpu': to_secs(ch,cm,cs)}) |
85 |
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
|
86 |
for name, threads, elapsed, cpu, gc, factor in re.findall(pat2, logdata): |
41542 | 87 |
|
88 |
if name not in t: |
|
89 |
t[name] = {} |
|
90 |
||
91 |
t[name]['threads'] = int(threads) |
|
92 |
t[name]['elapsed_inner'] = elapsed |
|
93 |
t[name]['cpu_inner'] = cpu |
|
94 |
t[name]['gc'] = gc |
|
42186
bb688200b949
adapted parsing of session timing (cf. e86b10c68f0b)
krauss
parents:
42140
diff
changeset
|
95 |
t[name]['factor'] = factor |
41542 | 96 |
|
97 |
return t |
|
98 |
||
99 |
||
100 |
def extract_isabelle_run_summary(logdata): |
|
101 |
||
41894 | 102 |
re_error = re.compile(r'^(?:make: )?\*\*\* (.*)$', re.MULTILINE) |
41542 | 103 |
summary = '\n'.join(re_error.findall(logdata)) |
104 |
if summary == '': |
|
105 |
summary = 'ok' |
|
106 |
||
107 |
return summary |
|
108 |
||
109 |
||
45164 | 110 |
def extract_image_size(isabelle_home): |
111 |
||
112 |
isabelle_output = isabelle_getenv(isabelle_home, 'ISABELLE_OUTPUT') |
|
113 |
return dict((p, path.getsize(path.join(isabelle_output, p))) for p in os.listdir(isabelle_output) if p != "log") |
|
114 |
||
115 |
def extract_report_data(isabelle_home, logdata): |
|
116 |
||
117 |
return { |
|
118 |
'timing': extract_isabelle_run_timing(logdata), |
|
119 |
'image_size': extract_image_size(isabelle_home) } |
|
120 |
||
121 |
||
42392 | 122 |
@tool |
123 |
def import_isatest_log(env, conf, logfile): |
|
124 |
||
125 |
"""Imports isatest log file as a report.""" |
|
126 |
||
127 |
def the_match(pat, text, name): |
|
128 |
match = re.search(pat, text) |
|
129 |
if not match: raise Exception('No match found for ' + name) |
|
130 |
return match.groups() |
|
131 |
||
132 |
def parse_date(d): |
|
133 |
return datetime.strptime(d, '%a %b %d %H:%M:%S %Z %Y') |
|
134 |
||
135 |
log = util.readfile(logfile) |
|
136 |
||
137 |
(begin_date, host) = the_match(r'-+ starting test -+ ([^-]*) -+ (\S*)', log, 'start tag') |
|
138 |
(isabelle_version,) = the_match(r'Isabelle version: ([a-f0-9]{12})', log, 'Isabelle version') |
|
139 |
(success, end_date) = the_match(r'-+ test (successful|FAILED) -+ ([^-]*) -', log, 'end tag') |
|
140 |
summary = extract_isabelle_run_summary(log) |
|
141 |
data = {'timing': extract_isabelle_run_timing(log)} |
|
142 |
atts = {'log': Lazy.simple(log)} |
|
143 |
||
144 |
content = Report_Content(summary, host, parse_date(begin_date), |
|
145 |
parse_date(end_date), Lazy.simple(data), atts) |
|
146 |
revision = ('Isabelle', env.repositories.get('Isabelle')[isabelle_version].hex()) |
|
147 |
case = Case(conf, [revision]) |
|
148 |
||
149 |
env.report_db.put(case, (success == 'successful'), content) |
|
150 |
||
151 |
||
152 |
||
41542 | 153 |
def isabelle_usedir(env, isa_path, isabelle_usedir_opts, base_image, dir_name): |
154 |
||
155 |
return env.run_process('%s/bin/isabelle' % isa_path, 'usedir', |
|
156 |
isabelle_usedir_opts, base_image, dir_name) |
|
157 |
||
158 |
||
159 |
def isabelle_dependency_only(env, case, paths, dep_paths, playground): |
|
160 |
||
42114 | 161 |
isabelle_home = paths[0] |
162 |
result = path.join(isabelle_home, 'heaps') |
|
41542 | 163 |
os.makedirs(result) |
164 |
for dep_path in dep_paths: |
|
165 |
subprocess.check_call(['cp', '-R'] + glob(dep_path + '/*') + [result]) |
|
166 |
||
167 |
return (True, 'ok', {}, {}, result) |
|
168 |
||
169 |
||
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
170 |
def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground, |
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
171 |
usedir_options=default_usedir_options, more_settings=''): |
41542 | 172 |
|
42114 | 173 |
isabelle_home = paths[0] |
41542 | 174 |
dep_path = dep_paths[0] |
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
175 |
prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, |
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
176 |
usedir_options=usedir_options, more_settings=more_settings) |
42114 | 177 |
os.chdir(path.join(isabelle_home, 'src', subdir)) |
41542 | 178 |
|
42114 | 179 |
(return_code, log) = isabelle_usedir(env, isabelle_home, '-b', base, img) |
41542 | 180 |
|
42114 | 181 |
result = path.join(isabelle_home, 'heaps') |
45164 | 182 |
|
41542 | 183 |
return (return_code == 0, extract_isabelle_run_summary(log), |
45164 | 184 |
extract_report_data(isabelle_home, log), {'log': log}, result) |
41542 | 185 |
|
186 |
||
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
187 |
def isabelle_make(subdir, env, case, paths, dep_paths, playground, usedir_options=default_usedir_options, |
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
188 |
more_settings='', target='all', keep_results=False): |
42115
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
189 |
|
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
190 |
isabelle_home = paths[0] |
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
191 |
dep_path = dep_paths[0] if dep_paths else None |
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
192 |
prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, |
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
193 |
usedir_options=usedir_options, more_settings=more_settings) |
42115
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
194 |
os.chdir(path.join(isabelle_home, subdir)) |
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
195 |
|
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
196 |
(return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', '-k', target) |
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
197 |
|
42140 | 198 |
result = path.join(isabelle_home, 'heaps') if keep_results else None |
45164 | 199 |
|
42115
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
200 |
return (return_code == 0, extract_isabelle_run_summary(log), |
45164 | 201 |
extract_report_data(isabelle_home, log), {'log': log}, result) |
42115
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
202 |
|
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
203 |
|
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
204 |
def isabelle_makeall(env, case, paths, dep_paths, playground, usedir_options=default_usedir_options, |
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
205 |
more_settings='', target='all', make_options=()): |
41542 | 206 |
|
42823 | 207 |
if 'lxbroy10' in misc.hostnames(): |
208 |
make_options += ('-j', '8') |
|
46200
4a892432e8f1
more modest settings for lxbroy10 -- might actually perform better;
wenzelm
parents:
45164
diff
changeset
|
209 |
usedir_options += " -M 4 -q 2 -i false -d false" |
42823 | 210 |
more_settings += ''' |
211 |
ML_PLATFORM="x86_64-linux" |
|
45157
efc2e2d80218
mira configuration: use official polyml 5.4.1 on lxbroy10
krauss
parents:
43903
diff
changeset
|
212 |
ML_HOME="/home/polyml/polyml-5.4.1/x86_64-linux" |
42823 | 213 |
ML_SYSTEM="polyml-5.4.1" |
46200
4a892432e8f1
more modest settings for lxbroy10 -- might actually perform better;
wenzelm
parents:
45164
diff
changeset
|
214 |
ML_OPTIONS="-H 4000 --gcthreads 4" |
43334
9970a4580d13
adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
bulwahn
parents:
43153
diff
changeset
|
215 |
|
9970a4580d13
adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
bulwahn
parents:
43153
diff
changeset
|
216 |
ISABELLE_GHC="/usr/bin/ghc" |
42823 | 217 |
''' |
218 |
||
42114 | 219 |
isabelle_home = paths[0] |
42115
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset
|
220 |
dep_path = dep_paths[0] if dep_paths else None |
42821
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
221 |
prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, |
4629cbaebc04
clarified handling of ISABELLE_USEDIR_OPTIONS in mira
krauss
parents:
42472
diff
changeset
|
222 |
usedir_options=usedir_options, more_settings=more_settings) |
42114 | 223 |
os.chdir(isabelle_home) |
41542 | 224 |
|
42121 | 225 |
(return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'makeall', '-k', *(make_options + (target,))) |
41542 | 226 |
|
227 |
return (return_code == 0, extract_isabelle_run_summary(log), |
|
45164 | 228 |
extract_report_data(isabelle_home, log), {'log': log}, None) |
41542 | 229 |
|
230 |
||
43689 | 231 |
def make_pure(env, case, paths, dep_paths, playground, more_settings=''): |
41542 | 232 |
|
42114 | 233 |
isabelle_home = paths[0] |
43689 | 234 |
prepare_isabelle_repository(isabelle_home, env.settings.contrib, '', |
235 |
more_settings=more_settings) |
|
42114 | 236 |
os.chdir(path.join(isabelle_home, 'src', 'Pure')) |
41542 | 237 |
|
42114 | 238 |
(return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure') |
41542 | 239 |
|
42114 | 240 |
result = path.join(isabelle_home, 'heaps') |
41542 | 241 |
return (return_code == 0, extract_isabelle_run_summary(log), |
242 |
{'timing': extract_isabelle_run_timing(log)}, {'log': log}, result) |
|
243 |
||
43689 | 244 |
|
245 |
# Isabelle configurations |
|
246 |
||
247 |
@configuration(repos = [Isabelle], deps = []) |
|
248 |
def Pure(*args): |
|
249 |
"""Pure image""" |
|
250 |
return make_pure(*args) |
|
251 |
||
41542 | 252 |
@configuration(repos = [Isabelle], deps = [(Pure, [0])]) |
253 |
def HOL(*args): |
|
254 |
"""HOL image""" |
|
255 |
return build_isabelle_image('HOL', 'Pure', 'HOL', *args) |
|
256 |
||
46934 | 257 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
258 |
def HOL_Library(*args): |
|
259 |
"""HOL-Library image""" |
|
260 |
return build_isabelle_image('HOL', 'HOL', 'HOL-Library', *args) |
|
261 |
||
262 |
@configuration(repos = [Isabelle], deps = [(Pure, [0])]) |
|
263 |
def ZF(*args): |
|
264 |
"""ZF image""" |
|
265 |
return build_isabelle_image('ZF', 'Pure', 'ZF', *args) |
|
266 |
||
267 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
|
268 |
def HOL_HOLCF(*args): |
|
269 |
"""HOLCF image""" |
|
270 |
return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args) |
|
271 |
||
47895 | 272 |
settings64=''' |
273 |
ML_PLATFORM=x86_64-linux |
|
274 |
ML_HOME="/home/polyml/polyml-5.4.1/x86_64-linux" |
|
275 |
ML_SYSTEM="polyml-5.4.1" |
|
276 |
''' |
|
277 |
||
47897 | 278 |
@configuration(repos = [Isabelle], deps = []) |
279 |
def Pure_64(*args): |
|
280 |
"""Pure image (64 bit)""" |
|
281 |
return make_pure(*args, more_settings=settings64) |
|
282 |
||
43689 | 283 |
@configuration(repos = [Isabelle], deps = [(Pure_64, [0])]) |
284 |
def HOL_64(*args): |
|
285 |
"""HOL image (64 bit)""" |
|
47895 | 286 |
return build_isabelle_image('HOL', 'Pure', 'HOL', *args, more_settings=settings64) |
43689 | 287 |
|
288 |
@configuration(repos = [Isabelle], deps = [(HOL_64, [0])]) |
|
289 |
def HOL_HOLCF_64(*args): |
|
290 |
"""HOL-HOLCF image (64 bit)""" |
|
47895 | 291 |
return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args, more_settings=settings64) |
41542 | 292 |
|
43689 | 293 |
@configuration(repos = [Isabelle], deps = [(HOL_64, [0])]) |
294 |
def HOL_Nominal_64(*args): |
|
295 |
"""HOL-Nominal image (64 bit)""" |
|
47895 | 296 |
return build_isabelle_image('HOL/Nominal', 'HOL', 'HOL-Nominal', *args, more_settings=settings64) |
41542 | 297 |
|
43689 | 298 |
@configuration(repos = [Isabelle], deps = [(HOL_64, [0])]) |
299 |
def HOL_Word_64(*args): |
|
300 |
"""HOL-Word image (64 bit)""" |
|
47895 | 301 |
return build_isabelle_image('HOL/Word', 'HOL', 'HOL-Word', *args, more_settings=settings64) |
41542 | 302 |
|
303 |
@configuration(repos = [Isabelle], deps = [ |
|
43689 | 304 |
(HOL_64, [0]), |
305 |
(HOL_HOLCF_64, [0]), |
|
306 |
(HOL_Nominal_64, [0]), |
|
307 |
(HOL_Word_64, [0]) |
|
41542 | 308 |
]) |
309 |
def AFP_images(*args): |
|
43689 | 310 |
"""Isabelle images needed for the AFP (64 bit)""" |
41542 | 311 |
return isabelle_dependency_only(*args) |
312 |
||
42822
dc7232f0c303
no dependencies for Isabelle_makeall, which will be built in one go
krauss
parents:
42821
diff
changeset
|
313 |
@configuration(repos = [Isabelle], deps = []) |
41542 | 314 |
def Isabelle_makeall(*args): |
315 |
"""Isabelle makeall""" |
|
316 |
return isabelle_makeall(*args) |
|
317 |
||
318 |
||
46934 | 319 |
# distribution and documentation Build |
46931 | 320 |
|
321 |
@configuration(repos = [Isabelle], deps = []) |
|
322 |
def Distribution(env, case, paths, dep_paths, playground): |
|
46934 | 323 |
"""Build of distribution""" |
46931 | 324 |
## FIXME This is rudimentary; study Admin/CHECKLIST to complete this configuration accordingly |
325 |
isabelle_home = paths[0] |
|
46934 | 326 |
(return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'makedist'), |
46931 | 327 |
REPOS = repositories.get(Isabelle).local_path, DISTPREFIX = os.getcwd()) |
328 |
return (return_code == 0, '', ## FIXME might add summary here |
|
329 |
{}, {'log': log}, None) ## FIXME might add proper result here |
|
330 |
||
46934 | 331 |
@configuration(repos = [Isabelle], deps = [ |
332 |
(HOL, [0]), |
|
333 |
(HOL_HOLCF, [0]), |
|
334 |
(ZF, [0]), |
|
335 |
(HOL_Library, [0]) |
|
336 |
]) |
|
337 |
def Documentation_images(*args): |
|
338 |
"""Isabelle images needed to build the documentation""" |
|
339 |
return isabelle_dependency_only(*args) |
|
340 |
||
341 |
@configuration(repos = [Isabelle], deps = [(Documentation_images, [0])]) |
|
342 |
def Documentation(env, case, paths, dep_paths, playground): |
|
343 |
"""Build of documentation""" |
|
344 |
isabelle_home = paths[0] |
|
345 |
dep_path = dep_paths[0] |
|
346 |
prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, |
|
347 |
usedir_options = default_usedir_options) |
|
348 |
(return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'build', 'doc-src')) |
|
349 |
return (return_code == 0, extract_isabelle_run_summary(log), |
|
350 |
extract_report_data(isabelle_home, log), {'log': log}, None) |
|
351 |
||
46931 | 352 |
|
41542 | 353 |
# Mutabelle configurations |
354 |
||
355 |
def invoke_mutabelle(theory, env, case, paths, dep_paths, playground): |
|
356 |
||
357 |
"""Mutant testing for counterexample generators in Isabelle""" |
|
358 |
||
359 |
(loc_isabelle,) = paths |
|
360 |
(dep_isabelle,) = dep_paths |
|
43152
6c4e021dec06
adding more settings to mira's mutabelle configuration
bulwahn
parents:
42948
diff
changeset
|
361 |
more_settings = ''' |
43153
cbb748ccf81b
changing the mira setting again for the mutabelle configuration
bulwahn
parents:
43152
diff
changeset
|
362 |
ISABELLE_GHC="/usr/bin/ghc" |
43152
6c4e021dec06
adding more settings to mira's mutabelle configuration
bulwahn
parents:
42948
diff
changeset
|
363 |
''' |
6c4e021dec06
adding more settings to mira's mutabelle configuration
bulwahn
parents:
42948
diff
changeset
|
364 |
prepare_isabelle_repository(loc_isabelle, env.settings.contrib, dep_isabelle, |
6c4e021dec06
adding more settings to mira's mutabelle configuration
bulwahn
parents:
42948
diff
changeset
|
365 |
more_settings = more_settings) |
41542 | 366 |
os.chdir(loc_isabelle) |
367 |
||
368 |
(return_code, log) = env.run_process('bin/isabelle', |
|
369 |
'mutabelle', '-O', playground, theory) |
|
370 |
||
371 |
try: |
|
372 |
mutabelle_log = util.readfile(path.join(playground, 'log')) |
|
373 |
except IOError: |
|
374 |
mutabelle_log = '' |
|
375 |
||
42472 | 376 |
mutabelle_data = dict( |
377 |
(tool, {'counterexample': c, 'no_counterexample': n, 'timeout': t, 'error': e}) |
|
378 |
for tool, c, n, t, e in re.findall(r'(\S+)\s+: C: (\d+) N: (\d+) T: (\d+) E: (\d+)', log)) |
|
379 |
||
41542 | 380 |
return (return_code == 0 and mutabelle_log != '', extract_isabelle_run_summary(log), |
42472 | 381 |
{'mutabelle_results': {theory: mutabelle_data}}, |
41652 | 382 |
{'log': log, 'mutabelle_log': mutabelle_log}, None) |
41542 | 383 |
|
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
384 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
41542 | 385 |
def Mutabelle_Relation(*args): |
386 |
"""Mutabelle regression suite on Relation theory""" |
|
387 |
return invoke_mutabelle('Relation', *args) |
|
388 |
||
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
389 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
41542 | 390 |
def Mutabelle_List(*args): |
391 |
"""Mutabelle regression suite on List theory""" |
|
392 |
return invoke_mutabelle('List', *args) |
|
393 |
||
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
394 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
41542 | 395 |
def Mutabelle_Set(*args): |
396 |
"""Mutabelle regression suite on Set theory""" |
|
397 |
return invoke_mutabelle('Set', *args) |
|
398 |
||
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
399 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
41542 | 400 |
def Mutabelle_Map(*args): |
401 |
"""Mutabelle regression suite on Map theory""" |
|
402 |
return invoke_mutabelle('Map', *args) |
|
403 |
||
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
404 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
41542 | 405 |
def Mutabelle_Divides(*args): |
406 |
"""Mutabelle regression suite on Divides theory""" |
|
407 |
return invoke_mutabelle('Divides', *args) |
|
408 |
||
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
409 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
41542 | 410 |
def Mutabelle_MacLaurin(*args): |
411 |
"""Mutabelle regression suite on MacLaurin theory""" |
|
412 |
return invoke_mutabelle('MacLaurin', *args) |
|
413 |
||
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
414 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
41542 | 415 |
def Mutabelle_Fun(*args): |
416 |
"""Mutabelle regression suite on Fun theory""" |
|
417 |
return invoke_mutabelle('Fun', *args) |
|
42040 | 418 |
|
42393 | 419 |
mutabelle_confs = 'Mutabelle_Relation Mutabelle_List Mutabelle_Set Mutabelle_Map Mutabelle_Divides Mutabelle_MacLaurin Mutabelle_Fun'.split(' ') |
420 |
||
421 |
@scheduler() |
|
422 |
def mutabelle_scheduler(env): |
|
423 |
"""Scheduler for Mutabelle.""" |
|
424 |
return schedule.age_scheduler(env, 'Isabelle', mutabelle_confs) |
|
42040 | 425 |
|
47896 | 426 |
|
42040 | 427 |
# Judgement Day configurations |
428 |
||
42095 | 429 |
judgement_day_provers = ('e', 'spass', 'vampire', 'z3', 'cvc3', 'yices') |
42040 | 430 |
|
431 |
def judgement_day(base_path, theory, opts, env, case, paths, dep_paths, playground): |
|
432 |
"""Judgement Day regression suite""" |
|
433 |
||
434 |
isa = paths[0] |
|
435 |
dep_path = dep_paths[0] |
|
436 |
||
437 |
os.chdir(path.join(playground, '..', base_path)) # Mirabelle requires specific cwd |
|
438 |
prepare_isabelle_repository(isa, env.settings.contrib, dep_path) |
|
439 |
||
440 |
output = {} |
|
441 |
success_rates = {} |
|
442 |
some_success = False |
|
443 |
||
444 |
for atp in judgement_day_provers: |
|
445 |
||
446 |
log_dir = path.join(playground, 'mirabelle_log_' + atp) |
|
447 |
os.makedirs(log_dir) |
|
448 |
||
449 |
cmd = ('%s/bin/isabelle mirabelle -q -O %s sledgehammer[prover=%s,%s] %s.thy' |
|
450 |
% (isa, log_dir, atp, opts, theory)) |
|
451 |
||
452 |
os.system(cmd) |
|
453 |
output[atp] = util.readfile(path.join(log_dir, theory + '.log')) |
|
454 |
||
455 |
percentages = list(re.findall(r'Success rate: (\d+)%', output[atp])) |
|
456 |
if len(percentages) == 2: |
|
457 |
success_rates[atp] = { |
|
458 |
'sledgehammer': int(percentages[0]), |
|
459 |
'metis': int(percentages[1])} |
|
460 |
if success_rates[atp]['sledgehammer'] > 0: |
|
461 |
some_success = True |
|
462 |
else: |
|
463 |
success_rates[atp] = {} |
|
464 |
||
465 |
||
466 |
data = {'success_rates': success_rates} |
|
467 |
raw_attachments = dict((atp + "_output", output[atp]) for atp in judgement_day_provers) |
|
468 |
# FIXME: summary? |
|
469 |
return (some_success, '', data, raw_attachments, None) |
|
470 |
||
471 |
||
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
472 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
42040 | 473 |
def JD_NS(*args): |
474 |
"""Judgement Day regression suite NS""" |
|
475 |
return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args) |
|
476 |
||
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
477 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
42040 | 478 |
def JD_FTA(*args): |
479 |
"""Judgement Day regression suite FTA""" |
|
480 |
return judgement_day('Isabelle/src/HOL/Library', 'Fundamental_Theorem_Algebra', 'prover_timeout=10', *args) |
|
481 |
||
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
482 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
42040 | 483 |
def JD_Hoare(*args): |
484 |
"""Judgement Day regression suite Hoare""" |
|
42058
1eda69f0b9a8
moved some configurations to AFP, and fixed others
krauss
parents:
42040
diff
changeset
|
485 |
return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args) |
42040 | 486 |
|
42948
e6990acab6ff
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset
|
487 |
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) |
42040 | 488 |
def JD_SN(*args): |
489 |
"""Judgement Day regression suite SN""" |
|
42058
1eda69f0b9a8
moved some configurations to AFP, and fixed others
krauss
parents:
42040
diff
changeset
|
490 |
return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args) |
42040 | 491 |
|
42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
492 |
|
42192 | 493 |
JD_confs = 'JD_NS JD_FTA JD_Hoare JD_SN JD_Arrow JD_FFT JD_Jinja JD_QE JD_S2S'.split(' ') |
494 |
||
495 |
@scheduler() |
|
42197 | 496 |
def judgement_day_scheduler(env): |
42192 | 497 |
"""Scheduler for Judgement Day.""" |
498 |
return schedule.age_scheduler(env, 'Isabelle', JD_confs) |
|
499 |
||
500 |
||
42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
501 |
# SML/NJ |
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
502 |
|
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
503 |
smlnj_settings = ''' |
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
504 |
ML_SYSTEM=smlnj |
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
505 |
ML_HOME="/home/smlnj/110.72/bin" |
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
506 |
ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256" |
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
507 |
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
|
508 |
''' |
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
509 |
|
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
510 |
@configuration(repos = [Isabelle], deps = []) |
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
511 |
def SML_HOL(*args): |
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
512 |
"""HOL image built with SML/NJ""" |
42140 | 513 |
return isabelle_make('src/HOL', *args, more_settings=smlnj_settings, target='HOL', keep_results=True) |
42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
514 |
|
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
515 |
@configuration(repos = [Isabelle], deps = []) |
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
516 |
def SML_makeall(*args): |
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset
|
517 |
"""Makeall built with SML/NJ""" |
42138
e54a985daa61
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
krauss
parents:
42121
diff
changeset
|
518 |
return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3')) |
43894
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
519 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
520 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
521 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
522 |
# Importer |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
523 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
524 |
@configuration(repos = ['Hollight'], deps = []) |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
525 |
def Hollight_proof_objects(env, case, paths, dep_paths, playground): |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
526 |
"""Build proof object bundle from HOL Light""" |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
527 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
528 |
hollight_home = paths[0] |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
529 |
os.chdir(os.path.join(hollight_home, 'Proofrecording', 'hol_light')) |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
530 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
531 |
subprocess.check_call(['make']) |
43897 | 532 |
(return_code, _) = util.run_process.run_process( |
43894
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
533 |
'''echo -e '#use "hol.ml";;\n export_saved_proofs None;;' | ocaml''', |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
534 |
environment={'HOLPROOFEXPORTDIR': './proofs_extended', 'HOLPROOFOBJECTS': 'EXTENDED'}, |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
535 |
shell=True) |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
536 |
subprocess.check_call('tar -czf proofs_extended.tar.gz proofs_extended'.split(' ')) |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
537 |
subprocess.check_call(['mv', 'proofs_extended.tar.gz', playground]) |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
538 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
539 |
return (return_code == 0, '', {}, {}, playground) |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
540 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
541 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
542 |
@configuration(repos = [Isabelle, 'Hollight'], deps = [(Hollight_proof_objects, [1])]) |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
543 |
def HOL_Generate_HOLLight(env, case, paths, dep_paths, playground): |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
544 |
"""Generated theories by HOL Light import""" |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
545 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
546 |
os.chdir(playground) |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
547 |
subprocess.check_call(['tar', '-xzf', path.join(dep_paths[0], 'proofs_extended.tar.gz')]) |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
548 |
proofs_dir = path.join(playground, 'proofs_extended') |
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
549 |
|
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset
|
550 |
return isabelle_make('src/HOL', env, case, paths, dep_paths, playground, |
43903 | 551 |
more_settings=('HOL4_PROOFS="%s"' % proofs_dir), target='HOL-Generate-HOLLight') |