lib/Tools/mkroot

store proper theorems even for fixed points that have no passive live variables

#!/usr/bin/env bash
#
# Author: Makarius
#
# DESCRIPTION: prepare session root directory


## diagnostics

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

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
  echo
  echo "  Options are:"
  echo "    -d           enable document preparation"
  echo "    -n NAME      alternative session name (default: DIR base name)"
  echo
  echo "  Prepare session root DIR (default: current directory)."
  echo
  exit 1
}

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


## process command line

# options

DOC=""
NAME=""

while getopts "n:d" OPT
do
  case "$OPT" in
    d)
      DOC="true"
      ;;
    n)
      NAME="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

if [ "$#" -eq 0 ]; then
  DIR="."
elif [ "$#" -eq 1 ]; then
  DIR="$1"
  shift
else
  usage
fi


## main

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

[ -z "$NAME" ] && NAME="$(basename "$(cd "$DIR"; pwd -P)")"

[ -e "$DIR/ROOT" ] && fail "Cannot overwrite existing $DIR/ROOT"

[ "$DOC" = true -a -e "$DIR/document" ] && \
  fail "Cannot overwrite existing $DIR/document"

echo
echo "Preparing session \"$NAME\" in \"$DIR\""


# ROOT

echo "  creating $DIR/ROOT"

if [ "$DOC" = true ]; then
  cat > "$DIR/ROOT" <<EOF
session "$NAME" = "$ISABELLE_LOGIC" +
  options [document = $ISABELLE_DOC_FORMAT, document_output = "output"]
  theories [document = false]
    (* Foo Bar *)
  theories
    (* Baz *)
  files "document/root.tex"
EOF
else
  cat > "$DIR/ROOT" <<EOF
session "$NAME" = "$ISABELLE_LOGIC" +
  options [document = false]
  theories
    (* Foo Bar Baz *)
EOF
fi


# document directory

if [ "$DOC" = true ]; then
  echo "  creating $DIR/document/root.tex"

  mkdir "$DIR/document" || fail "Bad directory: \"$DIR/document\""
  
  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')

  cat > "$DIR/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

declare -a DIR_PARTS=($DIR)
if [ ${#DIR_PARTS[@]} = 1 ]; then
  OPT_DIR="-D $DIR"
else
  OPT_DIR="-D \"$DIR\""
fi

cat <<EOF

Now use the following command line to build the session:

  isabelle build $OPT_DIR

EOF