# HG changeset patch
# User wenzelm
# Date 1456685658 -3600
# Node ID 2026ef279d1ecd4d0f7b6562f4f0af49e8e35a7f
# Parent  38c89353b3491a0ded70a534fee424c239c7ccd1
simplified / unified isatest settings;

diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/isatest-makedist
--- a/Admin/isatest/isatest-makedist	Sun Feb 28 17:40:01 2016 +0100
+++ b/Admin/isatest/isatest-makedist	Sun Feb 28 19:54:18 2016 +0100
@@ -102,10 +102,7 @@
 
 $SSH lxbroy10 "$MAKEALL -x HOL-Proofs $HOME/settings/at64-poly"
 sleep 15
-$SSH lxbroy4 "
-  $MAKEALL -l HOL-Library $HOME/settings/at-poly;
-  $MAKEALL -l HOL-Library $HOME/settings/at-poly-e;
-  $MAKEALL $HOME/settings/at-poly-test"
+$SSH lxbroy4 "$MAKEALL -l HOL-Library $HOME/settings/at-poly"
 sleep 15
 $SSH macbroy2 "
   $MAKEALL $HOME/settings/mac-poly64-M4;
@@ -115,11 +112,9 @@
   $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs;
   $MAKEALL $HOME/settings/mac-poly-M8-quick_and_dirty"
 sleep 15
-$SSH macbroy30 "
-  $MAKEALL $HOME/settings/mac-poly-M2;
-  $MAKEALL $HOME/settings/mac-poly64-M2"
+$SSH macbroy30 "$MAKEALL $HOME/settings/mac-poly-M2"
 sleep 15
-$SSH macbroy31 "$MAKEALL $HOME/settings/mac-poly-M2-alternative"
+$SSH macbroy31 "$MAKEALL $MAKEALL $HOME/settings/mac-poly64-M2"
 
 echo ------------------- spawned tests successfully --- `date` --- $HOSTNAME >> $DISTLOG 2>&1
 
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/at-poly-e
--- a/Admin/isatest/settings/at-poly-e	Sun Feb 28 17:40:01 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-
-  POLYML_HOME="/home/polyml/polyml-5.4.1"
-  ML_SYSTEM="polyml-5.4.1"
-  ML_PLATFORM="x86-linux"
-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 1000"
-
-ISABELLE_GHC=/usr/bin/ghc
-
-ISABELLE_HOME_USER=~/isabelle-at-poly-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_BUILD_OPTIONS="browser_info=true document=pdf"
-
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/at-poly-test
--- a/Admin/isatest/settings/at-poly-test	Sun Feb 28 17:40:01 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-init_components /home/isabelle/contrib "$HOME/admin/components/main"
-
-  POLYML_HOME="/home/polyml/polyml-svn"
-  ML_SYSTEM="polyml-5.5.2"
-  ML_PLATFORM="x86-linux"
-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 500 --gcthreads 4"
-
-ISABELLE_GHC=/usr/bin/ghc
-
-ISABELLE_HOME_USER=~/isabelle-at-poly-test
-
-# 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=4 parallel_proofs=2"
-
-ISABELLE_GHC="/usr/bin/ghc"
-ISABELLE_OCAML="/usr/bin/ocaml"
-ISABELLE_SWIPL="/usr/bin/swipl"
-
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/mac-poly-M2
--- a/Admin/isatest/settings/mac-poly-M2	Sun Feb 28 17:40:01 2016 +0100
+++ b/Admin/isatest/settings/mac-poly-M2	Sun Feb 28 19:54:18 2016 +0100
@@ -4,10 +4,9 @@
 init_components /home/isabelle/contrib "$HOME/admin/components/optional"
 init_components /home/isabelle/contrib "$HOME/admin/components/nonfree"
 
-ML_SYSTEM="polyml-5.5.0"
-ML_PLATFORM="x86-darwin"
-ML_HOME="/home/polyml/polyml-5.5.0/$ML_PLATFORM"
-ML_OPTIONS="-H 500"
+ML_PLATFORM="$ISABELLE_PLATFORM32"
+ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ML_OPTIONS="-H 1000 --gcthreads 4"
 
 ISABELLE_GHC=ghc
 
@@ -28,4 +27,3 @@
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
 ISABELLE_BUILD_OPTIONS="browser_info=true document=pdf threads=2 parallel_proofs=2"
-
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/mac-poly-M2-alternative
--- a/Admin/isatest/settings/mac-poly-M2-alternative	Sun Feb 28 17:40:01 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-# -*- 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_PLATFORM="$ISABELLE_PLATFORM32"
-ML_HOME="$POLYML_HOME/$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_GHC=ghc
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/mac-poly-M4
--- a/Admin/isatest/settings/mac-poly-M4	Sun Feb 28 17:40:01 2016 +0100
+++ b/Admin/isatest/settings/mac-poly-M4	Sun Feb 28 19:54:18 2016 +0100
@@ -1,10 +1,12 @@
 # -*- 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_PLATFORM="$ISABELLE_PLATFORM32"
 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 500 --gcthreads 4"
