lib/Tools/install

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

#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: install standalone Isabelle executables


PRG=$(basename "$0")

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS]"
  echo
  echo "  Options are:"
  echo "    -d DISTDIR   refer to DISTDIR as Isabelle distribution"
  echo "                 (default ISABELLE_HOME)"
  echo "    -p DIR       install standalone binaries in DIR"
  echo
  echo "  Install Isabelle executables with absolute references to the current"
  echo "  distribution directory."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}


## process command line

# options

NO_OPTS=true

DISTDIR="$ISABELLE_HOME"
BINDIR=""

while getopts "d:p:" OPT
do
  NO_OPTS=""
  case "$OPT" in
    d)
      DISTDIR="$OPTARG"
      ;;
    p)
      BINDIR="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

[ "$#" -ne 0 -o -n "$NO_OPTS" ] && usage


## main

echo "referring to distribution at $DISTDIR"


# standalone binaries

#set by configure
AUTO_BASH=bash

case "$AUTO_BASH" in
  /*)
    BASH="$AUTO_BASH"
    ;;
  *)
    BASH="/usr/bin/env bash"
    ;;
esac

if [ -n "$BINDIR" ]; then
  mkdir -p "$BINDIR" || fail "Bad directory: $BINDIR"

  for NAME in isatool isabelle-process isabelle-interface
  do
    BIN="$BINDIR/$NAME"
    DIST="$DISTDIR/bin/$NAME"
    echo "installing $BIN"
    rm -f "$BIN"
    echo "#!$BASH" > "$BIN" || fail "Cannot write file: $BIN"
    echo >> "$BIN"
    echo "exec \"$DIST\" \"\$@\"" >> "$BIN"
    chmod +x "$BIN"
  done
  for NAME in Isabelle isabelle
  do
    BIN="$BINDIR/$NAME"
    echo "installing $BIN"
    rm -f "$BIN"
    cp "$ISABELLE_HOME/bin/$NAME" "$BIN" || fail "Cannot write file: $BIN"
    chmod +x "$BIN"
  done
fi