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