author | webertj |
Wed, 10 Mar 2004 20:21:08 +0100 | |
changeset 14451 | 2253d273d944 |
parent 14447 | 5b61dc4eab24 |
child 14461 | fab539f843d9 |
permissions | -rw-r--r-- |
10503 | 1 |
# -*- shell-script -*- |
2294 | 2 |
# $Id$ |
9818 | 3 |
# Author: Markus Wenzel, TU Muenchen |
4 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
2294 | 5 |
# |
2309 | 6 |
# Isabelle settings -- site defaults. |
9225 | 7 |
# Do *NOT* copy this file into your personal isabelle directory!!! |
2309 | 8 |
|
2426 | 9 |
### |
3177 | 10 |
### ML compiler settings (ESSENTIAL!) |
2426 | 11 |
### |
12 |
||
9236 | 13 |
# Note that ML_HOME specifies the location of the actual compiler |
14 |
# binaries. Do not invent new ML system names unless you know what |
|
9759 | 15 |
# you are doing. Only one of the sections below should be activated. |
2426 | 16 |
|
12828 | 17 |
# Poly/ML 3.x, 4.0, 4.1, 4.1.1, 4.1.2 |
10205
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
18 |
if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then |
14447 | 19 |
#maybe a shrink-wrapped polyml on x86-linux ... |
20 |
||
21 |
# include version number, needed for choosing right options |
|
22 |
ML_SYSTEM=polyml-4.1.3 |
|
23 |
# processor/OS type |
|
10205
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
24 |
ML_PLATFORM=x86-linux |
14447 | 25 |
# 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
|
26 |
ML_HOME=/usr/bin |
14447 | 27 |
# 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
|
28 |
ML_DBASE=/usr/lib/poly/ML_dbase |
14447 | 29 |
# options to pass to poly |
12752 | 30 |
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
|
31 |
else |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
32 |
#... or rather a self-contained multi-platform installation |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
33 |
POLYML_HOME=$(choosefrom \ |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
34 |
"$ISABELLE_HOME/contrib/polyml" \ |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
35 |
"$ISABELLE_HOME/../polyml" \ |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
36 |
"/usr/share/polyml" \ |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
37 |
"/usr/local/polyml" \ |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
38 |
"/opt/polyml") |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
39 |
ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml) |
10503 | 40 |
ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform) |
10205
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
41 |
ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
12752 | 42 |
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
|
43 |
fi |
8345 | 44 |
|
5708 | 45 |
# Standard ML of New Jersey 110 or later |
8345 | 46 |
#ML_SYSTEM=smlnj-110 |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
47 |
#ML_HOME="$ISABELLE_HOME/../smlnj/bin" |
8345 | 48 |
#ML_OPTIONS="@SMLdebug=/dev/null" |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
49 |
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") |
5708 | 50 |
|
11062 | 51 |
# MLWorks 2.0 |
52 |
#ML_SYSTEM=mlworks |
|
53 |
#ML_HOME="$ISABELLE_HOME/../mlworks/bin" |
|
54 |
#ML_OPTIONS="" |
|
55 |
#ML_PLATFORM="" |
|
56 |
||
9252 | 57 |
# Moscow ML 2.00 or later (experimental!) |
58 |
#ML_SYSTEM=mosml |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
59 |
#ML_HOME="$ISABELLE_HOME/../mosml/bin" |
6413 | 60 |
#ML_PLATFORM="" |
9252 | 61 |
#ML_OPTIONS="" |
5708 | 62 |
|
2426 | 63 |
# Standard ML of New Jersey 0.93 |
64 |
#ML_SYSTEM=smlnj-0.93 |
|
65 |
#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
|
66 |
#ML_OPTIONS="" |
|
6413 | 67 |
#ML_PLATFORM="" |
2426 | 68 |
|
2294 | 69 |
|
2426 | 70 |
### |
13920 | 71 |
### Compilation options for isatool usedir |
72 |
### (as on command line) |
|
2435 | 73 |
### |
74 |
||
14253 | 75 |
ISABELLE_USEDIR_OPTIONS="-v true" |
11569 | 76 |
|
14044
bbd2f7b00736
set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible)
kleing
parents:
13920
diff
changeset
|
77 |
# for overriding proof objects in HOL image |
bbd2f7b00736
set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible)
kleing
parents:
13920
diff
changeset
|
78 |
HOL_PROOF_OBJECTS="" |
bbd2f7b00736
set HOL_PROOF_OBJECTS in settings, not makefile (makes override in user settings possible)
kleing
parents:
13920
diff
changeset
|
79 |
|
2435 | 80 |
|
81 |
### |
|
7773 | 82 |
### Document preparation |
83 |
### |
|
84 |
||
13920 | 85 |
# latex command for isatool latex/document |
7773 | 86 |
ISABELLE_LATEX="latex" |
13920 | 87 |
|
88 |
# pdflatex command for isatool latex/document |
|
7773 | 89 |
ISABELLE_PDFLATEX="pdflatex" |
13920 | 90 |
|
91 |
# bibtex command for isatool latex/document |
|
7813 | 92 |
ISABELLE_BIBTEX="bibtex" |
13920 | 93 |
|
14344 | 94 |
# makeindex command for isatool latex/document |
95 |
ISABELLE_MAKEINDEX="makeindex" |
|
96 |
||
13920 | 97 |
# dvips command for isatool latex/document |
7773 | 98 |
ISABELLE_DVIPS="dvips -D 600" |
13920 | 99 |
|
100 |
# epstopdf command for isatool latex/document |
|
11800 | 101 |
ISABELLE_EPSTOPDF="epstopdf" |
7773 | 102 |
|
13920 | 103 |
# Paranoia setting for strange latex installations ... |
11062 | 104 |
#unset TEXMF |
105 |
||
13920 | 106 |
# If ISABELLE_THUMBPDF is set, isatool tries to |
107 |
# generate thumbnails for proof documents |
|
108 |
# |
|
109 |
# probably not generally available ... |
|
11062 | 110 |
#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf" |
7864 | 111 |
|
7773 | 112 |
|
113 |
### |
|
2968 | 114 |
### Misc path settings |
2426 | 115 |
### |
2294 | 116 |
|
2426 | 117 |
# The place for user configuration, heap files, etc. |
118 |
ISABELLE_HOME_USER=~/isabelle |
|
2294 | 119 |
|
3177 | 120 |
# 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
|
121 |
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" |
2786 | 122 |
|
4334 | 123 |
# 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
|
124 |
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" |
4334 | 125 |
|
2786 | 126 |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
127 |
# 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
|
128 |
ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" |
2780 | 129 |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
130 |
# Heap output location. ML system identifier is appended automatically later on. |
2780 | 131 |
if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
132 |
#Isabelle build tells us to store heaps etc. within the distribution. |
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
133 |
ISABELLE_OUTPUT="$ISABELLE_HOME/heaps" |
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
134 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info" |
2780 | 135 |
else |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
136 |
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" |
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
137 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" |
2780 | 138 |
fi |
139 |
||
9225 | 140 |
# Site settings check -- just to make it a little bit harder to copy this file! |
141 |
[ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
|
142 |
{ echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
|
143 |
||
13920 | 144 |
|
145 |
### |
|
146 |
### default logic, users may want to override this. |
|
147 |
### |
|
3184 | 148 |
ISABELLE_LOGIC=HOL |
2294 | 149 |
|
2786 | 150 |
|
13920 | 151 |
### |
152 |
### Docs |
|
153 |
### |
|
2294 | 154 |
|
3177 | 155 |
#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
|
156 |
ISABELLE_DOCS="$ISABELLE_HOME/doc" |
2345 | 157 |
|
3177 | 158 |
#The dvi file viewer |
3062 | 159 |
DVI_VIEWER=xdvi |
2426 | 160 |
#DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5" |
11103 | 161 |
#DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7" |
2476 | 162 |
#DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10" |
3062 | 163 |
#DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9" |
2345 | 164 |
|
2294 | 165 |
|
2426 | 166 |
### |
167 |
### Interfaces |
|
168 |
### |
|
169 |
||
13920 | 170 |
# ISABELLE_INTERFACE is the program which is run by the Isabelle command |
171 |
||
172 |
# 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
|
173 |
ISABELLE_INTERFACE=none |
2294 | 174 |
|
13920 | 175 |
# Emacs running (obsolete) Isamode. |
2968 | 176 |
#ISABELLE_INTERFACE=emacs |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
177 |
ISAMODE_HOME="$ISABELLE_HOME/contrib/Isamode" |
5964 | 178 |
ISAMODE_OPTIONS="" |
179 |
||
13920 | 180 |
# Proof General path, look in a variety of places |
9679 | 181 |
ISABELLE_INTERFACE=$(choosefrom \ |
182 |
"$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \ |
|
183 |
"$ISABELLE_HOME/../ProofGeneral/isar/interface" \ |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
184 |
"/usr/share/ProofGeneral/isar/interface" \ |
9948 | 185 |
"/usr/local/ProofGeneral/isar/interface" \ |
10070 | 186 |
"/opt/ProofGeneral/isar/interface" \ |
9956
e75e6a603e71
added /usr/share/emacs/ProofGeneral/isar/interface choice;
wenzelm
parents:
9948
diff
changeset
|
187 |
"/usr/share/emacs/ProofGeneral/isar/interface" \ |
9679 | 188 |
"$ISABELLE_INTERFACE") |
13920 | 189 |
|
190 |
# Options to pass to Isabelle command when PG is selected as interface |
|
5964 | 191 |
PROOFGENERAL_OPTIONS="" |
11981 | 192 |
#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true" |
7185 | 193 |
|
13920 | 194 |
# try xemacs first, else emacs |
12476 | 195 |
type -path xemacs >/dev/null || PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS" |
196 |
||
197 |
||
13920 | 198 |
# X-Symbol installation location (for Proof General, obsolete for PG >= 3.5) |
9679 | 199 |
XSYMBOL_HOME=$(choosefrom \ |
200 |
"$ISABELLE_HOME/contrib/x-symbol" \ |
|
201 |
"$ISABELLE_HOME/../x-symbol" \ |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
202 |
"/usr/share/x-symbol" \ |
9948 | 203 |
"/usr/local/x-symbol" \ |
10070 | 204 |
"/opt/x-symbol" \ |
9679 | 205 |
"") |
13920 | 206 |
|
207 |
# Executed before xemacs with ProofGeneral is called. |
|
208 |
# Required for remote fonts only. |
|
9994 | 209 |
#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
9569 | 210 |
|
7185 | 211 |
|
212 |
### |
|
213 |
### External reasoning tools |
|
214 |
### |
|
215 |
||
7194 | 216 |
## Set HOME only for tools you have installed! |
7185 | 217 |
|
218 |
# SVC (Stanford Validity Checker) |
|
219 |
#SVC_HOME= |
|
220 |
#SVC_MACHINE=i386-redhat-linux |
|
221 |
#SVC_MACHINE=sparc-sun-solaris |
|
7296 | 222 |
|
223 |
# Mucke (mu-calculus model checker) |
|
224 |
#MUCKE_HOME=/usr/local/bin |
|
225 |
||
226 |
# Einhoven model checker |
|
227 |
#EINDHOVEN_HOME=/usr/local/bin |
|
14451 | 228 |
|
229 |
# ZChaff SAT solver |
|
230 |
#ZCHAFF_HOME=/usr/local/bin |