# HG changeset patch # User isatest # Date 1200349168 -3600 # Node ID a1a3f614dd8673701058a3a6c5889e51f471117d # Parent cc3f0094998629cc48e34b5fafeb860b72fd4ec9 make at-sml-dev experimental diff -r cc3f00949986 -r a1a3f614dd86 Admin/isatest/isatest-check --- a/Admin/isatest/isatest-check Mon Jan 14 21:42:58 2008 +0100 +++ b/Admin/isatest/isatest-check Mon Jan 14 23:19:28 2008 +0100 @@ -48,7 +48,7 @@ # check if tests are still running, wait for them a couple of hours i=0 -while [ -n "$(ls $RUNNING)" -a $i -lt 8 ]; do +while [ -n "$(ls $RUNNING)" -a $i -lt 10 ]; do sleep 3600 let "i = i+1" done diff -r cc3f00949986 -r a1a3f614dd86 Admin/isatest/isatest-makeall --- a/Admin/isatest/isatest-makeall Mon Jan 14 21:42:58 2008 +0100 +++ b/Admin/isatest/isatest-makeall Mon Jan 14 23:19:28 2008 +0100 @@ -55,8 +55,8 @@ ;; atbroy98) - MFLAGS="-j 2" - NICE="nice -n 1" + MFLAGS="" + NICE="" ;; atbroy31) diff -r cc3f00949986 -r a1a3f614dd86 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Mon Jan 14 21:42:58 2008 +0100 +++ b/Admin/isatest/isatest-makedist Mon Jan 14 23:19:28 2008 +0100 @@ -105,7 +105,7 @@ sleep 5 $SSH atbroy99 "$MAKEALL $HOME/settings/at64-poly-5.1-para" sleep 5 -$SSH atbroy98 "$MAKEALL $HOME/settings/at-sml-dev" +$SSH atbroy98 "$MAKEALL $HOME/settings/at-sml-dev-e" sleep 5 $SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly" sleep 5 diff -r cc3f00949986 -r a1a3f614dd86 Admin/isatest/settings/at-sml-dev --- a/Admin/isatest/settings/at-sml-dev Mon Jan 14 21:42:58 2008 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ -# -*- shell-script -*- - -# Standard ML of New Jersey 110 or later -ML_SYSTEM=smlnj -ML_HOME="/usr/proj/smlnj/110.67/bin" -ML_OPTIONS="@SMLdebug=/dev/null" -ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") - -ISABELLE_HOME_USER="$HOME/isabelle-at-sml-dev" # /tmp/isatest/isabelle-at-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. -if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then - #Isabelle build tells us to store heaps etc. within the distribution. - ISABELLE_OUTPUT="$ISABELLE_HOME/heaps" - ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info" -else - ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" - ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" -fi - -ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" - -HOL_USEDIR_OPTIONS="-p 0" diff -r cc3f00949986 -r a1a3f614dd86 Admin/isatest/settings/at-sml-dev-e --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/settings/at-sml-dev-e Mon Jan 14 23:19:28 2008 +0100 @@ -0,0 +1,33 @@ +# -*- shell-script -*- + +# Standard ML of New Jersey 110 or later +ML_SYSTEM=smlnj +ML_HOME="/usr/proj/smlnj/110.67/bin" +ML_OPTIONS="@SMLdebug=/dev/null" +ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") + +ISABELLE_HOME_USER="$HOME/isabelle-at-sml-dev-e" + +# 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. +if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then + #Isabelle build tells us to store heaps etc. within the distribution. + ISABELLE_OUTPUT="$ISABELLE_HOME/heaps" + ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info" +else + ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" + ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" +fi + +ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true" + +HOL_USEDIR_OPTIONS="-p 0"