author | wenzelm |
Wed, 26 Sep 2001 20:33:33 +0200 | |
changeset 11569 | 06d6f1ea6021 |
parent 11552 | aca5398ccd35 |
child 11800 | 5f84c687ba06 |
permissions | -rw-r--r-- |
wenzelm@10503 | 1 |
# -*- shell-script -*- |
wenzelm@2294 | 2 |
# $Id$ |
wenzelm@9818 | 3 |
# Author: Markus Wenzel, TU Muenchen |
wenzelm@9818 | 4 |
# License: GPL (GNU GENERAL PUBLIC LICENSE) |
wenzelm@2294 | 5 |
# |
wenzelm@2309 | 6 |
# Isabelle settings -- site defaults. |
wenzelm@9225 | 7 |
# Do *NOT* copy this file into your personal isabelle directory!!! |
wenzelm@2309 | 8 |
|
wenzelm@2426 | 9 |
### |
wenzelm@3177 | 10 |
### ML compiler settings (ESSENTIAL!) |
wenzelm@2426 | 11 |
### |
wenzelm@2294 | 12 |
|
wenzelm@9236 | 13 |
# Note that ML_HOME specifies the location of the actual compiler |
wenzelm@9236 | 14 |
# binaries. Do not invent new ML system names unless you know what |
wenzelm@9759 | 15 |
# you are doing. Only one of the sections below should be activated. |
wenzelm@2294 | 16 |
|
wenzelm@11569 | 17 |
# Poly/ML 3.x and 4.0 or later |
wenzelm@10205 | 18 |
if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then |
wenzelm@11569 | 19 |
#maybe a shrink-wrapped polyml-4.1.1 on x86-linux ... |
wenzelm@11569 | 20 |
ML_SYSTEM=polyml-4.1.1 |
wenzelm@10205 | 21 |
ML_PLATFORM=x86-linux |
wenzelm@10205 | 22 |
ML_HOME=/usr/bin |
wenzelm@10205 | 23 |
ML_DBASE=/usr/lib/poly/ML_dbase |
wenzelm@10205 | 24 |
ML_OPTIONS="-h 30000" |
wenzelm@10205 | 25 |
else |
wenzelm@10205 | 26 |
#... or rather a self-contained multi-platform installation |
wenzelm@10205 | 27 |
POLYML_HOME=$(choosefrom \ |
wenzelm@10205 | 28 |
"$ISABELLE_HOME/contrib/polyml" \ |
wenzelm@10205 | 29 |
"$ISABELLE_HOME/../polyml" \ |
wenzelm@10205 | 30 |
"/usr/share/polyml" \ |
wenzelm@10205 | 31 |
"/usr/local/polyml" \ |
wenzelm@10205 | 32 |
"/opt/polyml") |
wenzelm@10205 | 33 |
ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml) |
wenzelm@10503 | 34 |
ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform) |
wenzelm@10205 | 35 |
ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
wenzelm@10205 | 36 |
ML_OPTIONS="-h 30000" |
wenzelm@10205 | 37 |
fi |
wenzelm@8345 | 38 |
|
wenzelm@5708 | 39 |
# Standard ML of New Jersey 110 or later |
wenzelm@8345 | 40 |
#ML_SYSTEM=smlnj-110 |
wenzelm@9787 | 41 |
#ML_HOME="$ISABELLE_HOME/../smlnj/bin" |
wenzelm@8345 | 42 |
#ML_OPTIONS="@SMLdebug=/dev/null" |
wenzelm@9787 | 43 |
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") |
wenzelm@5708 | 44 |
|
wenzelm@11062 | 45 |
# MLWorks 2.0 |
wenzelm@11062 | 46 |
#ML_SYSTEM=mlworks |
wenzelm@11062 | 47 |
#ML_HOME="$ISABELLE_HOME/../mlworks/bin" |
wenzelm@11062 | 48 |
#ML_OPTIONS="" |
wenzelm@11062 | 49 |
#ML_PLATFORM="" |
wenzelm@11062 | 50 |
|
wenzelm@9252 | 51 |
# Moscow ML 2.00 or later (experimental!) |
wenzelm@9252 | 52 |
#ML_SYSTEM=mosml |
wenzelm@9787 | 53 |
#ML_HOME="$ISABELLE_HOME/../mosml/bin" |
wenzelm@9252 | 54 |
#ML_PLATFORM="" |
wenzelm@9252 | 55 |
#ML_OPTIONS="" |
wenzelm@9252 | 56 |
|
wenzelm@2426 | 57 |
# Standard ML of New Jersey 0.93 |
wenzelm@2426 | 58 |
#ML_SYSTEM=smlnj-0.93 |
wenzelm@2426 | 59 |
#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src |
wenzelm@2426 | 60 |
#ML_OPTIONS="" |
wenzelm@6413 | 61 |
#ML_PLATFORM="" |
wenzelm@2426 | 62 |
|
wenzelm@2426 | 63 |
|
wenzelm@2426 | 64 |
### |
wenzelm@3177 | 65 |
### Compilation options |
wenzelm@2435 | 66 |
### |
wenzelm@2435 | 67 |
|
wenzelm@11569 | 68 |
ISABELLE_USEDIR_OPTIONS="" |
wenzelm@11569 | 69 |
|
wenzelm@11569 | 70 |
# Default for precompiled distribution ... |
wenzelm@11569 | 71 |
#ISABELLE_USEDIR_OPTIONS="-i true -d pdf -p 2" |
wenzelm@2435 | 72 |
|
wenzelm@2435 | 73 |
|
wenzelm@2435 | 74 |
### |
wenzelm@7773 | 75 |
### Document preparation |
wenzelm@7773 | 76 |
### |
wenzelm@7773 | 77 |
|
wenzelm@7773 | 78 |
TEXINPUTS="$ISABELLE_HOME/lib/texinputs:$TEXINPUTS" |
wenzelm@7773 | 79 |
ISABELLE_LATEX="latex" |
wenzelm@7773 | 80 |
ISABELLE_PDFLATEX="pdflatex" |
wenzelm@7813 | 81 |
ISABELLE_BIBTEX="bibtex" |
wenzelm@7773 | 82 |
ISABELLE_DVIPS="dvips -D 600" |
wenzelm@7773 | 83 |
|
wenzelm@11062 | 84 |
# Paranoia setting ... |
wenzelm@11062 | 85 |
#unset TEXMF |
wenzelm@11062 | 86 |
|
wenzelm@7873 | 87 |
# The thumbpdf tool is probably not generally available ... |
wenzelm@11062 | 88 |
#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf" |
wenzelm@7864 | 89 |
|
wenzelm@7773 | 90 |
|
wenzelm@7773 | 91 |
### |
wenzelm@2968 | 92 |
### Misc path settings |
wenzelm@2426 | 93 |
### |
wenzelm@2426 | 94 |
|
wenzelm@2426 | 95 |
# The place for user configuration, heap files, etc. |
wenzelm@2294 | 96 |
ISABELLE_HOME_USER=~/isabelle |
wenzelm@2294 | 97 |
|
wenzelm@3177 | 98 |
# Where to look for isabelle tools (multiple dirs separated by ':'). |
wenzelm@9787 | 99 |
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" |
wenzelm@2786 | 100 |
|
wenzelm@4334 | 101 |
# Location for temporary files (should be on a local file system). |
wenzelm@9787 | 102 |
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" |
wenzelm@4334 | 103 |
|
wenzelm@2786 | 104 |
|
wenzelm@9787 | 105 |
# Heap input locations. ML system identifier is included in lookup. |
wenzelm@9787 | 106 |
ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" |
wenzelm@2786 | 107 |
|
wenzelm@9787 | 108 |
# Heap output location. ML system identifier is appended automatically later on. |
wenzelm@2780 | 109 |
if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then |
wenzelm@9787 | 110 |
#Isabelle build tells us to store heaps etc. within the distribution. |
wenzelm@9787 | 111 |
ISABELLE_OUTPUT="$ISABELLE_HOME/heaps" |
wenzelm@9787 | 112 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info" |
wenzelm@2780 | 113 |
else |
wenzelm@9787 | 114 |
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" |
wenzelm@9787 | 115 |
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" |
wenzelm@2780 | 116 |
fi |
wenzelm@2780 | 117 |
|
wenzelm@9225 | 118 |
# Site settings check -- just to make it a little bit harder to copy this file! |
wenzelm@9225 | 119 |
[ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
wenzelm@9225 | 120 |
{ echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
wenzelm@9225 | 121 |
|
wenzelm@11569 | 122 |
# Users may want to change this. |
wenzelm@3184 | 123 |
ISABELLE_LOGIC=HOL |
wenzelm@2294 | 124 |
|
wenzelm@2786 | 125 |
|
wenzelm@2786 | 126 |
## Docs |
wenzelm@2294 | 127 |
|
wenzelm@3177 | 128 |
#Where to look for docs (multiple dirs separated by ':'). |
wenzelm@9787 | 129 |
ISABELLE_DOCS="$ISABELLE_HOME/doc" |
wenzelm@2345 | 130 |
|
wenzelm@3177 | 131 |
#The dvi file viewer |
wenzelm@3062 | 132 |
DVI_VIEWER=xdvi |
wenzelm@2426 | 133 |
#DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5" |
wenzelm@11103 | 134 |
#DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7" |
wenzelm@2476 | 135 |
#DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10" |
wenzelm@3062 | 136 |
#DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9" |
wenzelm@2345 | 137 |
|
wenzelm@2294 | 138 |
|
wenzelm@3158 | 139 |
## Fonts -- how to install the Isabelle X11 fonts (can be tricky!). |
wenzelm@3158 | 140 |
|
wenzelm@3158 | 141 |
# (1) Get fonts from local (client side) directory: |
wenzelm@9787 | 142 |
ISABELLE_INSTALLFONTS="xset fp+ \"$ISABELLE_HOME/lib/fonts\"; xset fp rehash" |
wenzelm@3158 | 143 |
|
paulson@3689 | 144 |
# (2) Get from font server at Munich or Cambridge: |
wenzelm@3256 | 145 |
#ISABELLE_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
paulson@3689 | 146 |
#ISABELLE_INSTALLFONTS="xset fp+ tcp/font-serv.cl.cam.ac.uk:7100" |
wenzelm@2577 | 147 |
|
wenzelm@5964 | 148 |
|
wenzelm@2426 | 149 |
### |
wenzelm@2426 | 150 |
### Interfaces |
wenzelm@2426 | 151 |
### |
wenzelm@2426 | 152 |
|
wenzelm@2426 | 153 |
# The null interface: pass-through to 'isabelle'. |
wenzelm@11552 | 154 |
ISABELLE_INTERFACE=none |
wenzelm@2294 | 155 |
|
wenzelm@2786 | 156 |
# Simple xterm based interface. |
wenzelm@11552 | 157 |
#ISABELLE_INTERFACE=xterm |
wenzelm@5964 | 158 |
ISABELLE_XTERM_OPTIONS="" |
wenzelm@2968 | 159 |
|
wenzelm@3303 | 160 |
# Emacs running Isamode. |
wenzelm@2968 | 161 |
#ISABELLE_INTERFACE=emacs |
wenzelm@9787 | 162 |
ISAMODE_HOME="$ISABELLE_HOME/contrib/Isamode" |
wenzelm@5964 | 163 |
ISAMODE_OPTIONS="" |
wenzelm@5964 | 164 |
|
wenzelm@9679 | 165 |
# Proof General |
wenzelm@9679 | 166 |
ISABELLE_INTERFACE=$(choosefrom \ |
wenzelm@9679 | 167 |
"$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \ |
wenzelm@9679 | 168 |
"$ISABELLE_HOME/../ProofGeneral/isar/interface" \ |
wenzelm@9787 | 169 |
"/usr/share/ProofGeneral/isar/interface" \ |
wenzelm@9948 | 170 |
"/usr/local/ProofGeneral/isar/interface" \ |
wenzelm@10070 | 171 |
"/opt/ProofGeneral/isar/interface" \ |
wenzelm@9956 | 172 |
"/usr/share/emacs/ProofGeneral/isar/interface" \ |
wenzelm@9679 | 173 |
"$ISABELLE_INTERFACE") |
wenzelm@5964 | 174 |
PROOFGENERAL_OPTIONS="" |
wenzelm@7185 | 175 |
|
wenzelm@9759 | 176 |
# X-Symbol mode for Proof General |
wenzelm@9679 | 177 |
XSYMBOL_HOME=$(choosefrom \ |
wenzelm@9679 | 178 |
"$ISABELLE_HOME/contrib/x-symbol" \ |
wenzelm@9679 | 179 |
"$ISABELLE_HOME/../x-symbol" \ |
wenzelm@9787 | 180 |
"/usr/share/x-symbol" \ |
wenzelm@9948 | 181 |
"/usr/local/x-symbol" \ |
wenzelm@10070 | 182 |
"/opt/x-symbol" \ |
wenzelm@9679 | 183 |
"") |
wenzelm@11062 | 184 |
# Required for remote fonts only ... |
wenzelm@9994 | 185 |
#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200" |
wenzelm@9569 | 186 |
|
wenzelm@7185 | 187 |
|
wenzelm@7185 | 188 |
### |
wenzelm@7185 | 189 |
### External reasoning tools |
wenzelm@7185 | 190 |
### |
wenzelm@7185 | 191 |
|
wenzelm@7194 | 192 |
## Set HOME only for tools you have installed! |
wenzelm@7185 | 193 |
|
wenzelm@7185 | 194 |
# SVC (Stanford Validity Checker) |
wenzelm@7185 | 195 |
#SVC_HOME= |
wenzelm@7185 | 196 |
#SVC_MACHINE=i386-redhat-linux |
wenzelm@7185 | 197 |
#SVC_MACHINE=sparc-sun-solaris |
wenzelm@7296 | 198 |
|
wenzelm@7296 | 199 |
# Mucke (mu-calculus model checker) |
wenzelm@7296 | 200 |
#MUCKE_HOME=/usr/local/bin |
wenzelm@7296 | 201 |
|
wenzelm@7296 | 202 |
# Einhoven model checker |
wenzelm@7296 | 203 |
#EINDHOVEN_HOME=/usr/local/bin |