lib/Tools/mkdir

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: prepare logic session directory


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] [LOGIC] NAME"
  echo
  echo "  Options are:"
  echo "    -I FILE      alternative IsaMakefile output"
  echo "    -P           include parent logic target"
  echo "    -b           setup build mode (session outputs heap image)"
  echo "    -q           quiet mode"
  echo
  echo "  Prepare session directory, including IsaMakefile and document source"
  echo "  with parent LOGIC (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
  echo
  exit 1
}

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


## process command line

# options

ISAMAKEFILE="IsaMakefile"
PARENT=""
BUILD=""
QUIET=""

while getopts "I:Pbq" OPT
do
  case "$OPT" in
    I)
      ISAMAKEFILE="$OPTARG"
      ;;
    P)
      PARENT=true
      ;;
    b)
      BUILD=true
      ;;
    q)
      QUIET=true
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args


if [ "$#" -eq 1 ]; then
  LOGIC="$ISABELLE_LOGIC"
  DIR_NAME="$1"; shift
elif [ "$#" -eq 2 ]; then
  LOGIC="$1"; shift
  DIR_NAME="$1"; shift
else
  usage
fi

DIR=$(dirname "$DIR_NAME")
NAME=$(basename "$DIR_NAME")


## main

[ -z "$QUIET" ] && echo "Preparing session \"$NAME\" ..."


# IsaMakefile

mkdir -p "$DIR" || fail "Bad directory: $DIR"
cd "$DIR"

DOCUMENT_ROOT=""
VERBOSE=""
[ -z "$QUIET" ] && VERBOSE="-v true "

if [ -n "$BUILD" ]; then
  IMAGES="$NAME"
  TEST=""
  TARGET="\$(OUT)/$NAME"
  ROOT_ML="ROOT.ML"
  SOURCES="*.thy"
  DOCUMENT_ROOT="document/root.tex"
  USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
else
  IMAGES=""
  TEST="$NAME"
  TARGET="\$(LOG)/$LOGIC-$NAME.gz"
  ROOT_ML="$NAME/ROOT.ML"
  SOURCES="$NAME/*.thy"
  DOCUMENT_ROOT="$NAME/document/root.tex"
  USEDIR="\$(USEDIR)"
fi

if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then
  echo "keeping $DIR/$ISAMAKEFILE" >&2
else
  [ -z "$QUIET" -a -n "$ISAMAKEFILE" -a "$ISAMAKEFILE" != - ] && \
    echo "creating $DIR/$ISAMAKEFILE" >&2
  { echo
    echo "## targets"
    echo
    echo "default: $NAME"
    echo "images: $IMAGES"
    echo "test: $TEST"
    echo
    echo "all: images test"
    echo
    echo
    echo "## global settings"
    echo
    echo "SRC = \$(ISABELLE_HOME)/src"
    echo "OUT = \$(ISABELLE_OUTPUT)"
    echo "LOG = \$(OUT)/log"
    echo
    echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
    echo
    echo
    echo "## $NAME"
    echo ""
    if [ -n "$PARENT" ]; then
      echo "$NAME: $LOGIC $TARGET"
      echo
      echo "$LOGIC:"
      echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
      echo
      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT ## $SOURCES"
      echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
    else
      echo "$NAME: $TARGET"
      echo
      echo "$TARGET: ## $ROOT_ML $DOCUMENT_ROOT $SOURCES"
      echo -e "\t@$USEDIR $LOGIC $NAME"
    fi
    echo
    echo
    echo "## clean"
    echo
    echo "clean:"
    echo -e "\t@rm -f $TARGET"
  } | {
    if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then
      cat
    else
      cat > "$ISAMAKEFILE"
    fi
  }
fi


# base directory

if [ -z "$BUILD" ]; then
  mkdir -p "$NAME" || fail "Bad directory: $DIR/$NAME"
  cd "$NAME"
  PREFIX="$DIR/$NAME"
else
  PREFIX="$DIR"
fi

if [ -f ROOT.ML ]; then
  echo "keeping $PREFIX/ROOT.ML" >&2
else
  [ -z "$QUIET" ] && echo "creating $PREFIX/ROOT.ML" >&2
  cat >ROOT.ML <<EOF
(*
  no_document use_thy "ThisTheory";
  use_thy "ThatTheory";
*)
EOF
fi


# document directory

if [ -e document ]; then
  echo "keeping $PREFIX/document" >&2
else
  [ -z "$QUIET" ] && echo "creating $PREFIX/document" >&2
  mkdir document || fail "Bad directory: $PREFIX/document"

  [ -z "$QUIET" ] && echo "creating $PREFIX/document/root.tex" >&2
  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
  cat >document/root.tex <<EOF
\documentclass[11pt,a4paper]{article}
\usepackage{isabelle,isabellesym}

% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed

%\usepackage{amssymb}
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
  %\<triangleq>, \<yen>, \<lozenge>

%\usepackage[greek,english]{babel}
  %option greek for \<euro>
  %option english (default language) for \<guillemotleft>, \<guillemotright>

%\usepackage[latin1]{inputenc}
  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
  %\<threesuperior>, \<threequarters>, \<degree>

%\usepackage[only,bigsqcap]{stmaryrd}
  %for \<Sqinter>

%\usepackage{eufrak}
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)

%\usepackage{textcomp}
  %for \<cent>, \<currency>

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{$TITLE}
\author{$AUTHOR}
\maketitle

\tableofcontents

\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
%\bibliographystyle{abbrv}
%\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
EOF
fi


# notes

if [ -z "$QUIET" ]; then
  cat >&2 <<EOF

Notes:

  * 'isatool make' processes the session (including document preparation)

  * $DIR/IsaMakefile contains compilation options and file dependencies

  * $PREFIX/document/root.tex contains the LaTeX master document setup

  * $PREFIX/ROOT.ML needs to contain ML code to load all theories

EOF
fi