author  krauss 
Sun, 05 Aug 2012 22:00:59 +0200  
changeset 48686  4cf09bc175d7 
parent 48685  9f9b289964dc 
child 48687  968ecd2bca88 
permissions  rwrr 
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: ([af09]{12})', log, 'Isabelle version') 

129 
(success, end_date) = the_match(r'+ test (successfulFAILED) + ([^]*) ', 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 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

142 
def isabelle_build(env, case, paths, dep_paths, playground, *cmdargs, **kwargs): 
41542  143 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

144 
more_settings=kwargs.get('more_settings', '') 
41542  145 

42114  146 
isabelle_home = paths[0] 
41542  147 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

148 
# copy over build results from dependencies 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

149 
heap_dir = path.join(isabelle_home, 'heaps') 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

150 
classes_dir = path.join(heap_dir, 'classes') 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

151 
os.makedirs(classes_dir) 
42115
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset

152 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

153 
for dep_path in dep_paths: 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

154 
subprocess.check_call(['cp', 'a'] + glob(dep_path + '/*') + [heap_dir]) 
45164  155 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

156 
subprocess.check_call(['ln', 's', classes_dir, path.join(isabelle_home, 'lib', 'classes')]) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

157 
jars = glob(path.join(classes_dir, 'ext', '*.jar')) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

158 
if jars: 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

159 
subprocess.check_call(['touch'] + jars) 
42115
e6a1dc0aa058
mira interface to 'isabelle make' in addition to usedir and makeall;
krauss
parents:
42114
diff
changeset

160 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

161 
# misc preparations 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

162 
if 'lxbroy10' in misc.hostnames(): # special settings for lxbroy10 
42823  163 
more_settings += ''' 
164 
ML_PLATFORM="x86_64linux" 

45157
efc2e2d80218
mira configuration: use official polyml 5.4.1 on lxbroy10
krauss
parents:
43903
diff
changeset

165 
ML_HOME="/home/polyml/polyml5.4.1/x86_64linux" 
42823  166 
ML_SYSTEM="polyml5.4.1" 
46200
4a892432e8f1
more modest settings for lxbroy10  might actually perform better;
wenzelm
parents:
45164
diff
changeset

167 
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

168 

9970a4580d13
adding ISABELLE_GHC environment setting to mira configuration isabelle makeall all on lxbroy10
bulwahn
parents:
43153
diff
changeset

169 
ISABELLE_GHC="/usr/bin/ghc" 
42823  170 
''' 
171 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

172 
prepare_isabelle_repository(isabelle_home, env.settings.contrib, None, 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

173 
usedir_options="", more_settings=more_settings) 
42114  174 
os.chdir(isabelle_home) 
41542  175 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

176 
# invoke build tool 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

177 
(return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'build', 's', 'v', *cmdargs) 
41542  178 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

179 
# collect report 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

180 
return (return_code == 0, extract_isabelle_run_summary(log), 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

181 
extract_report_data(isabelle_home, log), {'log': log}, heap_dir) 
41542  182 

183 

43689  184 

185 
# Isabelle configurations 

186 

187 
@configuration(repos = [Isabelle], deps = []) 

188 
def Pure(*args): 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

189 
"""Pure Image""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

190 
return isabelle_build(*(args + ("b", "Pure"))) 
43689  191 

41542  192 
@configuration(repos = [Isabelle], deps = [(Pure, [0])]) 
193 
def HOL(*args): 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

194 
"""HOL Image""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

195 
return isabelle_build(*(args + ("b", "HOL"))) 
41542  196 

46934  197 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
198 
def HOL_Library(*args): 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

199 
"""HOL Library""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

200 
return isabelle_build(*(args + ("b", "HOLLibrary"))) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

201 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

202 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

203 
def HOL_HOLCF(*args): 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

204 
"""HOLCF""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

205 
return isabelle_build(*(args + ("b", "HOLHOLCF"))) 
46934  206 

207 
@configuration(repos = [Isabelle], deps = [(Pure, [0])]) 

208 
def ZF(*args): 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

209 
"""HOLCF""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

210 
return isabelle_build(*(args + ("b", "ZF"))) 
46934  211 

212 

47895  213 
settings64=''' 
214 
ML_PLATFORM=x86_64linux 

215 
ML_HOME="/home/polyml/polyml5.4.1/x86_64linux" 

216 
ML_SYSTEM="polyml5.4.1" 

217 
''' 

218 

47897  219 
@configuration(repos = [Isabelle], deps = []) 
220 
def Pure_64(*args): 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

221 
"""Pure Image (64 bit)""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

222 
return isabelle_build(*(args + ("b", "Pure")), more_settings=settings64) 
47897  223 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

224 
@configuration(repos = [Isabelle], deps = [(Pure, [0])]) 
43689  225 
def HOL_64(*args): 
48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

226 
"""HOL Image (64 bit)""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

227 
return isabelle_build(*(args + ("b", "HOL")), more_settings=settings64) 
41542  228 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

229 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

230 
def HOL_HOLCF_64(*args): 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

231 
"""HOLCF Image""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

232 
return isabelle_build(*(args + ("b", "HOLHOLCF")), more_settings=settings64) 
41542  233 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

234 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
43689  235 
def HOL_Word_64(*args): 
48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

236 
"""HOLWord Image""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

237 
return isabelle_build(*(args + ("b", "HOLWord")), more_settings=settings64) 
41542  238 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

239 
@configuration(repos = [Isabelle], deps = []) 
41542  240 
def AFP_images(*args): 
43689  241 
"""Isabelle images needed for the AFP (64 bit)""" 
48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

242 
return isabelle_build(*(args + ("b", "j", "2", "Pure", "HOL", "HOLHOLCF", "HOLWord")), more_settings=settings64) 
41542  243 

42822
dc7232f0c303
no dependencies for Isabelle_makeall, which will be built in one go
krauss
parents:
42821
diff
changeset

244 
@configuration(repos = [Isabelle], deps = []) 
41542  245 
def Isabelle_makeall(*args): 
48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

246 
"""Build all sessions""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

247 
return isabelle_build(*(args + ("j", "6", "o", "threads=4", "a")), more_settings=settings64) 
46934  248 

46931  249 

41542  250 
# Mutabelle configurations 
251 

252 
def invoke_mutabelle(theory, env, case, paths, dep_paths, playground): 

253 

254 
"""Mutant testing for counterexample generators in Isabelle""" 

255 

256 
(loc_isabelle,) = paths 

257 
(dep_isabelle,) = dep_paths 

43152
6c4e021dec06
adding more settings to mira's mutabelle configuration
bulwahn
parents:
42948
diff
changeset

258 
more_settings = ''' 
43153
cbb748ccf81b
changing the mira setting again for the mutabelle configuration
bulwahn
parents:
43152
diff
changeset

259 
ISABELLE_GHC="/usr/bin/ghc" 
43152
6c4e021dec06
adding more settings to mira's mutabelle configuration
bulwahn
parents:
42948
diff
changeset

260 
''' 
6c4e021dec06
adding more settings to mira's mutabelle configuration
bulwahn
parents:
42948
diff
changeset

261 
prepare_isabelle_repository(loc_isabelle, env.settings.contrib, dep_isabelle, 
6c4e021dec06
adding more settings to mira's mutabelle configuration
bulwahn
parents:
42948
diff
changeset

262 
more_settings = more_settings) 
41542  263 
os.chdir(loc_isabelle) 
264 

265 
(return_code, log) = env.run_process('bin/isabelle', 

266 
'mutabelle', 'O', playground, theory) 

267 

268 
try: 

269 
mutabelle_log = util.readfile(path.join(playground, 'log')) 

270 
except IOError: 

271 
mutabelle_log = '' 

272 

42472  273 
mutabelle_data = dict( 
274 
(tool, {'counterexample': c, 'no_counterexample': n, 'timeout': t, 'error': e}) 

275 
for tool, c, n, t, e in re.findall(r'(\S+)\s+: C: (\d+) N: (\d+) T: (\d+) E: (\d+)', log)) 

276 

41542  277 
return (return_code == 0 and mutabelle_log != '', extract_isabelle_run_summary(log), 
42472  278 
{'mutabelle_results': {theory: mutabelle_data}}, 
41652  279 
{'log': log, 'mutabelle_log': mutabelle_log}, None) 
41542  280 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

281 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  282 
def Mutabelle_Relation(*args): 
283 
"""Mutabelle regression suite on Relation theory""" 

284 
return invoke_mutabelle('Relation', *args) 

285 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

286 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  287 
def Mutabelle_List(*args): 
288 
"""Mutabelle regression suite on List theory""" 

289 
return invoke_mutabelle('List', *args) 

290 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

291 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  292 
def Mutabelle_Set(*args): 
293 
"""Mutabelle regression suite on Set theory""" 

294 
return invoke_mutabelle('Set', *args) 

295 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

296 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  297 
def Mutabelle_Map(*args): 
298 
"""Mutabelle regression suite on Map theory""" 

299 
return invoke_mutabelle('Map', *args) 

300 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

301 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  302 
def Mutabelle_Divides(*args): 
303 
"""Mutabelle regression suite on Divides theory""" 

304 
return invoke_mutabelle('Divides', *args) 

305 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

306 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  307 
def Mutabelle_MacLaurin(*args): 
308 
"""Mutabelle regression suite on MacLaurin theory""" 

309 
return invoke_mutabelle('MacLaurin', *args) 

310 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

311 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
41542  312 
def Mutabelle_Fun(*args): 
313 
"""Mutabelle regression suite on Fun theory""" 

314 
return invoke_mutabelle('Fun', *args) 

42040  315 

42393  316 
mutabelle_confs = 'Mutabelle_Relation Mutabelle_List Mutabelle_Set Mutabelle_Map Mutabelle_Divides Mutabelle_MacLaurin Mutabelle_Fun'.split(' ') 
317 

318 
@scheduler() 

319 
def mutabelle_scheduler(env): 

320 
"""Scheduler for Mutabelle.""" 

321 
return schedule.age_scheduler(env, 'Isabelle', mutabelle_confs) 

42040  322 

47896  323 

42040  324 
# Judgement Day configurations 
325 

42095  326 
judgement_day_provers = ('e', 'spass', 'vampire', 'z3', 'cvc3', 'yices') 
42040  327 

328 
def judgement_day(base_path, theory, opts, env, case, paths, dep_paths, playground): 

329 
"""Judgement Day regression suite""" 

330 

331 
isa = paths[0] 

332 
dep_path = dep_paths[0] 

333 

334 
os.chdir(path.join(playground, '..', base_path)) # Mirabelle requires specific cwd 

335 
prepare_isabelle_repository(isa, env.settings.contrib, dep_path) 

336 

337 
output = {} 

338 
success_rates = {} 

339 
some_success = False 

340 

341 
for atp in judgement_day_provers: 

342 

343 
log_dir = path.join(playground, 'mirabelle_log_' + atp) 

344 
os.makedirs(log_dir) 

345 

346 
cmd = ('%s/bin/isabelle mirabelle q O %s sledgehammer[prover=%s,%s] %s.thy' 

347 
% (isa, log_dir, atp, opts, theory)) 

348 

349 
os.system(cmd) 

350 
output[atp] = util.readfile(path.join(log_dir, theory + '.log')) 

351 

352 
percentages = list(re.findall(r'Success rate: (\d+)%', output[atp])) 

353 
if len(percentages) == 2: 

354 
success_rates[atp] = { 

355 
'sledgehammer': int(percentages[0]), 

356 
'metis': int(percentages[1])} 

357 
if success_rates[atp]['sledgehammer'] > 0: 

358 
some_success = True 

359 
else: 

360 
success_rates[atp] = {} 

361 

362 

363 
data = {'success_rates': success_rates} 

364 
raw_attachments = dict((atp + "_output", output[atp]) for atp in judgement_day_provers) 

365 
# FIXME: summary? 

366 
return (some_success, '', data, raw_attachments, None) 

367 

368 

42948
e6990acab6ff
reverted 7fdd8d4908dc  keeping images from Isabelle_makeall would be too expensive
krauss
parents:
42824
diff
changeset

369 
@configuration(repos = [Isabelle], deps = [(HOL, [0])]) 
42040  370 
def JD_NS(*args): 
371 
"""Judgement Day regression suite NS""" 

372 
return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args) 

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])]) 
42040  375 
def JD_FTA(*args): 
376 
"""Judgement Day regression suite FTA""" 

