etc/settings
author obua
Mon Aug 01 11:39:33 2005 +0200 (2005-08-01)
changeset 16966 37e34f315057
parent 16875 c62bdfbf6a2a
child 16968 5cb40c8b1f10
permissions -rw-r--r--
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
wenzelm@10503
     1
# -*- shell-script -*-
wenzelm@2294
     2
# $Id$
wenzelm@2294
     3
#
wenzelm@2309
     4
# Isabelle settings -- site defaults.
wenzelm@16875
     5
#
wenzelm@16875
     6
# Important notes:
wenzelm@16875
     7
#   * See the system manual for explanations on Isabelle settings
wenzelm@16875
     8
#   * DO NOT EDIT the repository copy of this file!
wenzelm@16875
     9
#   * DO NOT COPY this file into your personal isabelle directory!
wenzelm@2309
    10
wenzelm@2426
    11
###
wenzelm@3177
    12
### ML compiler settings (ESSENTIAL!)
wenzelm@2426
    13
###
wenzelm@2426
    14
wenzelm@9236
    15
# Note that ML_HOME specifies the location of the actual compiler
wenzelm@9236
    16
# binaries.  Do not invent new ML system names unless you know what
wenzelm@9759
    17
# you are doing.  Only one of the sections below should be activated.
wenzelm@2426
    18
kleing@14461
    19
# try finding the poly packages from the Isabelle site in the usual places
kleing@14461
    20
POLYML_HOME=$(choosefrom \
kleing@14461
    21
  "$ISABELLE_HOME/contrib/polyml" \
kleing@14461
    22
  "$ISABELLE_HOME/../polyml" \
kleing@14461
    23
  "/usr/share/polyml" \
kleing@14461
    24
  "/usr/local/polyml" \
kleing@14461
    25
  "/opt/polyml")
kleing@14447
    26
kleing@14461
    27
if [ -n "$POLYML_HOME" -a -e "$POLYML_HOME/bin/polyml-version" ]; then
kleing@14461
    28
  # looks like Isabelle poly packages
kleing@14461
    29
  ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
kleing@14461
    30
  ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
kleing@14461
    31
  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
kleing@14461
    32
  ML_OPTIONS="-h 15000"
kleing@14461
    33
elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
kleing@14461
    34
  # maybe a shrink-wrapped polyml on x86-linux ...
kleing@14461
    35
kleing@14613
    36
  # Poly/ML 4.0, 4.1, 4.1.x
kleing@14447
    37
  # include version number, needed for choosing right options
aspinall@15734
    38
  # If automatic setting doesn't work, use e.g. ML_VERSION=4.1.3
gagern@15865
    39
  ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p')
aspinall@15734
    40
  ML_SYSTEM=polyml-${ML_VERSION}
kleing@14447
    41
  # processor/OS type
wenzelm@10205
    42
  ML_PLATFORM=x86-linux
kleing@14447
    43
  # where to find binaries
wenzelm@10205
    44
  ML_HOME=/usr/bin
kleing@14447
    45
  # where to find the standard database
wenzelm@10205
    46
  ML_DBASE=/usr/lib/poly/ML_dbase
kleing@14447
    47
  # options to pass to poly
wenzelm@12752
    48
  ML_OPTIONS="-h 15000"
wenzelm@10205
    49
fi
wenzelm@8345
    50
wenzelm@5708
    51
# Standard ML of New Jersey 110 or later
wenzelm@16250
    52
#SMLNJ_CYGWIN_RUNTIME=1
wenzelm@8345
    53
#ML_SYSTEM=smlnj-110
wenzelm@15846
    54
#ML_HOME="$ISABELLE_HOME/contrib/smlnj/bin"
wenzelm@8345
    55
#ML_OPTIONS="@SMLdebug=/dev/null"
wenzelm@9787
    56
#ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
wenzelm@5708
    57
wenzelm@9252
    58
# Moscow ML 2.00 or later (experimental!)
wenzelm@9252
    59
#ML_SYSTEM=mosml
wenzelm@15846
    60
#ML_HOME="$ISABELLE_HOME/contrib/mosml/bin"
wenzelm@6413
    61
#ML_PLATFORM=""
wenzelm@9252
    62
#ML_OPTIONS=""
wenzelm@5708
    63
wenzelm@2294
    64
wenzelm@2426
    65
###
wenzelm@16186
    66
