# HG changeset patch # User wenzelm # Date 1249724422 -7200 # Node ID e88b295aae351f732d56b51105b347d7dfc0d8d5 # Parent 41fe1c93f218ba71b250b93fe6eb8c5dfcb6afce refined mac-poly64 tests; diff -r 41fe1c93f218 -r e88b295aae35 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Fri Aug 07 19:16:04 2009 +0200 +++ b/Admin/isatest/isatest-makedist Sat Aug 08 11:40:22 2009 +0200 @@ -106,7 +106,7 @@ sleep 15 $SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly" sleep 15 -$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8; $MAKEALL $HOME/settings/mac-poly64-M4" +$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8; $MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8" sleep 15 $SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly" sleep 15 diff -r 41fe1c93f218 -r e88b295aae35 Admin/isatest/settings/mac-poly64-M4 --- a/Admin/isatest/settings/mac-poly64-M4 Fri Aug 07 19:16:04 2009 +0200 +++ b/Admin/isatest/settings/mac-poly64-M4 Sat Aug 08 11:40:22 2009 +0200 @@ -4,7 +4,7 @@ ML_SYSTEM="polyml-experimental" ML_PLATFORM="x86_64-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="--mutable 2000 --immutable 2000" + ML_OPTIONS="--mutable 5000 --immutable 2000" ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4 @@ -23,6 +23,6 @@ ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" -ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4" +ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4 -q 2 -t true" -HOL_USEDIR_OPTIONS="-p 2 -q 1" +HOL_USEDIR_OPTIONS="-p 2 -q 2" diff -r 41fe1c93f218 -r e88b295aae35 Admin/isatest/settings/mac-poly64-M8 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/settings/mac-poly64-M8 Sat Aug 08 11:40:22 2009 +0200 @@ -0,0 +1,28 @@ +# -*- shell-script -*- :mode=shellscript: + + POLYML_HOME="/home/polyml/polyml-svn" + ML_SYSTEM="polyml-experimental" + ML_PLATFORM="x86_64-darwin" + ML_HOME="$POLYML_HOME/$ML_PLATFORM" + ML_OPTIONS="--mutable 5000 --immutable 2000" + + +ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8 + +# 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 -q 2 -t true" + +HOL_USEDIR_OPTIONS="-p 2 -q 2"