377 
return judgement_day('Isabelle/src/HOL/Library', 'Fundamental_Theorem_Algebra', 'prover_timeout=10', *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])]) 
42040  380 
def JD_Hoare(*args): 
381 
"""Judgement Day regression suite Hoare""" 

42058
1eda69f0b9a8
moved some configurations to AFP, and fixed others
krauss
parents:
42040
diff
changeset

382 
return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args) 
42040  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])]) 
42040  385 
def JD_SN(*args): 
386 
"""Judgement Day regression suite SN""" 

42058
1eda69f0b9a8
moved some configurations to AFP, and fixed others
krauss
parents:
42040
diff
changeset

387 
return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args) 
42040  388 

42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

389 

42192  390 
JD_confs = 'JD_NS JD_FTA JD_Hoare JD_SN JD_Arrow JD_FFT JD_Jinja JD_QE JD_S2S'.split(' ') 
391 

392 
@scheduler() 

42197  393 
def judgement_day_scheduler(env): 
42192  394 
"""Scheduler for Judgement Day.""" 
395 
return schedule.age_scheduler(env, 'Isabelle', JD_confs) 

396 

397 

42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

398 
# SML/NJ 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

399 

b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

400 
smlnj_settings = ''' 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

401 
ML_SYSTEM=smlnj 
48443  402 
ML_HOME="/home/smlnj/110.74/bin" 
403 
ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024" 

42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

404 
ML_PLATFORM=$(eval $("$ML_HOME/.archnopsys" 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

405 
''' 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

