Admin/mira.py
author haftmann
Mon Jul 11 18:44:58 2011 +0200 (2011-07-11)
changeset 43764 366d5726de09
parent 43689 b8d79bd6029e
child 43894 182caf5cf0b6
permissions -rw-r--r--
explicit code equation for equality
     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
     9 from datetime import datetime
    10 import re
    11 
    12 import util
    13 from util import Lazy
    14 
    15 from mira.report import Report, Report_Content
    16 from mira.case import Case
    17 from mira.tools import tool
    18 from mira import schedule, misc
    19 from mira.environment import scheduler
    20 
    21 
    22 # build and evaluation tools
    23 
    24 default_usedir_options = "$ISABELLE_USEDIR_OPTIONS -d pdf -g true -i true -t true"
    25 
    26 def prepare_isabelle_repository(loc_isabelle, loc_contrib, loc_dependency_heaps,
    27   usedir_options=default_usedir_options, more_settings=''):
    28 
    29     # prepare components
    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 
    35     contributed_components = path.join(loc_isabelle, 'Admin', 'contributed_components')
    36     if path.exists(contributed_components):
    37         components = []
    38         for component in util.readfile_lines(contributed_components):
    39             loc_component = path.join(loc_isabelle, component)
    40             if path.exists(loc_component):
    41                 components.append(loc_component)
    42         writer = open(path.join(loc_isabelle, 'etc', 'components'), 'a')
    43         for component in components:
    44             writer.write(component + '\n')
    45         writer.close()
    46 
    47     # provide existing dependencies
    48     if loc_dependency_heaps:
    49         isabelle_path = loc_dependency_heaps + '/$ISABELLE_IDENTIFIER:$ISABELLE_OUTPUT'
    50     else:
    51         isabelle_path = '$ISABELLE_OUTPUT'
    52 
    53     # patch settings
    54     extra_settings = '''
    55 ISABELLE_HOME_USER="$ISABELLE_HOME/home_user"
    56 ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
    57 ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
    58 ISABELLE_PATH="%s"
    59 
    60 ISABELLE_USEDIR_OPTIONS="%s"
    61 Z3_NON_COMMERCIAL="yes"
    62 %s
    63 ''' % (isabelle_path, usedir_options, more_settings)
    64 
    65     writer = open(path.join(loc_isabelle, 'etc', 'settings'), 'a')
    66     writer.write(extra_settings)
    67     writer.close()
    68 
    69 
    70 def extract_isabelle_run_timing(logdata):
    71 
    72     def to_secs(h, m, s):
    73         return (int(h) * 60 + int(m)) * 60 + int(s)
    74     pat = r'Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time'
    75     pat2 = r'Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time, factor (\d+\.\d+)\)'
    76     t = dict((name, {'elapsed': to_secs(eh,em,es), 'cpu': to_secs(ch,cm,cs)})
    77              for name, eh, em, es, ch, cm, cs in re.findall(pat, logdata))
    78     for name, threads, elapsed, cpu, gc, factor in re.findall(pat2, logdata):
    79 
    80         if name not in t:
    81             t[name] = {}
    82 
    83         t[name]['threads'] = int(threads)
    84         t[name]['elapsed_inner'] = elapsed
    85         t[name]['cpu_inner'] = cpu
    86         t[name]['gc'] = gc
    87         t[name]['factor'] = factor
    88 
    89     return t
    90 
    91 
    92 def extract_isabelle_run_summary(logdata):
    93 
    94     re_error = re.compile(r'^(?:make: )?\*\*\* (.*)$', re.MULTILINE)
    95     summary = '\n'.join(re_error.findall(logdata))
    96     if summary == '':
    97         summary = 'ok'
    98 
    99     return summary
   100 
   101 
   102 @tool
   103 def import_isatest_log(env, conf, logfile):
   104 
   105     """Imports isatest log file as a report."""
   106 
   107     def the_match(pat, text, name):
   108         match = re.search(pat, text)
   109         if not match: raise Exception('No match found for ' + name)
   110         return match.groups()
   111 
   112     def parse_date(d):
   113         return datetime.strptime(d, '%a %b %d %H:%M:%S %Z %Y')
   114 
   115     log = util.readfile(logfile)
   116 
   117     (begin_date, host) = the_match(r'-+ starting test -+ ([^-]*) -+ (\S*)', log, 'start tag')
   118     (isabelle_version,) = the_match(r'Isabelle version: ([a-f0-9]{12})', log, 'Isabelle version')
   119     (success, end_date) = the_match(r'-+ test (successful|FAILED) -+ ([^-]*) -', log, 'end tag')
   120     summary = extract_isabelle_run_summary(log)
   121     data = {'timing': extract_isabelle_run_timing(log)}
   122     atts = {'log': Lazy.simple(log)}
   123 
   124     content = Report_Content(summary, host, parse_date(begin_date),
   125       parse_date(end_date), Lazy.simple(data), atts)
   126     revision = ('Isabelle', env.repositories.get('Isabelle')[isabelle_version].hex())
   127     case = Case(conf, [revision])
   128 
   129     env.report_db.put(case, (success == 'successful'), content)
   130 
   131 
   132 
   133 def isabelle_usedir(env, isa_path, isabelle_usedir_opts, base_image, dir_name):
   134 
   135     return env.run_process('%s/bin/isabelle' % isa_path, 'usedir',
   136         isabelle_usedir_opts, base_image, dir_name)
   137 
   138 
   139 def isabelle_dependency_only(env, case, paths, dep_paths, playground):
   140 
   141     isabelle_home = paths[0]
   142     result = path.join(isabelle_home, 'heaps')
   143     os.makedirs(result)
   144     for dep_path in dep_paths:
   145         subprocess.check_call(['cp', '-R'] + glob(dep_path + '/*') + [result])
   146 
   147     return (True, 'ok', {}, {}, result)
   148 
   149 
   150 def build_isabelle_image(subdir, base, img, env, case, paths, dep_paths, playground,
   151   usedir_options=default_usedir_options, more_settings=''):
   152 
   153     isabelle_home = paths[0]
   154     dep_path = dep_paths[0]
   155     prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
   156       usedir_options=usedir_options, more_settings=more_settings)
   157     os.chdir(path.join(isabelle_home, 'src', subdir))
   158 
   159     (return_code, log) = isabelle_usedir(env, isabelle_home, '-b', base, img)
   160 
   161     result = path.join(isabelle_home, 'heaps')
   162     return (return_code == 0, extract_isabelle_run_summary(log),
   163       {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
   164 
   165 
   166 def isabelle_make(subdir, env, case, paths, dep_paths, playground, usedir_options=default_usedir_options,
   167   more_settings='', target='all', keep_results=False):
   168 
   169     isabelle_home = paths[0]
   170     dep_path = dep_paths[0] if dep_paths else None
   171     prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
   172       usedir_options=usedir_options, more_settings=more_settings)
   173     os.chdir(path.join(isabelle_home, subdir))
   174 
   175     (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', '-k', target)
   176 
   177     result = path.join(isabelle_home, 'heaps') if keep_results else None
   178     return (return_code == 0, extract_isabelle_run_summary(log),
   179       {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
   180 
   181 
   182 def isabelle_makeall(env, case, paths, dep_paths, playground, usedir_options=default_usedir_options,
   183   more_settings='', target='all', make_options=()):
   184 
   185     # FIXME!?
   186     if 'lxbroy10' in misc.hostnames():
   187         make_options += ('-j', '8')
   188         usedir_options += " -M 6 -q 2 -i false -d false"
   189         more_settings += '''
   190 ML_PLATFORM="x86_64-linux"
   191 ML_HOME="/home/polyml/polyml-svn/x86_64-linux"
   192 ML_SYSTEM="polyml-5.4.1"
   193 ML_OPTIONS="-H 8000 --gcthreads 6"
   194 
   195 ISABELLE_GHC="/usr/bin/ghc"
   196 '''
   197 
   198     isabelle_home = paths[0]
   199     dep_path = dep_paths[0] if dep_paths else None
   200     prepare_isabelle_repository(isabelle_home, env.settings.contrib, dep_path,
   201       usedir_options=usedir_options, more_settings=more_settings)
   202     os.chdir(isabelle_home)
   203 
   204     (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'makeall', '-k', *(make_options + (target,)))
   205 
   206     return (return_code == 0, extract_isabelle_run_summary(log),
   207       {'timing': extract_isabelle_run_timing(log)}, {'log': log}, None)
   208 
   209 
   210 def make_pure(env, case, paths, dep_paths, playground, more_settings=''):
   211 
   212     isabelle_home = paths[0]
   213     prepare_isabelle_repository(isabelle_home, env.settings.contrib, '',
   214       more_settings=more_settings)
   215     os.chdir(path.join(isabelle_home, 'src', 'Pure'))
   216 
   217     (return_code, log) = env.run_process('%s/bin/isabelle' % isabelle_home, 'make', 'Pure')
   218 
   219     result = path.join(isabelle_home, 'heaps')
   220     return (return_code == 0, extract_isabelle_run_summary(log),
   221       {'timing': extract_isabelle_run_timing(log)}, {'log': log}, result)
   222 
   223 
   224 # Isabelle configurations
   225 
   226 @configuration(repos = [Isabelle], deps = [])
   227 def Pure(*args):
   228     """Pure image"""
   229     return make_pure(*args)
   230 
   231 @configuration(repos = [Isabelle], deps = [])
   232 def Pure_64(*args):
   233     """Pure image (64 bit)"""
   234     return make_pure(*args, more_settings='ML_PLATFORM=x86_64-linux')
   235 
   236 @configuration(repos = [Isabelle], deps = [(Pure, [0])])
   237 def HOL(*args):
   238     """HOL image"""
   239     return build_isabelle_image('HOL', 'Pure', 'HOL', *args)
   240 
   241 @configuration(repos = [Isabelle], deps = [(Pure_64, [0])])
   242 def HOL_64(*args):
   243     """HOL image (64 bit)"""
   244     return build_isabelle_image('HOL', 'Pure', 'HOL', *args, more_settings='ML_PLATFORM=x86_64-linux')
   245 
   246 @configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
   247 def HOL_HOLCF_64(*args):
   248     """HOL-HOLCF image (64 bit)"""
   249     return build_isabelle_image('HOL/HOLCF', 'HOL', 'HOLCF', *args, more_settings='ML_PLATFORM=x86_64-linux')
   250 
   251 @configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
   252 def HOL_Nominal_64(*args):
   253     """HOL-Nominal image (64 bit)"""
   254     return build_isabelle_image('HOL/Nominal', 'HOL', 'HOL-Nominal', *args, more_settings='ML_PLATFORM=x86_64-linux')
   255 
   256 @configuration(repos = [Isabelle], deps = [(HOL_64, [0])])
   257 def HOL_Word_64(*args):
   258     """HOL-Word image (64 bit)"""
   259     return build_isabelle_image('HOL/Word', 'HOL', 'HOL-Word', *args, more_settings='ML_PLATFORM=x86_64-linux')
   260 
   261 @configuration(repos = [Isabelle], deps = [
   262     (HOL_64, [0]),
   263     (HOL_HOLCF_64, [0]),
   264     (HOL_Nominal_64, [0]),
   265     (HOL_Word_64, [0])
   266   ])
   267 def AFP_images(*args):
   268     """Isabelle images needed for the AFP (64 bit)"""
   269     return isabelle_dependency_only(*args)
   270 
   271 @configuration(repos = [Isabelle], deps = [])
   272 def Isabelle_makeall(*args):
   273     """Isabelle makeall"""
   274     return isabelle_makeall(*args)
   275 
   276 
   277 # Mutabelle configurations
   278 
   279 def invoke_mutabelle(theory, env, case, paths, dep_paths, playground):
   280 
   281     """Mutant testing for counterexample generators in Isabelle"""
   282 
   283     (loc_isabelle,) = paths
   284     (dep_isabelle,) = dep_paths
   285     more_settings = '''
   286 ISABELLE_GHC="/usr/bin/ghc"
   287 '''
   288     prepare_isabelle_repository(loc_isabelle, env.settings.contrib, dep_isabelle,
   289       more_settings = more_settings)
   290     os.chdir(loc_isabelle)
   291     
   292     (return_code, log) = env.run_process('bin/isabelle',
   293       'mutabelle', '-O', playground, theory)
   294     
   295     try:
   296         mutabelle_log = util.readfile(path.join(playground, 'log'))
   297     except IOError:
   298         mutabelle_log = ''
   299 
   300     mutabelle_data = dict(
   301         (tool, {'counterexample': c, 'no_counterexample': n, 'timeout': t, 'error': e})
   302         for tool, c, n, t, e in re.findall(r'(\S+)\s+: C: (\d+) N: (\d+) T: (\d+) E: (\d+)', log))
   303 
   304     return (return_code == 0 and mutabelle_log != '', extract_isabelle_run_summary(log),
   305       {'mutabelle_results': {theory: mutabelle_data}},
   306       {'log': log, 'mutabelle_log': mutabelle_log}, None)
   307 
   308 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   309 def Mutabelle_Relation(*args):
   310     """Mutabelle regression suite on Relation theory"""
   311     return invoke_mutabelle('Relation', *args)
   312 
   313 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   314 def Mutabelle_List(*args):
   315     """Mutabelle regression suite on List theory"""
   316     return invoke_mutabelle('List', *args)
   317 
   318 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   319 def Mutabelle_Set(*args):
   320     """Mutabelle regression suite on Set theory"""
   321     return invoke_mutabelle('Set', *args)
   322 
   323 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   324 def Mutabelle_Map(*args):
   325     """Mutabelle regression suite on Map theory"""
   326     return invoke_mutabelle('Map', *args)
   327 
   328 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   329 def Mutabelle_Divides(*args):
   330     """Mutabelle regression suite on Divides theory"""
   331     return invoke_mutabelle('Divides', *args)
   332 
   333 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   334 def Mutabelle_MacLaurin(*args):
   335     """Mutabelle regression suite on MacLaurin theory"""
   336     return invoke_mutabelle('MacLaurin', *args)
   337 
   338 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   339 def Mutabelle_Fun(*args):
   340     """Mutabelle regression suite on Fun theory"""
   341     return invoke_mutabelle('Fun', *args)
   342 
   343 mutabelle_confs = 'Mutabelle_Relation Mutabelle_List Mutabelle_Set Mutabelle_Map Mutabelle_Divides Mutabelle_MacLaurin Mutabelle_Fun'.split(' ')
   344 
   345 @scheduler()
   346 def mutabelle_scheduler(env):
   347     """Scheduler for Mutabelle."""
   348     return schedule.age_scheduler(env, 'Isabelle', mutabelle_confs)
   349 
   350 # Judgement Day configurations
   351 
   352 judgement_day_provers = ('e', 'spass', 'vampire', 'z3', 'cvc3', 'yices')
   353 
   354 def judgement_day(base_path, theory, opts, env, case, paths, dep_paths, playground):
   355     """Judgement Day regression suite"""
   356 
   357     isa = paths[0]
   358     dep_path = dep_paths[0]
   359 
   360     os.chdir(path.join(playground, '..', base_path)) # Mirabelle requires specific cwd
   361     prepare_isabelle_repository(isa, env.settings.contrib, dep_path)
   362 
   363     output = {}
   364     success_rates = {}
   365     some_success = False
   366 
   367     for atp in judgement_day_provers:
   368 
   369         log_dir = path.join(playground, 'mirabelle_log_' + atp)
   370         os.makedirs(log_dir)
   371 
   372         cmd = ('%s/bin/isabelle mirabelle -q -O %s sledgehammer[prover=%s,%s] %s.thy'
   373                % (isa, log_dir, atp, opts, theory))
   374 
   375         os.system(cmd)
   376         output[atp] = util.readfile(path.join(log_dir, theory + '.log'))
   377 
   378         percentages = list(re.findall(r'Success rate: (\d+)%', output[atp]))
   379         if len(percentages) == 2:
   380             success_rates[atp] = {
   381                 'sledgehammer': int(percentages[0]),
   382                 'metis': int(percentages[1])}
   383             if success_rates[atp]['sledgehammer'] > 0:
   384                 some_success = True
   385         else:
   386             success_rates[atp] = {}
   387 
   388 
   389     data = {'success_rates': success_rates}
   390     raw_attachments = dict((atp + "_output", output[atp]) for atp in judgement_day_provers)
   391     # FIXME: summary?
   392     return (some_success, '', data, raw_attachments, None)
   393 
   394 
   395 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   396 def JD_NS(*args):
   397     """Judgement Day regression suite NS"""
   398     return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
   399 
   400 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   401 def JD_FTA(*args):
   402     """Judgement Day regression suite FTA"""
   403     return judgement_day('Isabelle/src/HOL/Library', 'Fundamental_Theorem_Algebra', 'prover_timeout=10', *args)
   404 
   405 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   406 def JD_Hoare(*args):
   407     """Judgement Day regression suite Hoare"""
   408     return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args)
   409 
   410 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   411 def JD_SN(*args):
   412     """Judgement Day regression suite SN"""
   413     return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
   414 
   415 
   416 JD_confs = 'JD_NS JD_FTA JD_Hoare JD_SN JD_Arrow JD_FFT JD_Jinja JD_QE JD_S2S'.split(' ')
   417 
   418 @scheduler()
   419 def judgement_day_scheduler(env):
   420     """Scheduler for Judgement Day."""
   421     return schedule.age_scheduler(env, 'Isabelle', JD_confs)
   422 
   423 
   424 # SML/NJ
   425 
   426 smlnj_settings = '''
   427 ML_SYSTEM=smlnj
   428 ML_HOME="/home/smlnj/110.72/bin"
   429 ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=256"
   430 ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
   431 '''
   432 
   433 @configuration(repos = [Isabelle], deps = [])
   434 def SML_HOL(*args):
   435     """HOL image built with SML/NJ"""
   436     return isabelle_make('src/HOL', *args, more_settings=smlnj_settings, target='HOL', keep_results=True)
   437 
   438 @configuration(repos = [Isabelle], deps = [])
   439 def SML_makeall(*args):
   440     """Makeall built with SML/NJ"""
   441     return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3'))