# HG changeset patch # User isatest # Date 1187002438 -7200 # Node ID 9f49e5d12a32e54ee4411e0db21d7d518b60916f # Parent ae70f95e31de89cc336b1e6262baa7365107bc01 multi-threading with poly 5.1 test diff -r ae70f95e31de -r 9f49e5d12a32 Admin/isatest/settings/at-poly-5.1-para --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/settings/at-poly-5.1-para Mon Aug 13 12:53:58 2007 +0200 @@ -0,0 +1,33 @@ +# -*- shell-script -*- + + POLYML_HOME="/usr/proj/polyml/polyml-5.1-test" + ML_SYSTEM="polyml-5.1" + ML_PLATFORM="x86-linux" + ML_HOME="$POLYML_HOME/$ML_PLATFORM" + ML_OPTIONS="-H 500" + +ISABELLE_HOME_USER=~/isabelle-at-poly-5.1-para + +# 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 -M 99" + +HOL_USEDIR_OPTIONS="-p 2"