406 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

407 
@configuration(repos = [Isabelle], deps = [(Pure, [0])]) 
42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

408 
def SML_HOL(*args): 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

409 
"""HOL image built with SML/NJ""" 
48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

410 
return isabelle_build(*(args + ("b", "HOL")), more_settings=smlnj_settings) 
42116
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

411 

b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

412 
@configuration(repos = [Isabelle], deps = []) 
b9ae421fbcc7
added configurations SML_HOL and SML_makeall (even though the latter is practically infeasible)
krauss
parents:
42115
diff
changeset

413 
def SML_makeall(*args): 
48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

414 
"""SML/NJ build of all possible sessions""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

415 
return isabelle_build(*(args + ("j", "3", "a")), more_settings=smlnj_settings) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

416 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

417 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

418 
# Legacy Isabelle configurations 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

419 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

420 
# distribution and documentation Build 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

421 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

422 
@configuration(repos = [Isabelle], deps = []) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

423 
def Distribution(env, case, paths, dep_paths, playground): 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

424 
"""Build of distribution""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

425 
## FIXME This is rudimentary; study Admin/CHECKLIST to complete this configuration accordingly 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

426 
isabelle_home = paths[0] 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

427 
(return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'Release', 'makedist'), 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

428 
REPOS = repositories.get(Isabelle).local_path, DISTPREFIX = os.getcwd()) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

