--- a/Admin/CHECKLIST Fri May 28 11:23:34 2010 +0200
+++ b/Admin/CHECKLIST Fri May 28 11:37:38 2010 +0200
@@ -3,8 +3,6 @@
- test polyml-5.3.0, polyml-5.2.1, polyml-5.2, polyml-5.1, polyml-5.0;
-- test sparc-solaris, x86-solaris;
-
- test Proof General;
- test Scala wrapper;
--- a/Admin/isatest/isatest-makeall Fri May 28 11:23:34 2010 +0200
+++ b/Admin/isatest/isatest-makeall Fri May 28 11:37:38 2010 +0200
@@ -67,16 +67,6 @@
MFLAGS="-k -j 2"
;;
- sunbroy2)
- MFLAGS="-k -j 2"
- NICE="nice"
- ;;
-
- sunbroy1)
- MFLAGS="-k -j 2"
- NICE="nice"
- ;;
-
macbroy2)
MFLAGS="-k"
NICE=""
--- a/Admin/isatest/isatest-makedist Fri May 28 11:23:34 2010 +0200
+++ b/Admin/isatest/isatest-makedist Fri May 28 11:37:38 2010 +0200
@@ -113,8 +113,6 @@
$SSH atbroy102 "$MAKEALL $HOME/settings/cygwin-poly-e"
#sleep 15
#$SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly"
-#sleep 15
-#$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
--- a/Admin/isatest/isatest-statistics Fri May 28 11:23:34 2010 +0200
+++ b/Admin/isatest/isatest-statistics Fri May 28 11:37:38 2010 +0200
@@ -51,7 +51,7 @@
SESSIONS="$@"
case "$PLATFORM" in
- *para* | *-M* | sun-poly)
+ *para* | *-M*)
PARALLEL=true
;;
*)
--- a/Admin/isatest/isatest-stats Fri May 28 11:23:34 2010 +0200
+++ b/Admin/isatest/isatest-stats Fri May 28 11:37:38 2010 +0200
@@ -6,7 +6,7 @@
THIS=$(cd "$(dirname "$0")"; pwd -P)
-PLATFORMS="at-poly at-poly-test at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly"
+PLATFORMS="at-poly at-poly-test at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev"
ISABELLE_SESSIONS="\
HOL-Plain \
--- a/Admin/isatest/settings/sun-poly Fri May 28 11:23:34 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
- POLYML_HOME="/home/polyml/polyml-5.3.0"
- ML_SYSTEM="polyml-5.3.0"
- ML_PLATFORM="sparc-solaris"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="-H 1000"
-
-ISABELLE_HOME_USER=/tmp/isabelle-sun-poly
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-#ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true -M 6 -q 2"
-
-unset KODKODI
-
--- a/Admin/isatest/settings/sun-sml Fri May 28 11:23:34 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-# Standard ML of New Jersey 110.0.7 (stable version)
-ML_SYSTEM=smlnj-110.0.7
-ML_HOME="/home/proj/smlnj/110.0.7/bin"
-ML_OPTIONS="@SMLdebug=/dev/null"
-ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-
-ISABELLE_HOME_USER=~/isabelle-sun-sml
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-# ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-
-unset KODKODI
-
--- a/Admin/isatest/settings/sun-sml-dev Fri May 28 11:23:34 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-# Standard ML of New Jersey 110 or later
-ML_SYSTEM=smlnj-110
-ML_HOME="/home/smlnj/110.60/bin"
-ML_OPTIONS="@SMLdebug=/dev/null"
-ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
-
-ISABELLE_HOME_USER=~/isabelle-sun-sml-dev
-
-# Where to look for isabelle tools (multiple dirs separated by ':').
-ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
-
-# Location for temporary files (should be on a local file system).
-ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
-
-
-# Heap input locations. ML system identifier is included in lookup.
-ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
-
-# Heap output location. ML system identifier is appended automatically later on.
-ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
-ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
-
-# ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
-
-unset KODKODI
-