polyml: use polyml-platform/version from Isabelle distribution;
authorwenzelm
Mon Aug 01 19:20:21 2005 +0200 (2005-08-01)
changeset 169685cb40c8b1f10
parent 16967 40759607c590
child 16969 e26915e01d15
polyml: use polyml-platform/version from Isabelle distribution;
removed DEFS_CHAIN_HISTORY;
etc/settings
     1.1 --- a/etc/settings	Mon Aug 01 14:40:21 2005 +0200
     1.2 +++ b/etc/settings	Mon Aug 01 19:20:21 2005 +0200
     1.3 @@ -12,41 +12,22 @@
     1.4  ### ML compiler settings (ESSENTIAL!)
     1.5  ###
     1.6  
     1.7 -# Note that ML_HOME specifies the location of the actual compiler
     1.8 -# binaries.  Do not invent new ML system names unless you know what
     1.9 -# you are doing.  Only one of the sections below should be activated.
    1.10 -
    1.11 -# try finding the poly packages from the Isabelle site in the usual places
    1.12 -POLYML_HOME=$(choosefrom \
    1.13 -  "$ISABELLE_HOME/contrib/polyml" \
    1.14 -  "$ISABELLE_HOME/../polyml" \
    1.15 -  "/usr/share/polyml" \
    1.16 -  "/usr/local/polyml" \
    1.17 -  "/opt/polyml")
    1.18 +# ML_HOME specifies the location of the actual compiler binaries.  Do
    1.19 +# not invent new ML system names unless you know what you are doing.
    1.20 +# Only one of the sections below should be activated.
    1.21  
    1.22 -if [ -n "$POLYML_HOME" -a -e "$POLYML_HOME/bin/polyml-version" ]; then
    1.23 -  # looks like Isabelle poly packages
    1.24 -  ML_SYSTEM=$("$POLYML_HOME/bin/polyml-version" 2>/dev/null || echo polyml)
    1.25 -  ML_PLATFORM=$("$POLYML_HOME/bin/polyml-platform" 2>/dev/null || echo unknown-platform)
    1.26 -  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    1.27 -  ML_OPTIONS="-h 15000"
    1.28 -elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
    1.29 -  # maybe a shrink-wrapped polyml on x86-linux ...
    1.30 -
    1.31 -  # Poly/ML 4.0, 4.1, 4.1.x
    1.32 -  # include version number, needed for choosing right options
    1.33 -  # If automatic setting doesn't work, use e.g. ML_VERSION=4.1.3
    1.34 -  ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p')
    1.35 -  ML_SYSTEM=polyml-${ML_VERSION}
    1.36 -  # processor/OS type
    1.37 -  ML_PLATFORM=x86-linux
    1.38 -  # where to find binaries
    1.39 -  ML_HOME=/usr/bin
    1.40 -  # where to find the standard database
    1.41 -  ML_DBASE=/usr/lib/poly/ML_dbase
    1.42 -  # options to pass to poly
    1.43 -  ML_OPTIONS="-h 15000"
    1.44 -fi
    1.45 +# Poly/ML 4.x
    1.46 +POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
    1.47 +ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
    1.48 +ML_HOME=$(choosefrom \
    1.49 +  "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
    1.50 +  "$ISABELLE_HOME/../polyml/$ML_PLATFORM" \
    1.51 +  "/usr/share/polyml/$ML_PLATFORM" \
    1.52 +  "/usr/local/polyml/$ML_PLATFORM" \
    1.53 +  "/opt/polyml/$ML_PLATFORM" \
    1.54 +  $POLY_HOME)
    1.55 +ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
    1.56 +ML_OPTIONS="-h 50000"
    1.57  
    1.58  # Standard ML of New Jersey 110 or later
    1.59  #SMLNJ_CYGWIN_RUNTIME=1
    1.60 @@ -159,8 +140,6 @@
    1.61  ### Interfaces
    1.62  ###
    1.63  
    1.64 -# ISABELLE_INTERFACE is the program which is run by the Isabelle command
    1.65 -
    1.66  # Fallback: the null interface (pass-through to raw isabelle process).
    1.67  ISABELLE_INTERFACE=none
    1.68  
    1.69 @@ -174,7 +153,6 @@
    1.70    "/usr/share/emacs/ProofGeneral/isar/interface" \
    1.71    "$ISABELLE_INTERFACE")
    1.72  
    1.73 -# Options to pass to Isabelle command when PG is selected as interface
    1.74  PROOFGENERAL_OPTIONS=""
    1.75  #PROOFGENERAL_OPTIONS="-m no_brackets -m no_type_brackets -x true"
    1.76  
    1.77 @@ -221,11 +199,8 @@
    1.78  # For configuring HOL/Matrix/cplex
    1.79  # LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
    1.80  # First option: use the commercial cplex solver
    1.81 -# LP_SOLVER=CPLEX
    1.82 -# CPLEX_PATH=cplex
    1.83 +#LP_SOLVER=CPLEX
    1.84 +#CPLEX_PATH=cplex
    1.85  # Second option: use the open source glpk solver
    1.86 -# LP_SOLVER=GLPK
    1.87 -# GLPK_PATH=glpsol
    1.88 -
    1.89 -# toogles the detail of the error message in case of a cyclic definition
    1.90 -DEFS_CHAIN_HISTORY=ON
    1.91 +#LP_SOLVER=GLPK
    1.92 +#GLPK_PATH=glpsol