author | haftmann |
Sat, 04 Jun 2005 21:35:20 +0200 | |
changeset 16237 | d97b594cba5f |
parent 16186 | 6eb74e2cec7e |
child 16250 | 1a91cdebd604 |
permissions | -rw-r--r-- |
10503 | 1 |
# -*- shell-script -*- |
2294 | 2 |
# $Id$ |
3 |
# |
|
2309 | 4 |
# Isabelle settings -- site defaults. |
9225 | 5 |
# Do *NOT* copy this file into your personal isabelle directory!!! |
2309 | 6 |
|
2426 | 7 |
### |
3177 | 8 |
### ML compiler settings (ESSENTIAL!) |
2426 | 9 |
### |
10 |
||
9236 | 11 |
# Note that ML_HOME specifies the location of the actual compiler |
12 |
# binaries. Do not invent new ML system names unless you know what |
|
9759 | 13 |
# you are doing. Only one of the sections below should be activated. |
2426 | 14 |
|
14461
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
15 |
|
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
16 |
# try finding the poly packages from the Isabelle site in the usual places |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
17 |
POLYML_HOME=$(choosefrom \ |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
18 |
"$ISABELLE_HOME/contrib/polyml" \ |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
19 |
"$ISABELLE_HOME/../polyml" \ |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
20 |
"/usr/share/polyml" \ |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
21 |
"/usr/local/polyml" \ |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
22 |
"/opt/polyml") |
14447 | 23 |
|
14461
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
24 |
if [ -n "$POLYML_HOME" -a -e "$POLYML_HOME/bin/polyml-version" ]; then |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
25 |
# looks like Isabelle poly packages |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
26 |
ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml) |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
27 |
ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform) |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
28 |
ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
29 |
ML_OPTIONS="-h 15000" |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
30 |
elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
31 |
# maybe a shrink-wrapped polyml on x86-linux ... |
fab539f843d9
look for multi platform poly first, choose shrink wrapped poly-4.1.3 (guess) only
kleing
parents:
14451
diff
changeset
|
32 |
|
14613 | 33 |
# Poly/ML 4.0, 4.1, 4.1.x |
14447 | 34 |
# include version number, needed for choosing right options |
15734
56a807868e23
Include automatic determination of poly version.
aspinall
parents:
15717
diff
changeset
|
35 |
# If automatic setting doesn't work, use e.g. ML_VERSION=4.1.3 |
15865
222092a48131
removed --version which is not a valid polyml flag and has no effect
gagern
parents:
15846
diff
changeset
|
36 |
ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p') |
15734
56a807868e23
Include automatic determination of poly version.
aspinall
parents:
15717
diff
changeset
|
37 |
ML_SYSTEM=polyml-${ML_VERSION} |
14447 | 38 |
# processor/OS type |
10205
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
39 |
ML_PLATFORM=x86-linux |
14447 | 40 |
# where to find binaries |
10205
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
41 |
ML_HOME=/usr/bin |
14447 | 42 |
# where to find the standard database |
10205
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
43 |
ML_DBASE=/usr/lib/poly/ML_dbase |
14447 | 44 |
# options to pass to poly |
12752 | 45 |
ML_OPTIONS="-h 15000" |
10205
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
46 |
fi |
8345 | 47 |
|
5708 | 48 |
# Standard ML of New Jersey 110 or later |
8345 | 49 |
#ML_SYSTEM=smlnj-110 |
15846 | 50 |
#ML_HOME="$ISABELLE_HOME/contrib/smlnj/bin" |
8345 | 51 |
#ML_OPTIONS="@SMLdebug=/dev/null" |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
52 |
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") |
5708 | 53 |
|
9252 | 54 |
# Moscow ML 2.00 or later (experimental!) |
55 |
#ML_SYSTEM=mosml |
|
15846 | 56 |
#ML_HOME="$ISABELLE_HOME/contrib/mosml/bin" |
6413 | 57 |
#ML_PLATFORM="" |
9252 | 58 |
#ML_OPTIONS="" |
5708 | 59 |
|
2294 | 60 |
|
2426 | 61 |
### |
16186 | 62 |
### Compilation options (cf. isatool usedir) |
2435 | 63 |
### |
64 |
||
14253 | 65 |
ISABELLE_USEDIR_OPTIONS="-v true" |
11569 | 66 |
|
16186 | 67 |
# Specifically for the HOL image |
68 |
HOL_USEDIR_OPTIONS="" |
|
14044
bbd2f7b00736
set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible)
kleing
parents:
13920
diff
changeset
|
69 |
|
2435 | 70 |
|
71 |
### |
|
16186 | 72 |
### Document preparation (cf. isatool latex/document) |
7773 | 73 |
### |
74 |
||
75 |
ISABELLE_LATEX="latex" |
|
76 |
ISABELLE_PDFLATEX="pdflatex" |
|
7813 | 77 |
ISABELLE_BIBTEX="bibtex" |
14344 | 78 |
ISABELLE_MAKEINDEX="makeindex" |
7773 | 79 |
ISABELLE_DVIPS="dvips -D 600" |
11800 | 80 |
ISABELLE_EPSTOPDF="epstopdf" |
7773 | 81 |
|
13920 | 82 |
# Paranoia setting for strange latex installations ... |
11062 | 83 |
#unset TEXMF |
84 |
||
13920 | 85 |
# If ISABELLE_THUMBPDF is set, isatool tries to |
86 |
# generate thumbnails for proof documents |
|
11062 | 87 |
#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf" |
7864 | 88 |
|
7773 | 89 |
|
90 |
### |
|
2968 | 91 |
### Misc path settings |
2426 | 92 |
### |
2294 | 93 |
|
2426 | 94 |
# The place for user configuration, heap files, etc. |
95 |
ISABELLE_HOME_USER=~/isabelle |
|
2294 | 96 |
|
3177 | 97 |
# Where to look for isabelle tools (multiple dirs separated by ':'). |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
98 |
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" |
2786 | 99 |
|
4334 | 100 |
# Location for temporary files (should be on a local file system). |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
101 |
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" |
4334 | 102 |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
103 |
# Heap input locations. ML system identifier is included in lookup. |
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
104 |
ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" |
2780 | 105 |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
106 |
# Heap output location. ML system identifier is appended automatically later on. |
15846 | 107 |
if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then |
108 |
#Isabelle build tells us to store heaps etc. within the distribution. |
|
109 |
ISABELLE_OUTPUT="$ISABELLE_HOME/heaps" |
|
110 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info" |
|
111 |
else |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
112 |
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" |
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
113 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" |
15846 | 114 |
fi |
2780 | 115 |
|
16186 | 116 |
# Site settings check -- just to make it a little bit harder to copy this file verbatim! |
9225 | 117 |
[ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
118 |
{ echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
|
119 |
||
13920 | 120 |
|
121 |
### |
|
16186 | 122 |
### default logic (users may want to override this in their own settings file) |
13920 | 123 |
### |
16186 | 124 |
|
3184 | 125 |
ISABELLE_LOGIC=HOL |
2294 | 126 |
|
2786 | 127 |
|
13920 | 128 |
### |
129 |
### Docs |
|
130 |
### |
|
2294 | 131 |
|
16186 | 132 |
# Where to look for docs (multiple dirs separated by ':'). |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
133 |
ISABELLE_DOCS="$ISABELLE_HOME/doc" |
2345 | 134 |
|
16186 | 135 |
# Preferred document format |
15703 | 136 |
ISABELLE_DOC_FORMAT=pdf |
137 |
||
16186 | 138 |
# The dvi file viewer |
3062 | 139 |
DVI_VIEWER=xdvi |
2426 | 140 |
#DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5" |
11103 | 141 |
#DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7" |
2476 | 142 |
#DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10" |
3062 | 143 |
#DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9" |
2345 | 144 |
|
16186 | 145 |
# The pdf file viewer |
15218 | 146 |
PDF_VIEWER=acroread |
147 |
#PDF_VIEWER=xpdf |
|
16186 | 148 |
#PDF_VIEWER=open #best for Mac users: will open in default PDF viewer |
15218 | 149 |
|
16186 | 150 |
# Printer spool command for PS files |
14933 | 151 |
PRINT_COMMAND=lp |
152 |
||
2294 | 153 |
|
2426 | 154 |
### |
155 |
### Interfaces |
|
156 |
### |
|
157 |
||
13920 | 158 |
# ISABELLE_INTERFACE is the program which is run by the Isabelle command |
159 |
||
160 |
# Fallback: the null interface (pass-through to raw isabelle process). |
|
11552
aca5398ccd35
ISABELLE_INTERFACE=none by default (cannot expect X11 everywhere);
wenzelm
parents:
11103
diff
changeset
|
161 |
ISABELLE_INTERFACE=none |
2294 | 162 |
|
13920 | 163 |
# Proof General path, look in a variety of places |
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15734
diff
changeset
|
164 |
ISABELLE_INTERFACE=$(choosefrom\ |
9679 | 165 |
"$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \ |
166 |
"$ISABELLE_HOME/../ProofGeneral/isar/interface" \ |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
167 |
"/usr/share/ProofGeneral/isar/interface" \ |
9948 | 168 |
"/usr/local/ProofGeneral/isar/interface" \ |
10070 | 169 |
"/opt/ProofGeneral/isar/interface" \ |
9956
e75e6a603e71
added /usr/share/emacs/ProofGeneral/isar/interface choice;
wenzelm
parents:
9948
diff
changeset
|
170 |
"/usr/share/emacs/ProofGeneral/isar/interface" \ |
9679 | 171 |
"$ISABELLE_INTERFACE") |
13920 | 172 |
|
173 |
# Options to pass to Isabelle command when PG is selected as interface |
|
5964 | 174 |
PROOFGENERAL_OPTIONS="" |
11981 | 175 |
#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true" |
7185 | 176 |
|
13920 | 177 |
# try xemacs first, else emacs |
12476 | 178 |
type -path xemacs >/dev/null || PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS" |
179 |
||
180 |
||
13920 | 181 |
# X-Symbol installation location (for Proof General, obsolete for PG >= 3.5) |
9679 | 182 |
XSYMBOL_HOME=$(choosefrom \ |
183 |
"$ISABELLE_HOME/contrib/x-symbol" \ |
|
184 |
"$ISABELLE_HOME/../x-symbol" \ |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
185 |
"/usr/share/x-symbol" \ |
9948 | 186 |
"/usr/local/x-symbol" \ |
10070 | 187 |
"/opt/x-symbol" \ |
9679 | 188 |
"") |
13920 | 189 |
|
190 |
# Executed before xemacs with ProofGeneral is called. |
|
191 |
# Required for remote fonts only. |
|
9994 | 192 |
#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
9569 | 193 |
|
7185 | 194 |
|
195 |
### |
|
196 |
### External reasoning tools |
|
197 |
### |
|
198 |
||
7194 | 199 |
## Set HOME only for tools you have installed! |
7185 | 200 |
|
201 |
# SVC (Stanford Validity Checker) |
|
202 |
#SVC_HOME= |
|
203 |
#SVC_MACHINE=i386-redhat-linux |
|
204 |
#SVC_MACHINE=sparc-sun-solaris |
|
7296 | 205 |
|
206 |
# Mucke (mu-calculus model checker) |
|
207 |
#MUCKE_HOME=/usr/local/bin |
|
208 |
||
209 |
# Einhoven model checker |
|
210 |
#EINDHOVEN_HOME=/usr/local/bin |
|
14451 | 211 |
|
15331 | 212 |
# zChaff (SAT Solver) |
15284 | 213 |
#ZCHAFF_HOME=/usr/local/bin |
15331 | 214 |
#ZCHAFF_VERSION=2004.5.13 |
215 |
#ZCHAFF_VERSION=2004.11.15 |
|
14942 | 216 |
|
217 |
# BerkMin561 (SAT Solver) |
|
218 |
#BERKMIN_HOME=/usr/local/bin |
|
219 |
#BERKMIN_EXE=BerkMin561-linux |
|
220 |
#BERKMIN_EXE=BerkMin561-solaris |
|
14943 | 221 |
|
222 |
# Jerusat 1.3 (SAT Solver) |
|
223 |
#JERUSAT_HOME=/usr/local/bin |