reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
authorkrauss
Sun, 22 May 2011 22:22:25 +0200
changeset 43789e6990acab6ff
parent 43788 fcb6250bf6b4
child 43790 618adb3584e5
reverted 7fdd8d4908dc -- keeping images from Isabelle_makeall would be too expensive
Admin/mira.py
     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)