| author | haftmann | 
| Tue, 26 May 2009 13:40:49 +0200 | |
| changeset 31255 | 0f8cb37bcafd | 
| parent 29643 | 5e0df4b6849e | 
| child 31310 | b5365a9db718 | 
| permissions | -rw-r--r-- | 
| 25529 | 1  | 
# -*- shell-script -*-  | 
2  | 
||
| 28669 | 3  | 
POLYML_HOME="/home/polyml/polyml-5.2.1"  | 
4  | 
ML_SYSTEM="polyml-5.2.1"  | 
|
| 25529 | 5  | 
ML_PLATFORM="x86_64-linux"  | 
6  | 
ML_HOME="$POLYML_HOME/$ML_PLATFORM"  | 
|
7  | 
ML_OPTIONS="-H 500"  | 
|
8  | 
||
| 27088 | 9  | 
ISABELLE_HOME_USER=~/isabelle-at64-poly-para-e  | 
| 25529 | 10  | 
|
11  | 
# Where to look for isabelle tools (multiple dirs separated by ':').  | 
|
12  | 
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"  | 
|
13  | 
||
14  | 
# Location for temporary files (should be on a local file system).  | 
|
15  | 
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"  | 
|
16  | 
||
17  | 
||
18  | 
# Heap input locations. ML system identifier is included in lookup.  | 
|
19  | 
ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"  | 
|
20  | 
||
21  | 
# Heap output location. ML system identifier is appended automatically later on.  | 
|
| 26210 | 22  | 
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"  | 
23  | 
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"  | 
|
| 25529 | 24  | 
|
25  | 
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 2"  | 
|
26  | 
||
| 
29643
 
5e0df4b6849e
HOL_USEDIR_OPTIONS: -Q false, giving up parallel proofs for now due to memory shortage;
 
wenzelm 
parents: 
28669 
diff
changeset
 | 
27  | 
HOL_USEDIR_OPTIONS="-p 2 -Q false"  |