| author | blanchet | 
| Mon, 20 Jan 2014 18:24:56 +0100 | |
| changeset 55073 | 9b96fb4c8cfd | 
| 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  |