Eliminated ZCHAFF_VERSION configuration variable, since zChaff's output format is identical in all versions since March 2003 (at least), and also because it forces users who want to use the latest versions to lie about the version number.
I also made the BERKMIN_EXE variable optional, defaulting to BerkMin561 (a reasonable name with no platform encoded in it).
These changes have no inpacts on already working Isabelle installations.
1 # -*- shell-script -*- :mode=shellscript:
3 # Isabelle settings -- site defaults.
6 # * See the system manual for explanations on Isabelle settings
7 # * DO NOT EDIT the repository copy of this file!
8 # * DO NOT COPY this file into your personal isabelle directory!
11 ### ML compiler settings (ESSENTIAL!)
14 # ML_HOME specifies the location of the actual compiler binaries. Do
15 # not invent new ML system names unless you know what you are doing.
16 # Only one of the sections below should be activated.
18 # Poly/ML 4.x/5.x (automated settings)
19 POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
20 ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
21 ML_HOME=$(choosefrom \
22 "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
23 "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
24 "/usr/local/polyml/$ML_PLATFORM" \
25 "/usr/share/polyml/$ML_PLATFORM" \
26 "/opt/polyml/$ML_PLATFORM" \
28 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
33 #ML_PLATFORM=x86-linux
34 #ML_HOME=/usr/local/polyml/x86-linux
38 # Poly/ML 5.1 (64 bit)
39 #ML_PLATFORM=x86_64-linux
40 #ML_HOME=/usr/local/polyml/x86_64-linux
45 #ML_PLATFORM=x86-linux
46 #ML_HOME=/usr/local/polyml/x86-linux
47 #ML_SYSTEM=polyml-4.2.0
50 # Standard ML of New Jersey (slow!)
52 #ML_HOME="/usr/local/smlnj/bin"
53 #ML_OPTIONS="@SMLdebug=/dev/null"
54 #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
55 #SMLNJ_CYGWIN_RUNTIME=1
57 # Moscow ML 2.00 (experimental!)
59 #ML_HOME="/usr/local/mosml/bin"
63 # Alice 1.4 (experimental!)
65 #ML_HOME="/usr/local/alice/bin"
71 ### JVM components (Scala or Java)
74 ISABELLE_SCALA="scala"
77 if [ -e "$ISABELLE_HOME/contrib/scala" ]; then
78 classpath "$ISABELLE_HOME/contrib/scala/lib/scala-library.jar"
79 elif [ -e "$ISABELLE_HOME/../scala" ]; then
80 classpath "$ISABELLE_HOME/../scala/lib/scala-library.jar"
83 classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
87 ### Interactive sessions (cf. isabelle tty)
90 ISABELLE_LINE_EDITOR=""
91 [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
92 [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
96 ### Batch sessions (cf. isabelle usedir)
99 ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"
101 # Specifically for the HOL image
102 HOL_USEDIR_OPTIONS=""
103 #HOL_USEDIR_OPTIONS="-p 2"
105 #Source file identification (default: full name + date stamp)
106 ISABELLE_FILE_IDENT=""
107 #ISABELLE_FILE_IDENT="md5"
108 #ISABELLE_FILE_IDENT="md5sum"
109 #ISABELLE_FILE_IDENT="sha1sum"
110 #ISABELLE_FILE_IDENT="openssl dgst -sha1"
114 ### Document preparation (cf. isabelle latex/document)
117 ISABELLE_LATEX="latex"
118 ISABELLE_PDFLATEX="pdflatex"
119 ISABELLE_BIBTEX="bibtex"
120 ISABELLE_MAKEINDEX="makeindex"
121 ISABELLE_DVIPS="dvips -D 600"
122 ISABELLE_EPSTOPDF="epstopdf"
124 # Paranoia setting for strange latex installations ...
129 ### Misc path settings
132 # The place for user configuration, heap files, etc.
133 ISABELLE_HOME_USER=~/.isabelle
135 # Where to look for isabelle tools (multiple dirs separated by ':').
136 ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
138 # Location for temporary files (should be on a local file system).
139 ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
141 # Heap input locations. ML system identifier is included in lookup.
142 ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps"
144 # Heap output location. ML system identifier is appended automatically later on.
145 ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER"
146 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
148 # Site settings check -- just to make it a little bit harder to copy this file verbatim!
149 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
150 { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; }
164 # Where to look for docs (multiple dirs separated by ':').
165 ISABELLE_DOCS="$ISABELLE_HOME/doc"
167 # Preferred document format
168 ISABELLE_DOC_FORMAT=pdf
170 # The dvi file viewer
172 #DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
173 #DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7"
174 #DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
175 #DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
177 # The pdf file viewer
178 if [ $(uname -s) = Darwin ]; then
187 # Printer spool command for PS files
192 ### Proof General / Emacs
195 # Proof General home, look in a variety of places
196 PROOFGENERAL_HOME=$(choosefrom \
197 "$ISABELLE_HOME/contrib/ProofGeneral" \
198 "$ISABELLE_HOME/../ProofGeneral" \
199 "/usr/local/ProofGeneral" \
200 "/usr/share/ProofGeneral" \
201 "/opt/ProofGeneral" \
204 PROOFGENERAL_OPTIONS=""
205 #PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"
207 # Automatic setup of remote fonts
208 #XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
209 XSYMBOL_INSTALLFONTS=""
216 JEDIT_HOME=$(choosefrom \
217 "$ISABELLE_HOME/contrib/jedit" \
218 "$ISABELLE_HOME/../jedit" \
224 JEDIT_JAVA_OPTIONS=""
225 #JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m"
226 JEDIT_OPTIONS="-reuseview -noserver -nobackground"
230 ### External reasoning tools
233 ## Set HOME only for tools you have installed!
236 E_HOME=$(choosefrom \
237 "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \
238 "$ISABELLE_HOME/../E/$ML_PLATFORM" \
241 VAMPIRE_HOME=$(choosefrom \
242 "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
243 "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
244 "/usr/local/Vampire" \
246 SPASS_HOME=$(choosefrom \
247 "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \
248 "$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \
252 # HOL4 proof objects (cf. Isabelle/src/HOL/Import)
253 #HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
255 # SVC (Stanford Validity Checker)
257 #SVC_MACHINE=i386-redhat-linux
258 #SVC_MACHINE=sparc-sun-solaris
260 # Mucke (mu-calculus model checker)
261 #MUCKE_HOME=/usr/local/bin
263 # Einhoven model checker
264 #EINDHOVEN_HOME=/usr/local/bin
266 # MiniSat 1.14 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
267 #MINISAT_HOME=/usr/local/bin
269 # zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
270 #ZCHAFF_HOME=/usr/local/bin
272 # BerkMin561 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
273 #BERKMIN_HOME=/usr/local/bin
274 #BERKMIN_EXE=BerkMin561-linux
275 #BERKMIN_EXE=BerkMin561-solaris
277 # Jerusat 1.3 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
278 #JERUSAT_HOME=/usr/local/bin
280 # For configuring HOL/Matrix/cplex
281 # LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
282 # First option: use the commercial cplex solver
285 # Second option: use the open source glpk solver