moved some configurations to AFP, and fixed others
authorkrauss
Mon, 21 Mar 2011 21:10:29 +0100
changeset 42058 1eda69f0b9a8
parent 42041 f90040058a24
child 42059 83f3dc509068
moved some configurations to AFP, and fixed others
Admin/mira.py
--- a/Admin/mira.py	Mon Mar 21 17:14:52 2011 +0100
+++ b/Admin/mira.py	Mon Mar 21 21:10:29 2011 +0100
@@ -294,21 +294,11 @@
     return (some_success, '', data, raw_attachments, None)
 
 
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_Arrow(*args):
-    """Judgement Day regression suite Arrow"""
-    return judgement_day('Afp/thys/ArrowImpossibilityGS/Thys', 'Arrow_Order', 'prover_timeout=10', *args)
-
 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
 def JD_NS(*args):
     """Judgement Day regression suite NS"""
     return judgement_day('Isabelle/src/HOL/Auth', 'NS_Shared', 'prover_timeout=10', *args)
 
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_FFT(*args):
-    """Judgement Day regression suite FFT"""
-    return judgement_day('Afp/thys/FFT', 'FFT', 'prover_timeout=10', *args)
-
 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
 def JD_FTA(*args):
     """Judgement Day regression suite FTA"""
@@ -317,25 +307,10 @@
 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
 def JD_Hoare(*args):
     """Judgement Day regression suite Hoare"""
-    return judgement_day('Isabelle/src/HOL/IMP', 'Hoare', 'prover_timeout=10', *args)
-
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_Jinja(*args):
-    """Judgement Day regression suite Jinja"""
-    return judgement_day('Afp/thys/Jinja/J', 'TypeSafe', 'prover_timeout=10', *args)
+    return judgement_day('Isabelle/src/HOL/IMPP', 'Hoare', 'prover_timeout=10', *args)
 
 @configuration(repos = [Isabelle], deps = [(HOL, [0])])
 def JD_SN(*args):
     """Judgement Day regression suite SN"""
-    return judgement_day('Isabelle/src/HOL/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
+    return judgement_day('Isabelle/src/HOL/Proofs/Lambda', 'StrongNorm', 'prover_timeout=10', *args)
 
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_QE(*args):
-    """Judgement Day regression suite QE"""
-    return judgement_day('Afp/thys/LinearQuantifierElim/Thys', 'QEpres', 'prover_timeout=10', *args)
-
-@configuration(repos = [Isabelle, AFP], deps = [(HOL, [0])])
-def JD_S2S(*args):
-    """Judgement Day regression suite S2S"""
-    return judgement_day('Afp/thys/SumSquares', 'TwoSquares', 'prover_timeout=10', *args)
-