etc/settings

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.

# -*- shell-script -*- :mode=shellscript:
#
# Isabelle settings -- site defaults.
#
# Important notes:
#   * See the system manual for explanations on Isabelle settings
#   * DO NOT EDIT the repository copy of this file!
#   * DO NOT COPY this file into your personal isabelle directory!

###
### ML compiler settings (ESSENTIAL!)
###

# ML_HOME specifies the location of the actual compiler binaries.  Do
# not invent new ML system names unless you know what you are doing.
# Only one of the sections below should be activated.

# Poly/ML 4.x/5.x (automated settings)
POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
ML_HOME=$(choosefrom \
  "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
  "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
  "/usr/local/polyml/$ML_PLATFORM" \
  "/usr/share/polyml/$ML_PLATFORM" \
  "/opt/polyml/$ML_PLATFORM" \
  $POLY_HOME)
ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
ML_OPTIONS="-H 200"
ML_DBASE=""

# Poly/ML 5.1
#ML_PLATFORM=x86-linux
#ML_HOME=/usr/local/polyml/x86-linux
#ML_SYSTEM=polyml-5.1
#ML_OPTIONS="-H 500"

# Poly/ML 5.1 (64 bit)
#ML_PLATFORM=x86_64-linux
#ML_HOME=/usr/local/polyml/x86_64-linux
#ML_SYSTEM=polyml-5.1
#ML_OPTIONS="-H 1000"

# Poly/ML 4.2.0
#ML_PLATFORM=x86-linux
#ML_HOME=/usr/local/polyml/x86-linux
#ML_SYSTEM=polyml-4.2.0
#ML_OPTIONS="-H 80"

# Standard ML of New Jersey (slow!)
#ML_SYSTEM=smlnj-110
#ML_HOME="/usr/local/smlnj/bin"
#ML_OPTIONS="@SMLdebug=/dev/null"
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
#SMLNJ_CYGWIN_RUNTIME=1

# Moscow ML 2.00 (experimental!)
#ML_SYSTEM=mosml
#ML_HOME="/usr/local/mosml/bin"
#ML_OPTIONS=""
#ML_PLATFORM=""

# Alice 1.4 (experimental!)
#ML_SYSTEM=alice
#ML_HOME="/usr/local/alice/bin"
#ML_OPTIONS=""
#ML_PLATFORM=""


###
### JVM components (Scala or Java)
###

ISABELLE_SCALA="scala"
ISABELLE_JAVA="java"

if [ -e "$ISABELLE_HOME/contrib/scala" ]; then
  classpath "$ISABELLE_HOME/contrib/scala/lib/scala-library.jar"
elif [ -e "$ISABELLE_HOME/../scala" ]; then
  classpath "$ISABELLE_HOME/../scala/lib/scala-library.jar"
fi

classpath "$ISABELLE_HOME/lib/classes/Pure.jar"


###
### Interactive sessions (cf. isabelle tty)
###

