more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML;
authorwenzelm
Wed, 21 Nov 2012 15:50:54 +0100
changeset 50149 aaf276a28551
parent 50147 8d2251b9a200
child 50150 2e0287c6bb61
more generous timeout for SML/NJ, which is approx. 40-80 times slower than Poly/ML; more generous timeout for HOL-Quickcheck_Examples, which is rather slow in checking its examples (and mostly sequential);
Admin/isatest/isatest-makeall
src/HOL/ROOT
--- a/Admin/isatest/isatest-makeall	Wed Nov 21 14:07:35 2012 +0100
+++ b/Admin/isatest/isatest-makeall	Wed Nov 21 15:50:54 2012 +0100
@@ -47,7 +47,7 @@
 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
 
 # build args and nice setup for different target platforms
-BUILD_ARGS="-v -o timeout=3600"
+BUILD_ARGS="-v"
 NICE="nice"
 case $HOSTNAME in
     macbroy2 | macbroy6 | macbroy30)
@@ -85,6 +85,15 @@
 
     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
 
+    case "$SETTINGS" in
+      *sml*)
+        BUILD_ARGS="-o timeout=36000 $BUILD_ARGS"
+        ;;
+      *)
+        BUILD_ARGS="-o timeout=3600 $BUILD_ARGS"
+        ;;
+    esac
+
     # logfile setup
 
     DATE=$(date "+%Y-%m-%d")
--- a/src/HOL/ROOT	Wed Nov 21 14:07:35 2012 +0100
+++ b/src/HOL/ROOT	Wed Nov 21 15:50:54 2012 +0100
@@ -793,7 +793,7 @@
   theories MutabelleExtra
 
 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
-  options [timeout = 3600, document = false]
+  options [timeout = 5400, document = false]
   theories
     Quickcheck_Examples
   (* FIXME