clarified timeout for isatest;
authorwenzelm
Mon Sep 22 21:45:59 2014 +0200 (2014-09-22)
changeset 58423e4d540c0dd57
parent 58422 b5d27faef560
child 58424 cbbba613b6ab
clarified timeout for isatest;
Admin/isatest/isatest-makeall
src/HOL/ROOT
     1.1 --- a/Admin/isatest/isatest-makeall	Mon Sep 22 21:31:45 2014 +0200
     1.2 +++ b/Admin/isatest/isatest-makeall	Mon Sep 22 21:45:59 2014 +0200
     1.3 @@ -87,10 +87,10 @@
     1.4  
     1.5      case "$SETTINGS" in
     1.6        *sml*)
     1.7 -        BUILD_ARGS="-o timeout=36000 $BUILD_ARGS"
     1.8 +        BUILD_ARGS="-o timeout=54000 $BUILD_ARGS"
     1.9          ;;
    1.10        *)
    1.11 -        BUILD_ARGS="-o timeout=3600 $BUILD_ARGS"
    1.12 +        BUILD_ARGS="-o timeout=5400 $BUILD_ARGS"
    1.13          ;;
    1.14      esac
    1.15  
     2.1 --- a/src/HOL/ROOT	Mon Sep 22 21:31:45 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Mon Sep 22 21:45:59 2014 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4    description {*
     2.5      HOL-Main with explicit proof terms.
     2.6    *}
     2.7 -  options [timeout = 5400, document = false]
     2.8 +  options [document = false]
     2.9    theories Proofs (*sequential change of global flag!*)
    2.10    theories "~~/src/HOL/Library/Old_Datatype"
    2.11    files
    2.12 @@ -260,7 +260,7 @@
    2.13  
    2.14      Testing Metis and Sledgehammer.
    2.15    *}
    2.16 -  options [timeout = 3600, document = false]
    2.17 +  options [document = false]
    2.18    theories
    2.19      Abstraction
    2.20      Big_O
    2.21 @@ -522,7 +522,7 @@
    2.22    description {*
    2.23      Miscellaneous examples for Higher-Order Logic.
    2.24    *}
    2.25 -  options [timeout = 3600, condition = ML_SYSTEM_POLYML]
    2.26 +  options [condition = ML_SYSTEM_POLYML]
    2.27    theories [document = false]
    2.28      "~~/src/HOL/Library/State_Monad"
    2.29      Code_Binary_Nat_examples
    2.30 @@ -722,7 +722,7 @@
    2.31    theories Nominal
    2.32  
    2.33  session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
    2.34 -  options [timeout = 3600, condition = ML_SYSTEM_POLYML, document = false]
    2.35 +  options [condition = ML_SYSTEM_POLYML, document = false]
    2.36    theories
    2.37      Nominal_Examples_Base
    2.38    theories [condition = ISABELLE_FULL_TEST]