Admin/mira.py
changeset 42040 869df9b88deb
parent 41894 7c4a4b02dbdb
child 42058 1eda69f0b9a8
equal deleted inserted replaced
42038:626fcf4a803e 42040:869df9b88deb
   245 
   245 
   246 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   246 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
   247 def Mutabelle_Fun(*args):
   247 def Mutabelle_Fun(*args):
   248     """Mutabelle regression suite on Fun theory"""
   248     """Mutabelle regression suite on Fun theory"""
   249     return invoke_mutabelle('Fun', *args)
   249     return invoke_mutabelle('Fun', *args)
       
   250 
       
   251 
       
   252 # Judgement Day configurations
       
   253 
       
   254 judgement_day_provers = ('e', 'spass', 'vampire')
       
   255 
       
   256 def judgement_day(base_path, theory, opts, env, case, paths, dep_paths, playground):
       
   257     """Judgement Day regression suite"""
       
   258 
       
   259     isa = paths[0]
       
   260     dep_path = dep_paths[0]
       
   261 
       
   262     os.chdir(path.join(playground, '..', base_path)) # Mirabelle requires specific cwd
       
   263     prepare_isabelle_repository(isa, env.settings.contrib, dep_path)
       
   264 
       
   265     output = {}
       
   266     success_rates = {}
       
   267     some_success = False
       
   268 
       
   269     for atp in judgement_day_provers:
       
   270 
       
   271         log_dir = path.join(playground, 'mirabelle_log_' + atp)
       
   272         os.makedirs(log_dir)
       
   273 
       
   274         cmd = ('%s/bin/isabelle mirabelle -q -O %s sledgehammer[prover=%s,%s] %s.thy'
       
   275                % (isa, log_dir, atp, opts, theory))
       
   276 
       
   277         os.system(cmd)
       
   278         output[atp] = util.readfile(path.join(log_dir, theory + '.log'))
       
   279 
       
   280         percentages = list(re.findall(r'Success rate: (\d+)%', output[atp]))
       
   281         if len(percentages) == 2:
       
   282             success_rates[atp] = {
       
   283                 'sledgehammer': int(percentages[0]),
       
   284                 'metis': int(percentages[1])}
       
   285             if success_rates[atp]['sledgehammer'] > 0:
       
   286                 some_success = True
       
   287         else:
       
   288             success_rates[atp] = {}
       
   289 
       
   290 
       
   291     data = {'success_rates': success_rates}
       
   292     raw_attachments = dict((atp + "_output", output[atp]) for atp in judgement_day_provers)
       
   293     # FIXME: summary?
       
   294     return (some_success, '', data, raw_attachments, None)
       
   295 
       
   296 
       
   297 @configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
       
   298 def JD_Arrow(*args):
       
   299     """Judgement Day regression suite Arrow"""
       
   300     return judgement_day('Afp/thys/ArrowImpossibilityGS/Thys', 'Arrow_Order', 'prover_timeout=10', *args)
       
   301 
       
   302 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
       
   303 def JD_NS(*args):
       
   304     """Judgement Day regression suite NS"""
       
   305     return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
       
   306 
       
   307 @configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
       
   308 def JD_FFT(*args):
       
   309     """Judgement Day regression suite FFT"""
       
   310     return judgement_day('Afp/thys/FFT', 'FFT', 'prover_timeout=10', *args)
       
   311 
       
   312 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
       
   313 def JD_FTA(*args):
       
   314     """Judgement Day regression suite FTA"""
       
   315     return judgement_day('Isabelle/src/HOL/Library', 'Fundamental_Theorem_Algebra', 'prover_timeout=10', *args)
       
   316 
       
   317 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
       
   318 def JD_Hoare(*args):
       
   319     """Judgement Day regression suite Hoare"""
       
   320     return judgement_day('Isabelle/src/HOL/IMP', 'Hoare', 'prover_timeout=10', *args)
       
   321 
       
   322 @configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
       
   323 def JD_Jinja(*args):
       
   324     """Judgement Day regression suite Jinja"""
       
   325     return judgement_day('Afp/thys/Jinja/J', 'TypeSafe', 'prover_timeout=10', *args)
       
   326 
       
   327 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
       
   328 def JD_SN(*args):
       
   329     """Judgement Day regression suite SN"""
       
   330     return judgement_day('Isabelle/src/HOL/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
       
   331 
       
   332 @configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
       
   333 def JD_QE(*args):
       
   334     """Judgement Day regression suite QE"""
       
   335     return judgement_day('Afp/thys/LinearQuantifierElim/Thys', 'QEpres', 'prover_timeout=10', *args)
       
   336 
       
   337 @configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
       
   338 def JD_S2S(*args):
       
   339     """Judgement Day regression suite S2S"""
       
   340     return judgement_day('Afp/thys/SumSquares', 'TwoSquares', 'prover_timeout=10', *args)
       
   341