429 
return (return_code == 0, '', ## FIXME might add summary here 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

430 
{}, {'log': log}, None) ## FIXME might add proper result here 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

431 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

432 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

433 
def isabelle_dependency_only(env, case, paths, dep_paths, playground): 
43894
182caf5cf0b6
added experimental mira configuration for HOL Light importer
krauss
parents:
43689
diff
changeset

434 

48686
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

435 
isabelle_home = paths[0] 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

436 
result = path.join(isabelle_home, 'heaps') 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

437 
os.makedirs(result) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

438 
for dep_path in dep_paths: 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

439 
subprocess.check_call(['cp', 'R'] + glob(dep_path + '/*') + [result]) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

440 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

441 
return (True, 'ok', {}, {}, result) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

442 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

443 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

444 
@configuration(repos = [Isabelle], deps = [ 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

445 
(HOL, [0]), 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

446 
(HOL_HOLCF, [0]), 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

447 
(ZF, [0]), 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

448 
(HOL_Library, [0]) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

449 
]) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

450 
def Documentation_images(*args): 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

451 
"""Isabelle images needed to build the documentation""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

452 
return isabelle_dependency_only(*args) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

453 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

454 
@configuration(repos = [Isabelle], deps = [(Documentation_images, [0])]) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

455 
def Documentation(env, case, paths, dep_paths, playground): 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

456 
"""Build of documentation""" 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

457 
isabelle_home = paths[0] 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

458 
dep_path = dep_paths[0] 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

459 
prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path, 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

460 
usedir_options = default_usedir_options) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

461 
(return_code, log) = env.run_process(path.join(isabelle_home, 'Admin', 'build', 'docsrc')) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

462 
return (return_code == 0, extract_isabelle_run_summary(log), 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

463 
extract_report_data(isabelle_home, log), {'log': log}, None) 
4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

464 

4cf09bc175d7
modernized mira configurations, making use of isabelle build
krauss
parents:
48685
diff
changeset

465 