lib/Tools/mkdir

rationalized output

#!/usr/bin/env bash
#
# Author: Markus Wenzel, TU Muenchen
#
# DESCRIPTION: prepare logic session directory


## diagnostics

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

function usage()
{
  echo
  echo "Usage: isabelle $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 = \$(ISABELLE_TOOL) 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; \$(ISABELLE_TOOL) 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_thys ["This_Theory1", "This_Theory2"];
  use_thys ["That_Theory1", "That_Theory2", "That_Theory3"];
*)
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{eurosym}
  %for \<euro>

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

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

%\usepackage{textcomp}
  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<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}

% for uniform font size
%\renewcommand{\isastyle}{\isastyleminor}


\begin{document}

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

\tableofcontents

% sane default for proof documents
\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:

  * 'isabelle 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