author | wenzelm |
Sat, 19 Apr 2014 17:23:05 +0200 | |
changeset 56618 | 874bdedb2313 |
parent 53838 | b9285f30a80a |
child 56961 | 2ac12a7b1a69 |
permissions | -rw-r--r-- |
31581 | 1 |
# -*- shell-script -*- :mode=shellscript: |
2 |
||
49345
f182f7fa158f
more standard init_components -- particularly important to pick up correct jdk/scala version;
wenzelm
parents:
48729
diff
changeset
|
3 |
init_components /home/isabelle/contrib "$HOME/admin/components/main" |
f182f7fa158f
more standard init_components -- particularly important to pick up correct jdk/scala version;
wenzelm
parents:
48729
diff
changeset
|
4 |
|
53687 | 5 |
POLYML_HOME="/home/polyml/polyml-5.5.1" |
53334
646a224ca76a
some tests on /home/polyml/polyml-svn, which is approaching polyml-5.5.1;
wenzelm
parents:
50871
diff
changeset
|
6 |
ML_SYSTEM="polyml-5.5.1" |
31581 | 7 |
ML_PLATFORM="x86-darwin" |
8 |
ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
|
53838 | 9 |
ML_OPTIONS="-H 500 --gcthreads 4" |
31581 | 10 |
|
11 |
||
31584 | 12 |
ISABELLE_HOME_USER=~/isabelle-mac-poly-M4 |
31581 | 13 |
|
14 |
# Where to look for isabelle tools (multiple dirs separated by ':'). |
|
15 |
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" |
|
16 |
||
17 |
# Location for temporary files (should be on a local file system). |
|
18 |
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" |
|
19 |
||
20 |
||
21 |
# Heap input locations. ML system identifier is included in lookup. |
|
22 |
ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" |
|
23 |
||
24 |
# Heap output location. ML system identifier is appended automatically later on. |
|
25 |
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" |
|
26 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" |
|
27 |
||
50871
2ea3c90ff0bb
more exhaustive full test, to avoid surprises with makedist_library;
wenzelm
parents:
50681
diff
changeset
|
28 |
ISABELLE_BUILD_OPTIONS="browser_info=false document=pdf document_variants=document:outline=/proof,/ML threads=4 parallel_proofs=2" |
31581 | 29 |
|
50285
f25bcb8a4591
prefer 32 bit platform for ISABELLE_FULL_TEST, to make memory problems more explicit instead of disk thrashing (notably in HOL-Quickcheck_Benchmark);
wenzelm
parents:
49405
diff
changeset
|
30 |
ISABELLE_FULL_TEST=true |
f25bcb8a4591
prefer 32 bit platform for ISABELLE_FULL_TEST, to make memory problems more explicit instead of disk thrashing (notably in HOL-Quickcheck_Benchmark);
wenzelm
parents:
49405
diff
changeset
|
31 |
|
50681 | 32 |
Z3_NON_COMMERCIAL="yes" |
33 |