ISABELLE_LINE_EDITOR=""
[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"


###
### Batch sessions (cf. isabelle usedir)
###

ISABELLE_USEDIR_OPTIONS="-M max -p 1 -v true -V outline=/proof,/ML"

# Specifically for the HOL image
HOL_USEDIR_OPTIONS=""
#HOL_USEDIR_OPTIONS="-p 2"

#Source file identification (default: full name + date stamp)
ISABELLE_FILE_IDENT=""
#ISABELLE_FILE_IDENT="md5"
#ISABELLE_FILE_IDENT="md5sum"
#ISABELLE_FILE_IDENT="sha1sum"
#ISABELLE_FILE_IDENT="openssl dgst -sha1"


###
### Document preparation (cf. isabelle latex/document)
###

ISABELLE_LATEX="latex"
ISABELLE_PDFLATEX="pdflatex"
ISABELLE_BIBTEX="bibtex"
ISABELLE_MAKEINDEX="makeindex"
ISABELLE_DVIPS="dvips -D 600"
ISABELLE_EPSTOPDF="epstopdf"

# Paranoia setting for strange latex installations ...
#unset TEXMF


###
### Misc path settings
###

# The place for user configuration, heap files, etc.
ISABELLE_HOME_USER=~/.isabelle

# Where to look for isabelle tools (multiple dirs separated by ':').
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"

# Location for temporary files (should be on a local file system).
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"

# Heap input locations. ML system identifier is included in lookup.
ISABELLE_PATH="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER:$ISABELLE_HOME/heaps"

# Heap output location. ML system identifier is appended automatically later on.
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps/$ISABELLE_IDENTIFIER"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"

# Site settings check -- just to make it a little bit harder to copy this file verbatim!
[ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
  { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }


###
### Default logic
###

ISABELLE_LOGIC=HOL


###
### Docs
###

# Where to look for docs (multiple dirs separated by ':').
ISABELLE_DOCS="$ISABELLE_HOME/doc"

# Preferred document format
ISABELLE_DOC_FORMAT=pdf

# The dvi file viewer
DVI_VIEWER=xdvi
#DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
#DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7"
#DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
#DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"

# The pdf file viewer
if [ $(uname -s) = Darwin ]; then
  PDF_VIEWER=open
else
  PDF_VIEWER=xpdf
fi
#PDF_VIEWER=acroread
#PDF_VIEWER=evince


# Printer spool command for PS files
PRINT_COMMAND=lp


###
### Proof General / Emacs
###

# Proof General home, look in a variety of places
PROOFGENERAL_HOME=$(choosefrom \
  "$ISABELLE_HOME/contrib/ProofGeneral" \
  "$ISABELLE_HOME/../ProofGeneral" \
  "/usr/local/ProofGeneral" \
  "/usr/share/ProofGeneral" \
  "/opt/ProofGeneral" \
  "")

PROOFGENERAL_OPTIONS=""
#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets"

# Automatic setup of remote fonts
#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
XSYMBOL_INSTALLFONTS=""


###
### jEdit
###

JEDIT_HOME=$(choosefrom \
  "$ISABELLE_HOME/contrib/jedit" \
  "$ISABELLE_HOME/../jedit" \
  "/usr/local/jedit" \
  "/usr/share/jedit" \
  "/opt/jedit" \
  "")

JEDIT_JAVA_OPTIONS=""
#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m"
JEDIT_OPTIONS="-reuseview -noserver -nobackground"


###
### External reasoning tools
###

## Set HOME only for tools you have installed!

# External provers
E_HOME=$(choosefrom \
  "$ISABELLE_HOME/contrib/E/$ML_PLATFORM" \
  "$ISABELLE_HOME/../E/$ML_PLATFORM" \
  "/usr/local/E" \
  "")
VAMPIRE_HOME=$(choosefrom \
  "$ISABELLE_HOME/contrib/vampire/$ML_PLATFORM" \
  "$ISABELLE_HOME/../vampire/$ML_PLATFORM" \
  "/usr/local/Vampire" \
  "")
SPASS_HOME=$(choosefrom \
  "$ISABELLE_HOME/contrib/spass/$ML_PLATFORM/bin" \
  "$ISABELLE_HOME/../spass/$ML_PLATFORM/bin" \
  "/usr/local/SPASS" \
  "")

# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
#HOL4_PROOFS="$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"

# SVC (Stanford Validity Checker)
#SVC_HOME=
#SVC_MACHINE=i386-redhat-linux
#SVC_MACHINE=sparc-sun-solaris

# Mucke (mu-calculus model checker)
#MUCKE_HOME=/usr/local/bin

# Einhoven model checker
#EINDHOVEN_HOME=/usr/local/bin

# MiniSat 1.14 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
#MINISAT_HOME=/usr/local/bin

# zChaff (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
#ZCHAFF_HOME=/usr/local/bin

# BerkMin561 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
#BERKMIN_HOME=/usr/local/bin
#BERKMIN_EXE=BerkMin561-linux
#BERKMIN_EXE=BerkMin561-solaris

# Jerusat 1.3 (SAT Solver, cf. Isabelle/src/HOL/Tools/sat_solver.ML)
#JERUSAT_HOME=/usr/local/bin

# For configuring HOL/Matrix/cplex
# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
# First option: use the commercial cplex solver
#LP_SOLVER=CPLEX
#CPLEX_PATH=cplex
# Second option: use the open source glpk solver
#LP_SOLVER=GLPK
#GLPK_PATH=glpsol