# HG changeset patch # User wenzelm # Date 1244830841 -7200 # Node ID 907616b9536c713dddb594acd15bafb072914fb1 # Parent 1c143f6a2226df0b37b5382e8feb99b6c58d012c more isatests; macbroy23: nice at-sml-dev-e; diff -r 1c143f6a2226 -r 907616b9536c Admin/isatest/isatest-makeall --- a/Admin/isatest/isatest-makeall Fri Jun 12 18:33:58 2009 +0200 +++ b/Admin/isatest/isatest-makeall Fri Jun 12 20:20:41 2009 +0200 @@ -71,14 +71,19 @@ NICE="nice" ;; + macbroy2) + MFLAGS="" + NICE="" + ;; + macbroy5) MFLAGS="-j 2" NICE="" ;; macbroy23) - MFLAGS="" - NICE="" + MFLAGS="-j 2" + NICE="nice" ;; macbroy2[0-9]) diff -r 1c143f6a2226 -r 907616b9536c Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Fri Jun 12 18:33:58 2009 +0200 +++ b/Admin/isatest/isatest-makedist Fri Jun 12 20:20:41 2009 +0200 @@ -109,9 +109,11 @@ sleep 15 $SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly" sleep 15 +$SSH macbroy2 "$MAKEALL $HOME/settings/at-mac-poly-5.1-para; $MAKEALL $HOME/settings/mac-poly-M8" +sleep 15 $SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly" sleep 15 -$SSH macbroy6 "/usr/stud/isatest/bin/isatest-makeall $HOME/settings/at-mac-poly-5.1-para" +$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly-M4" sleep 15 $SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly" diff -r 1c143f6a2226 -r 907616b9536c Admin/isatest/settings/mac-poly-M4 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/settings/mac-poly-M4 Fri Jun 12 20:20:41 2009 +0200 @@ -0,0 +1,28 @@ +# -*- shell-script -*- :mode=shellscript: + + POLYML_HOME="/home/polyml/polyml-svn" + ML_SYSTEM="polyml-experimental" + ML_PLATFORM="x86-darwin" + ML_HOME="$POLYML_HOME/$ML_PLATFORM" + ML_OPTIONS="--mutable 800 --immutable 2000" + + +ISABELLE_HOME_USER=~/isabelle-mac-poly-M4-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. +ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" +ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" + +ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4" + +HOL_USEDIR_OPTIONS="-p 2 -Q false" diff -r 1c143f6a2226 -r 907616b9536c Admin/isatest/settings/mac-poly-M8 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/settings/mac-poly-M8 Fri Jun 12 20:20:41 2009 +0200 @@ -0,0 +1,28 @@ +# -*- shell-script -*- :mode=shellscript: + + POLYML_HOME="/home/polyml/polyml-svn" + ML_SYSTEM="polyml-experimental" + ML_PLATFORM="x86-darwin" + ML_HOME="$POLYML_HOME/$ML_PLATFORM" + ML_OPTIONS="--mutable 800 --immutable 2000" + + +ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-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. +ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" +ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" + +ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8" + +HOL_USEDIR_OPTIONS="-p 2 -Q false"