1. changed configuration variables for linear programming (Cplex_tools):
LP_SOLVER is either CPLEX or GLPK
CPLEX_PATH is the path to the cplex binary
GLPK_PATH is the path to the glpk binary
The change makes it possible to switch between glpk and cplex at runtime.
2. moved conflicting list theories out of Library.thy into ROOT.ML
# -*- shell-script -*-
# $Id$
#
# 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!)
###
# Note that 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.
# try finding the poly packages from the Isabelle site in the usual places
POLYML_HOME=$(choosefrom \
"$ISABELLE_HOME/contrib/polyml" \
"$ISABELLE_HOME/../polyml" \
"/usr/share/polyml" \
"/usr/local/polyml" \
"/opt/polyml")
if [ -n "$POLYML_HOME" -a -e "$POLYML_HOME/bin/polyml-version" ]; then
# looks like Isabelle poly packages
ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-h 15000"
elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
# maybe a shrink-wrapped polyml on x86-linux ...
# Poly/ML 4.0, 4.1, 4.1.x
# include version number, needed for choosing right options
# If automatic setting doesn't work, use e.g. ML_VERSION=4.1.3
ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p')
ML_SYSTEM=polyml-${ML_VERSION}
# processor/OS type
ML_PLATFORM=x86-linux
# where to find binaries
ML_HOME=/usr/bin
# where to find the standard database
ML_DBASE=/usr/lib/poly/ML_dbase
# options to pass to poly
ML_OPTIONS="-h 15000"
fi
# Standard ML of New Jersey 110 or later
#SMLNJ_CYGWIN_RUNTIME=1
#ML_SYSTEM=smlnj-110
#ML_HOME="$ISABELLE_HOME/contrib/smlnj/bin"
#ML_OPTIONS="@SMLdebug=/dev/null"
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
# Moscow ML 2.00 or later (experimental!)
#ML_SYSTEM=mosml
#ML_HOME="$ISABELLE_HOME/contrib/mosml/bin"
#ML_PLATFORM=""
#ML_OPTIONS=""
###
### Compilation options (cf. isatool usedir)
###
ISABELLE_USEDIR_OPTIONS="-v true"
# Specifically for the HOL image
HOL_USEDIR_OPTIONS=""
###
### Document preparation (cf. isatool 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
# If ISABELLE_THUMBPDF is set, isatool tries to
# generate thumbnails for proof documents
#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf"
###
### 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_HOME/heaps"
# Heap output location. ML system identifier is appended automatically later on.
if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
#Isabelle build tells us to store heaps etc. within the distribution.
ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
else
ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
fi
# 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
PDF_VIEWER=acroread
#PDF_VIEWER=xpdf
#PDF_VIEWER=open #best for Mac users: will open in default PDF viewer
# Printer spool command for PS files
PRINT_COMMAND=lp
###
### Interfaces
###
# ISABELLE_INTERFACE is the program which is run by the Isabelle command
# Fallback: the null interface (pass-through to raw isabelle process).
ISABELLE_INTERFACE=none
# Proof General path, look in a variety of places
ISABELLE_INTERFACE=$(choosefrom\
"$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \
"$ISABELLE_HOME/../ProofGeneral/isar/interface" \
"/usr/share/ProofGeneral/isar/interface" \
"/usr/local/ProofGeneral/isar/interface" \
"/opt/ProofGeneral/isar/interface" \
"/usr/share/emacs/ProofGeneral/isar/interface" \
"$ISABELLE_INTERFACE")
# Options to pass to Isabelle command when PG is selected as interface
PROOFGENERAL_OPTIONS=""
#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true"
type -path xemacs >/dev/null || \
PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS"
# Executed before xemacs with ProofGeneral is called; required for remote fonts.
#XSYMBOL_INSTALLFONTS="xset fp+ tcp/isafonts.informatik.tu-muenchen.de:7200"
###
### External reasoning tools
###
## Set HOME only for tools you have installed!
# 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
# zChaff (SAT Solver)
#ZCHAFF_HOME=/usr/local/bin
#ZCHAFF_VERSION=2004.5.13
#ZCHAFF_VERSION=2004.11.15
# BerkMin561 (SAT Solver)
#BERKMIN_HOME=/usr/local/bin
#BERKMIN_EXE=BerkMin561-linux
#BERKMIN_EXE=BerkMin561-solaris
# Jerusat 1.3 (SAT Solver)
#JERUSAT_HOME=/usr/local/bin
# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
# 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
# toogles the detail of the error message in case of a cyclic definition
DEFS_CHAIN_HISTORY=ON