### Compilation options (cf. isatool usedir)
wenzelm@2435
    67
###
wenzelm@2435
    68
wenzelm@16875
    69
ISABELLE_USEDIR_OPTIONS="-v true"
wenzelm@11569
    70
wenzelm@16186
    71
# Specifically for the HOL image
wenzelm@16186
    72
HOL_USEDIR_OPTIONS=""
kleing@14044
    73
wenzelm@2435
    74
wenzelm@2435
    75
###
wenzelm@16186
    76
### Document preparation (cf. isatool latex/document)
wenzelm@7773
    77
###
wenzelm@7773
    78
wenzelm@7773
    79
ISABELLE_LATEX="latex"
wenzelm@7773
    80
ISABELLE_PDFLATEX="pdflatex"
wenzelm@7813
    81
ISABELLE_BIBTEX="bibtex"
kleing@14344
    82
ISABELLE_MAKEINDEX="makeindex"
wenzelm@7773
    83
ISABELLE_DVIPS="dvips -D 600"
wenzelm@11800
    84
ISABELLE_EPSTOPDF="epstopdf"
wenzelm@7773
    85
kleing@13920
    86
# Paranoia setting for strange latex installations ...
wenzelm@11062
    87
#unset TEXMF
wenzelm@11062
    88
kleing@13920
    89
# If ISABELLE_THUMBPDF is set, isatool tries to
kleing@13920
    90
# generate thumbnails for proof documents
wenzelm@11062
    91
#type -path thumbpdf >/dev/null && ISABELLE_THUMBPDF="thumbpdf"
wenzelm@7864
    92
wenzelm@7773
    93
wenzelm@7773
    94
###
wenzelm@2968
    95
### Misc path settings
wenzelm@2426
    96
###
wenzelm@2294
    97
wenzelm@2426
    98
# The place for user configuration, heap files, etc.
wenzelm@2426
    99
ISABELLE_HOME_USER=~/isabelle
wenzelm@2294
   100
wenzelm@3177
   101
# Where to look for isabelle tools (multiple dirs separated by ':').
wenzelm@9787
   102
ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
wenzelm@2786
   103
wenzelm@4334
   104
# Location for temporary files (should be on a local file system).
wenzelm@9787
   105
ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER"
wenzelm@4334
   106
wenzelm@9787
   107
# Heap input locations. ML system identifier is included in lookup.
wenzelm@9787
   108
ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps"
wenzelm@2780
   109
wenzelm@9787
   110
# Heap output location. ML system identifier is appended automatically later on.
wenzelm@15846
   111
if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
wenzelm@15846
   112
  #Isabelle build tells us to store heaps etc. within the distribution.
wenzelm@15846
   113
  ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
wenzelm@15846
   114
  ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
wenzelm@15846
   115
else
wenzelm@9787
   116
  ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps"
wenzelm@9787
   117
  ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
wenzelm@15846
   118
fi
wenzelm@2780
   119
wenzelm@16186
   120
# Site settings check -- just to make it a little bit harder to copy this file verbatim!
wenzelm@9225
   121
[ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
wenzelm@9225
   122
  { echo >&2 "### Isabelle site settings already present!  Maybe copied etc/settings in full?"; }
wenzelm@9225
   123
kleing@13920
   124
kleing@13920
   125
###
wenzelm@16875
   126
### default logic
kleing@13920
   127
###
wenzelm@16186
   128
wenzelm@3184
   129
ISABELLE_LOGIC=HOL
wenzelm@2294
   130
wenzelm@2786
   131
kleing@13920
   132
###
kleing@13920
   133
### Docs
kleing@13920
   134
###
wenzelm@2294
   135
wenzelm@16186
   136
# Where to look for docs (multiple dirs separated by ':').
wenzelm@9787
   137
ISABELLE_DOCS="$ISABELLE_HOME/doc"
wenzelm@2345
   138
wenzelm@16186
   139
# Preferred document format
wenzelm@15703
   140
ISABELLE_DOC_FORMAT=pdf
wenzelm@15703
   141
wenzelm@16186
   142
# The dvi file viewer
wenzelm@3062
   143
DVI_VIEWER=xdvi
wenzelm@2426
   144
#DVI_VIEWER="xdvi -geometry 498x704 -expert -s 5"
wenzelm@11103
   145
#DVI_VIEWER="xdvi -geometry 711x1005 -expert -s 7"
wenzelm@2476
   146
#DVI_VIEWER="xdvi -geometry 500x704 -expert -s 10"
wenzelm@3062
   147
#DVI_VIEWER="xdvi -geometry 555x782 -expert -s 9"
wenzelm@2345
   148
wenzelm@16186
   149
# The pdf file viewer
kleing@15218
   150
PDF_VIEWER=acroread
kleing@15218
   151
#PDF_VIEWER=xpdf
wenzelm@16186
   152
#PDF_VIEWER=open  #best for Mac users: will open in default PDF viewer
kleing@15218
   153
wenzelm@16186
   154
# Printer spool command for PS files
wenzelm@14933
   155
PRINT_COMMAND=lp
wenzelm@14933
   156
wenzelm@2294
   157
wenzelm@2426
   158
###
wenzelm@2426
   159
### Interfaces
wenzelm@2426
   160
###
wenzelm@2426
   161
kleing@13920
   162
# ISABELLE_INTERFACE is the program which is run by the Isabelle command
kleing@13920
   163
kleing@13920
   164
# Fallback: the null interface (pass-through to raw isabelle process).
wenzelm@11552
   165
ISABELLE_INTERFACE=none
wenzelm@2294
   166
kleing@13920
   167
# Proof General path, look in a variety of places
quigley@15779
   168
ISABELLE_INTERFACE=$(choosefrom\
wenzelm@9679
   169
  "$ISABELLE_HOME/contrib/ProofGeneral/isar/interface" \
wenzelm@9679
   170
  "$ISABELLE_HOME/../ProofGeneral/isar/interface" \
wenzelm@9787
   171
  "/usr/share/ProofGeneral/isar/interface" \
wenzelm@9948
   172
  "/usr/local/ProofGeneral/isar/interface" \
wenzelm@10070
   173
  "/opt/ProofGeneral/isar/interface" \
wenzelm@9956
   174
  "/usr/share/emacs/ProofGeneral/isar/interface" \
wenzelm@9679
   175
  "$ISABELLE_INTERFACE")
kleing@13920
   176
kleing@13920
   177
# Options to pass to Isabelle command when PG is selected as interface
wenzelm@5964
   178
PROOFGENERAL_OPTIONS=""
wenzelm@11981
   179
#PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true"
wenzelm@7185
   180
wenzelm@16875
   181
type -path xemacs >/dev/null || \
wenzelm@16875
   182
  PROOFGENERAL_OPTIONS="-p emacs $PROOFGENERAL_OPTIONS"
wenzelm@12476
   183
wenzelm@16875
   184
# Executed before xemacs with ProofGeneral is called; required for remote fonts.
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
webertj@14451
   204
webertj@15331
   205
# zChaff (SAT Solver)
webertj@15284
   206
#ZCHAFF_HOME=/usr/local/bin
webertj@15331
   207
#ZCHAFF_VERSION=2004.5.13
webertj@15331
   208
#ZCHAFF_VERSION=2004.11.15
webertj@14942
   209
webertj@14942
   210
# BerkMin561 (SAT Solver)
webertj@14942
   211
#BERKMIN_HOME=/usr/local/bin
webertj@14942
   212
#BERKMIN_EXE=BerkMin561-linux
webertj@14942
   213
#BERKMIN_EXE=BerkMin561-solaris
webertj@14943
   214
webertj@14943
   215
# Jerusat 1.3 (SAT Solver)
webertj@14943
   216
#JERUSAT_HOME=/usr/local/bin
wenzelm@16419
   217
wenzelm@16419
   218
# HOL4 proof objects (cf. Isabelle/src/HOL/Import)
wenzelm@16419
   219
HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
obua@16873
   220
obua@16873
   221
# For configuring HOL/Matrix/cplex
obua@16966
   222
# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
obua@16873
   223
# First option: use the commercial cplex solver
obua@16966
   224
# LP_SOLVER=CPLEX
obua@16966
   225
# CPLEX_PATH=cplex
obua@16873
   226
# Second option: use the open source glpk solver
obua@16966
   227
# LP_SOLVER=GLPK
obua@16966
   228
# GLPK_PATH=glpsol
obua@16966
   229
obua@16966
   230
# toogles the detail of the error message in case of a cyclic definition
obua@16966
   231
DEFS_CHAIN_HISTORY=ON