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