lib/Tools/mkdir

For the Isar version of the ZF logics manual

#!/usr/bin/env bash
#
# $Id$
# Author: Markus Wenzel, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# 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 pdf  ## -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

#set by configure
AUTO_PERL=perl

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 _ -)
  AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -)
  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}     % greek for \<euro>,
                                       % english for \<guillemotleft>, 
                                       %             \<guillemotright>
                                       % default language = last
%\usepackage[latin1]{inputenc}         % for \<onesuperior>, \<onequarter>,
                                       % \<twosuperior>, \<onehalf>,
                                       % \<threesuperior>, \<threequarters>,
                                       % \<degree>
%\usepackage[only,bigsqcap]{stmaryrd}  % for \<Sqinter>
%\usepackage{eufrak}                   % for \<AA> ... \<ZZ>, \<aa> ... \<zz>
                                       % (only needed if amssymb not used)
%\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

% include generated text of all theories
\input{session}

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

\end{document}
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