reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
1.1 --- a/Admin/mira.py Sun May 22 20:59:13 2011 +0200
1.2 +++ b/Admin/mira.py Sun May 22 22:22:25 2011 +0200
1.3 @@ -289,37 +289,37 @@
1.4 {'mutabelle_results': {theory: mutabelle_data}},
1.5 {'log': log, 'mutabelle_log': mutabelle_log}, None)
1.6
1.7 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.8 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.9 def Mutabelle_Relation(*args):
1.10 """Mutabelle regression suite on Relation theory"""
1.11 return invoke_mutabelle('Relation', *args)
1.12
1.13 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.14 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.15 def Mutabelle_List(*args):
1.16 """Mutabelle regression suite on List theory"""
1.17 return invoke_mutabelle('List', *args)
1.18
1.19 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.20 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.21 def Mutabelle_Set(*args):
1.22 """Mutabelle regression suite on Set theory"""
1.23 return invoke_mutabelle('Set', *args)
1.24
1.25 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.26 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.27 def Mutabelle_Map(*args):
1.28 """Mutabelle regression suite on Map theory"""
1.29 return invoke_mutabelle('Map', *args)
1.30
1.31 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.32 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.33 def Mutabelle_Divides(*args):
1.34 """Mutabelle regression suite on Divides theory"""
1.35 return invoke_mutabelle('Divides', *args)
1.36
1.37 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.38 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.39 def Mutabelle_MacLaurin(*args):
1.40 """Mutabelle regression suite on MacLaurin theory"""
1.41 return invoke_mutabelle('MacLaurin', *args)
1.42
1.43 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.44 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.45 def Mutabelle_Fun(*args):
1.46 """Mutabelle regression suite on Fun theory"""
1.47 return invoke_mutabelle('Fun', *args)
1.48 @@ -376,22 +376,22 @@
1.49 return (some_success, '', data, raw_attachments, None)
1.50
1.51
1.52 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.53 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.54 def JD_NS(*args):
1.55 """Judgement Day regression suite NS"""
1.56 return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
1.57
1.58 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.59 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.60 def JD_FTA(*args):
1.61 """Judgement Day regression suite FTA"""
1.62 return judgement_day('Isabelle/src/HOL/Library', 'Fundamental_Theorem_Algebra', 'prover_timeout=10', *args)
1.63
1.64 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.65 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.66 def JD_Hoare(*args):
1.67 """Judgement Day regression suite Hoare"""
1.68 return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args)
1.69
1.70 -@configuration(repos = [Isabelle], deps = [(Isabelle_makeall, [0])])
1.71 +@configuration(repos = [Isabelle], deps = [(HOL, [0])])
1.72 def JD_SN(*args):
1.73 """Judgement Day regression suite SN"""
1.74 return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)