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