# HG changeset patch # User wenzelm # Date 1416650741 -3600 # Node ID 8281f83d286f12bb960c5f9d8882949534375553 # Parent 3cded6b57a823d6df76b43bc60321451a94de5b9 isatest for Mac OS X Yosemite; diff -r 3cded6b57a82 -r 8281f83d286f Admin/PLATFORMS --- a/Admin/PLATFORMS Mon Dec 08 23:06:19 2014 +0100 +++ b/Admin/PLATFORMS Sat Nov 22 11:05:41 2014 +0100 @@ -33,9 +33,10 @@ x86-linux Ubuntu 10.04 LTS x86_64-linux Ubuntu 10.04 LTS - x86_64-darwin Mac OS X Lion (macbroy6) - Mac OS X Mountain Lion (macbroy30) - Mac OS X Mavericks (macbroy2) + x86_64-darwin Mac OS X 10.7 Lion (macbroy6) + Mac OS X 10.8 Mountain Lion (macbroy30) + Mac OS X 10.9 Mavericks (macbroy2) + Mac OS X 10.10 Yosemite (macbroy31) x86-cygwin Cygwin 1.7 (vmbroy9) diff -r 3cded6b57a82 -r 8281f83d286f Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Mon Dec 08 23:06:19 2014 +0100 +++ b/Admin/isatest/isatest-makedist Sat Nov 22 11:05:41 2014 +0100 @@ -120,6 +120,8 @@ $SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2" sleep 15 $SSH macbroy30 "$MAKEALL $HOME/settings/mac-poly-M2" +sleep 15 +$SSH macbroy31 "$MAKEALL $HOME/settings/mac-poly-M2-alternative" echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1 diff -r 3cded6b57a82 -r 8281f83d286f Admin/isatest/settings/mac-poly-M2-alternative --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/settings/mac-poly-M2-alternative Sat Nov 22 11:05:41 2014 +0100 @@ -0,0 +1,35 @@ +# -*- shell-script -*- :mode=shellscript: + +init_components /home/isabelle/contrib "$HOME/admin/components/main" +init_components /home/isabelle/contrib "$HOME/admin/components/optional" +init_components /home/isabelle/contrib "$HOME/admin/components/nonfree" + +ML_SYSTEM="polyml-5.5.2" +ML_PLATFORM="x86-darwin" +ML_HOME="/home/polyml/polyml-5.5.2/$ML_PLATFORM" +ML_OPTIONS="-H 1000" + +ISABELLE_HOME_USER=~/isabelle-mac-poly-M2-alternative + +# 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_BUILD_OPTIONS="browser_info=true document=pdf threads=2 parallel_proofs=2" + +ISABELLE_FULL_TEST=true + +ISABELLE_GHC=ghc + +Z3_NON_COMMERCIAL="yes" +