more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
authorwenzelm
Wed, 28 Dec 2011 13:08:18 +0100
changeset 46004 484ef66bc3a1
parent 46003 c0fe5e8e4864
child 46005 ae721b158a79
more selective target "full" -- avoid failure of HOL-Datatype_Benchmark on 32bit platforms;
Admin/isatest/isatest-makeall
Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makeall	Wed Dec 28 13:00:51 2011 +0100
+++ b/Admin/isatest/isatest-makeall	Wed Dec 28 13:08:18 2011 +0100
@@ -71,7 +71,6 @@
   
     macbroy2)
         MFLAGS="-k"
-        TARGETS=full
         NICE=""
         ;;
 
@@ -102,7 +101,6 @@
 
     macbroy30)
         MFLAGS="-k"
-        TARGETS=full
         NICE=""
         ;;
 
@@ -124,8 +122,13 @@
   TARGETS="$2"
   shift 2
   ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
-  DIR="$ISABELLE_HOME/src/$LOGIC"
-  TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
+  if [ "$LOGIC" = "." ]; then
+    DIR="."
+    TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
+  else
+    DIR="$ISABELLE_HOME/src/$LOGIC"
+    TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
+  fi
 else
   DIR="."
   TOOL="$ISABELLE_TOOL makeall $MFLAGS $TARGETS"
--- a/Admin/isatest/isatest-makedist	Wed Dec 28 13:00:51 2011 +0100
+++ b/Admin/isatest/isatest-makedist	Wed Dec 28 13:08:18 2011 +0100
@@ -107,7 +107,11 @@
 sleep 15
 $SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
 sleep 15
-$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8; $MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8"
+$SSH macbroy2 "
+  $MAKEALL $HOME/settings/mac-poly64-M4 -l . full;
+  $MAKEALL $HOME/settings/mac-poly64-M8 -l . full;
+  $MAKEALL $HOME/settings/mac-poly-M4;
+  $MAKEALL $HOME/settings/mac-poly-M8"
 sleep 15
 $SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
 sleep 15