explicit test of quick_and_dirty, which is rarely used in practice;
authorwenzelm
Mon Sep 16 13:56:02 2013 +0200 (2013-09-16)
changeset 53662396e7db3240c
parent 53661 7b4cefeb87d8
child 53663 62f42e9ec0f3
explicit test of quick_and_dirty, which is rarely used in practice;
Admin/isatest/isatest-makedist
Admin/isatest/settings/mac-poly-M8-quick_and_dirty
     1.1 --- a/Admin/isatest/isatest-makedist	Mon Sep 16 13:54:58 2013 +0200
     1.2 +++ b/Admin/isatest/isatest-makedist	Mon Sep 16 13:56:02 2013 +0200
     1.3 @@ -113,7 +113,8 @@
     1.4    $MAKEALL $HOME/settings/mac-poly64-M8;
     1.5    $MAKEALL $HOME/settings/mac-poly-M4;
     1.6    $MAKEALL $HOME/settings/mac-poly-M8;
     1.7 -  $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs"
     1.8 +  $MAKEALL $HOME/settings/mac-poly-M8-skip_proofs;
     1.9 +  $MAKEALL $HOME/settings/mac-poly-M8-quick_and_dirty"
    1.10  sleep 15
    1.11  $SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly64-M2"
    1.12  sleep 15
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/Admin/isatest/settings/mac-poly-M8-quick_and_dirty	Mon Sep 16 13:56:02 2013 +0200
     2.3 @@ -0,0 +1,31 @@
     2.4 +# -*- shell-script -*- :mode=shellscript:
     2.5 +
     2.6 +init_components /home/isabelle/contrib "$HOME/admin/components/main"
     2.7 +
     2.8 +  POLYML_HOME="/home/polyml/polyml-5.5.0"
     2.9 +  ML_SYSTEM="polyml-5.5.0"
    2.10 +  ML_PLATFORM="x86-darwin"
    2.11 +  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    2.12 +  ML_OPTIONS="-H 1000 --gcthreads 8"
    2.13 +
    2.14 +
    2.15 +ISABELLE_HOME_USER=~/isabelle-mac-poly-M8-quick_and_dirty
    2.16 +
    2.17 +# Where to look for isabelle tools (multiple dirs separated by ':').
    2.18 +ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
    2.19 +
    2.20 +# Location for temporary files (should be on a local file system).
    2.21 +ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
    2.22 +
    2.23 +
    2.24 +# Heap input locations. ML system identifier is included in lookup.
    2.25 +ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
    2.26 +
    2.27 +# Heap output location. ML system identifier is appended automatically later on.
    2.28 +ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
    2.29 +ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
    2.30 +
    2.31 +ISABELLE_BUILD_OPTIONS="threads=8 quick_and_dirty"
    2.32 +
    2.33 +Z3_NON_COMMERCIAL="yes"
    2.34 +