+ML_OPTIONS="-H 1000 --gcthreads 4"
 
 ISABELLE_HOME_USER=~/isabelle-mac-poly-M4
 
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/mac-poly-M8
--- a/Admin/isatest/settings/mac-poly-M8	Sun Feb 28 17:40:01 2016 +0100
+++ b/Admin/isatest/settings/mac-poly-M8	Sun Feb 28 19:54:18 2016 +0100
@@ -1,10 +1,12 @@
 # -*- 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_PLATFORM="$ISABELLE_PLATFORM32"
 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="-H 500 --gcthreads 8"
+ML_OPTIONS="-H 1000 --gcthreads 8"
 
 ISABELLE_HOME_USER=~/isabelle-mac-poly-M8
 
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/mac-poly-M8-quick_and_dirty
--- a/Admin/isatest/settings/mac-poly-M8-quick_and_dirty	Sun Feb 28 17:40:01 2016 +0100
+++ b/Admin/isatest/settings/mac-poly-M8-quick_and_dirty	Sun Feb 28 19:54:18 2016 +0100
@@ -1,14 +1,12 @@
 # -*- 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"
 
-  POLYML_HOME="/home/polyml/polyml-5.5.1"
-  ML_SYSTEM="polyml-5.5.1"
-  ML_PLATFORM="x86-darwin"
-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 1000"
-
-ISABELLE_GHC=ghc
+ML_PLATFORM="$ISABELLE_PLATFORM32"
+ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ML_OPTIONS="-H 1000 --gcthreads 8"
 
 ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-quick_and_dirty
 
@@ -27,3 +25,11 @@
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
 ISABELLE_BUILD_OPTIONS="threads=8 quick_and_dirty"
+
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/mac-poly-M8-skip_proofs
--- a/Admin/isatest/settings/mac-poly-M8-skip_proofs	Sun Feb 28 17:40:01 2016 +0100
+++ b/Admin/isatest/settings/mac-poly-M8-skip_proofs	Sun Feb 28 19:54:18 2016 +0100
@@ -1,14 +1,12 @@
 # -*- 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"
 
-  POLYML_HOME="/home/polyml/polyml-5.5.0"
-  ML_SYSTEM="polyml-5.5.0"
-  ML_PLATFORM="x86-darwin"
-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 1000 --gcthreads 8"
-
-ISABELLE_GHC=ghc
+ML_PLATFORM="$ISABELLE_PLATFORM32"
+ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ML_OPTIONS="-H 1000 --gcthreads 8"
 
 ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-skip_proofs
 
@@ -27,3 +25,11 @@
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
 ISABELLE_BUILD_OPTIONS="threads=8 skip_proofs"
+
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/mac-poly64-M2
--- a/Admin/isatest/settings/mac-poly64-M2	Sun Feb 28 17:40:01 2016 +0100
+++ b/Admin/isatest/settings/mac-poly64-M2	Sun Feb 28 19:54:18 2016 +0100
@@ -1,12 +1,12 @@
 # -*- 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"
 
-  POLYML_HOME="/home/polyml/polyml-5.5.0"
-  ML_SYSTEM="polyml-5.5.0"
-  ML_PLATFORM="x86_64-darwin"
-  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 1000"
+ML_PLATFORM="$ISABELLE_PLATFORM64"
+ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ML_OPTIONS="-H 2000 --gcthreads 2"
 
 ISABELLE_GHC=ghc
 
@@ -27,4 +27,3 @@
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
 ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=2 parallel_proofs=2"
-
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/mac-poly64-M4
--- a/Admin/isatest/settings/mac-poly64-M4	Sun Feb 28 17:40:01 2016 +0100
+++ b/Admin/isatest/settings/mac-poly64-M4	Sun Feb 28 19:54:18 2016 +0100
@@ -1,13 +1,13 @@
 # -*- 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_PLATFORM="$ISABELLE_PLATFORM64"
 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
 ML_OPTIONS="-H 2000 --gcthreads 4"
 
-ISABELLE_GHC=ghc
-
 ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
@@ -26,3 +26,10 @@
 
 ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=4 parallel_proofs=2"
 
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"
diff -r 38c89353b349 -r 2026ef279d1e Admin/isatest/settings/mac-poly64-M8
--- a/Admin/isatest/settings/mac-poly64-M8	Sun Feb 28 17:40:01 2016 +0100
+++ b/Admin/isatest/settings/mac-poly64-M8	Sun Feb 28 19:54:18 2016 +0100
@@ -1,13 +1,13 @@
 # -*- 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_PLATFORM="$ISABELLE_PLATFORM64"
 ML_HOME="$POLYML_HOME/$ML_PLATFORM"
 ML_OPTIONS="-H 2000 --gcthreads 8"
 
-ISABELLE_GHC=ghc
-
 ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
 
 # Where to look for isabelle tools (multiple dirs separated by ':').
@@ -26,3 +26,10 @@
 
 ISABELLE_BUILD_OPTIONS="browser_info=false document=false threads=8 parallel_proofs=2"
 
+ISABELLE_GHC=ghc
+ISABELLE_MLTON=mlton
+ISABELLE_OCAML=ocaml
+ISABELLE_OCAMLC=ocamlc
+ISABELLE_POLYML="$ML_HOME/poly"
+#ISABELLE_SCALA="$SCALA_HOME/bin"
+ISABELLE_SMLNJ="/mnt/nfsbroy/home/smlnj/bin/sml"