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