Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simplified / unified isatest settings;
authorwenzelm
Sun, 28 Feb 2016 19:54:18 +0100
changeset 62455 2026ef279d1e
parent 62454 38c89353b349
child 62456 11e06f5283bc
simplified / unified isatest settings;
Admin/isatest/isatest-makedist file | annotate | diff | comparison | revisions
Admin/isatest/settings/at-poly-e file | annotate | diff | comparison | revisions
Admin/isatest/settings/at-poly-test file | annotate | diff | comparison | revisions
Admin/isatest/settings/mac-poly-M2 file | annotate | diff | comparison | revisions
Admin/isatest/settings/mac-poly-M2-alternative file | annotate | diff | comparison | revisions
Admin/isatest/settings/mac-poly-M4 file | annotate | diff | comparison | revisions
Admin/isatest/settings/mac-poly-M8 file | annotate | diff | comparison | revisions
Admin/isatest/settings/mac-poly-M8-quick_and_dirty file | annotate | diff | comparison | revisions
Admin/isatest/settings/mac-poly-M8-skip_proofs file | annotate | diff | comparison | revisions
Admin/isatest/settings/mac-poly64-M2 file | annotate | diff | comparison | revisions
Admin/isatest/settings/mac-poly64-M4 file | annotate | diff | comparison | revisions
Admin/isatest/settings/mac-poly64-M8 file | annotate | diff | comparison | revisions 
--- 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
 
--- 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"
-
--- 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"
-
--- 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"
-
--- 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
--- 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
 
--- 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
 
--- 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"
--- 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"
--- 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"
-
--- 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"
--- 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"
isabelle