author | wenzelm |
Tue, 13 Feb 2001 01:32:54 +0100 | |
changeset 11103 | 2a3cc8e1723a |
parent 11062 | e86340dc1d28 |
child 11552 | aca5398ccd35 |
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 |
|
10205
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
17 |
# Poly/ML 3.x and 4.0 |
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 |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
19 |
#maybe a shrink-wrapped polyml-4.0 on x86-linux ... |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
20 |
ML_SYSTEM=polyml-4.0 |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
21 |
ML_PLATFORM=x86-linux |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
22 |
ML_HOME=/usr/bin |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
23 |
ML_DBASE=/usr/lib/poly/ML_dbase |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
24 |
ML_OPTIONS="-h 30000" |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
25 |
else |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
26 |
#... 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
|
27 |
POLYML_HOME=$(choosefrom \ |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
28 |
"$ISABELLE_HOME/contrib/polyml" \ |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
29 |
"$ISABELLE_HOME/../polyml" \ |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
30 |
"/usr/share/polyml" \ |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
31 |
"/usr/local/polyml" \ |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
32 |
"/opt/polyml") |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
33 |
ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml) |
10503 | 34 |
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
|
35 |
ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
36 |
ML_OPTIONS="-h 30000" |
7f3d844c9512
even smarter setup for several installations of Poly/ML 3.x and 4.0;
wenzelm
parents:
10070
diff
changeset
|
37 |
fi |
8345 | 38 |
|
5708 | 39 |
# Standard ML of New Jersey 110 or later |
8345 | 40 |
#ML_SYSTEM=smlnj-110 |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
41 |
#ML_HOME="$ISABELLE_HOME/../smlnj/bin" |
8345 | 42 |
#ML_OPTIONS="@SMLdebug=/dev/null" |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
43 |
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") |
5708 | 44 |
|
11062 | 45 |
# MLWorks 2.0 |
46 |
#ML_SYSTEM=mlworks |
|
47 |
#ML_HOME="$ISABELLE_HOME/../mlworks/bin" |
|
48 |
#ML_OPTIONS="" |
|
49 |
#ML_PLATFORM="" |
|
50 |
||
9252 | 51 |
# Moscow ML 2.00 or later (experimental!) |
52 |
#ML_SYSTEM=mosml |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
53 |
#ML_HOME="$ISABELLE_HOME/../mosml/bin" |
6413 | 54 |
#ML_PLATFORM="" |
9252 | 55 |
#ML_OPTIONS="" |
5708 | 56 |
|
2426 | 57 |
# Standard ML of New Jersey 0.93 |
58 |
#ML_SYSTEM=smlnj-0.93 |
|
59 |
#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
|
60 |
#ML_OPTIONS="" |
|
6413 | 61 |
#ML_PLATFORM="" |
2426 | 62 |
|
2294 | 63 |
|
2426 | 64 |
### |
3177 | 65 |
### Compilation options |
2435 | 66 |
### |
67 |
||
5387 | 68 |
ISABELLE_USEDIR_OPTIONS="-i false" |
7762
c98d70538033
ISABELLE_USEDIR_OPTIONS: -d pdf option (off by default);
wenzelm
parents:
7296
diff
changeset
|
69 |
#ISABELLE_USEDIR_OPTIONS="-i true -d pdf" |
2435 | 70 |
|
71 |
||
72 |
### |
|
7773 | 73 |
### Document preparation |
74 |
### |
|
75 |
||
76 |
TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS" |
|
77 |
ISABELLE_LATEX="latex" |
|
78 |
ISABELLE_PDFLATEX="pdflatex" |
|
7813 | 79 |
ISABELLE_BIBTEX="bibtex" |
7773 | 80 |
ISABELLE_DVIPS="dvips -D 600" |
81 |
||
11062 | 82 |
# Paranoia setting ... |
83 |
#unset TEXMF |
|
84 |
||
7873 | 85 |
# The thumbpdf tool is probably not generally available ... |
11062 | 86 |
#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf" |
7864 | 87 |
|
7773 | 88 |
|
89 |
### |
|
2968 | 90 |
### Misc path settings |
2426 | 91 |
### |
2294 | 92 |
|
2426 | 93 |
# The place for user configuration, heap files, etc. |
94 |
ISABELLE_HOME_USER=~/isabelle |
|
2294 | 95 |
|
3177 | 96 |
# 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
|
97 |
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" |
2786 | 98 |
|
4334 | 99 |
# 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
|
100 |
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" |
4334 | 101 |
|
2786 | 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. |
2780 | 107 |
if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
108 |
#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
|
109 |
ISABELLE_OUTPUT="$ISABELLE_HOME/heaps" |
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
110 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info" |
2780 | 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" |
2780 | 114 |
fi |
115 |
||
9225 | 116 |
# Site settings check -- just to make it a little bit harder to copy this file! |
117 |
[ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
|
118 |
{ echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
|
119 |
||
3177 | 120 |
#Users may want to change this. |
3184 | 121 |
ISABELLE_LOGIC=HOL |
2294 | 122 |
|
2786 | 123 |
|
124 |
## Docs |
|
2294 | 125 |
|
3177 | 126 |
#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
|
127 |
ISABELLE_DOCS="$ISABELLE_HOME/doc" |
2345 | 128 |
|
3177 | 129 |
#The dvi file viewer |
3062 | 130 |
DVI_VIEWER=xdvi |
2426 | 131 |
#DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5" |
11103 | 132 |
#DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7" |
2476 | 133 |
#DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10" |
3062 | 134 |
#DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9" |
2345 | 135 |
|
2294 | 136 |
|
3158 | 137 |
## Fonts -- how to install the Isabelle X11 fonts (can be tricky!). |
138 |
||
139 |
# (1) Get fonts from local (client side) directory: |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
140 |
ISABELLE_INSTALLFONTS="xset fp+ \"$ISABELLE_HOME/lib/fonts\"; xset fp rehash" |
3158 | 141 |
|
3689 | 142 |
# (2) Get from font server at Munich or Cambridge: |
3256 | 143 |
#ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
3689 | 144 |
#ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100" |
2577 | 145 |
|
5964 | 146 |
|
2426 | 147 |
### |
148 |
### Interfaces |
|
149 |
### |
|
150 |
||
151 |
# The null interface: pass-through to 'isabelle'. |
|
2294 | 152 |
#ISABELLE_INTERFACE=none |
153 |
||
2786 | 154 |
# Simple xterm based interface. |
2294 | 155 |
ISABELLE_INTERFACE=xterm |
5964 | 156 |
ISABELLE_XTERM_OPTIONS="" |
2968 | 157 |
|
3303 | 158 |
# Emacs running Isamode. |
2968 | 159 |
#ISABELLE_INTERFACE=emacs |
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
160 |
ISAMODE_HOME="$ISABELLE_HOME/contrib/Isamode" |
5964 | 161 |
ISAMODE_OPTIONS="" |
162 |
||
9679 | 163 |
# Proof General |
164 |
ISABELLE_INTERFACE=$(choosefrom \ |
|
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") |
5964 | 172 |
PROOFGENERAL_OPTIONS="" |
7185 | 173 |
|
9759 | 174 |
# X-Symbol mode for Proof General |
9679 | 175 |
XSYMBOL_HOME=$(choosefrom \ |
176 |
"$ISABELLE_HOME/contrib/x-symbol" \ |
|
177 |
"$ISABELLE_HOME/../x-symbol" \ |
|
9787
fb8c5a66dbe8
more robust handling of spaces in args / file names;
wenzelm
parents:
9759
diff
changeset
|
178 |
"/usr/share/x-symbol" \ |
9948 | 179 |
"/usr/local/x-symbol" \ |
10070 | 180 |
"/opt/x-symbol" \ |
9679 | 181 |
"") |
11062 | 182 |
# Required for remote fonts only ... |
9994 | 183 |
#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
9569 | 184 |
|
7185 | 185 |
|
186 |
### |
|
187 |
### External reasoning tools |
|
188 |
### |
|
189 |
||
7194 | 190 |
## Set HOME only for tools you have installed! |
7185 | 191 |
|
192 |
# SVC (Stanford Validity Checker) |
|
193 |
#SVC_HOME= |
|
194 |
#SVC_MACHINE=i386-redhat-linux |
|
195 |
#SVC_MACHINE=sparc-sun-solaris |
|
7296 | 196 |
|
197 |
# Mucke (mu-calculus model checker) |
|
198 |
#MUCKE_HOME=/usr/local/bin |
|
199 |
||
200 |
# Einhoven model checker |
|
201 |
#EINDHOVEN_HOME=/usr/local/bin |