lib/Tools/mkdir
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 29143 72c960b2b83e
child 32299 5f33ce0ed21f
permissions -rwxr-xr-x
renamed structure Display_Goal to Goal_Display;
wenzelm@10555
     1
#!/usr/bin/env bash
wenzelm@8159
     2
#
wenzelm@9788
     3
# Author: Markus Wenzel, TU Muenchen
wenzelm@8159
     4
#
wenzelm@8159
     5
# DESCRIPTION: prepare logic session directory
wenzelm@8159
     6
wenzelm@8159
     7
wenzelm@8159
     8
## diagnostics
wenzelm@8159
     9
wenzelm@10511
    10
PRG="$(basename "$0")"
wenzelm@8159
    11
wenzelm@8159
    12
function usage()
wenzelm@8159
    13
{
wenzelm@8159
    14
  echo
wenzelm@28650
    15
  echo "Usage: isabelle $PRG [OPTIONS] [LOGIC] NAME"
wenzelm@8159
    16
  echo
wenzelm@8159
    17
  echo "  Options are:"
wenzelm@8198
    18
  echo "    -I FILE      alternative IsaMakefile output"
wenzelm@8211
    19
  echo "    -P           include parent logic target"
wenzelm@8159
    20
  echo "    -b           setup build mode (session outputs heap image)"
wenzelm@11578
    21
  echo "    -q           quiet mode"
wenzelm@8159
    22
  echo
wenzelm@11578
    23
  echo "  Prepare session directory, including IsaMakefile and document source"
wenzelm@8199
    24
  echo "  with parent LOGIC (default ISABELLE_LOGIC=$ISABELLE_LOGIC)"
wenzelm@8159
    25
  echo
wenzelm@8159
    26
  exit 1
wenzelm@8159
    27
}
wenzelm@8159
    28
wenzelm@8159
    29
function fail()
wenzelm@8159
    30
{
wenzelm@8159
    31
  echo "$1" >&2
wenzelm@8159
    32
  exit 2
wenzelm@8159
    33
}
wenzelm@8159
    34
wenzelm@8159
    35
wenzelm@8159
    36
## process command line
wenzelm@8159
    37
wenzelm@8159
    38
# options
wenzelm@8159
    39
wenzelm@8198
    40
ISAMAKEFILE="IsaMakefile"
wenzelm@8211
    41
PARENT=""
wenzelm@8159
    42
BUILD=""
wenzelm@11578
    43
QUIET=""
wenzelm@8159
    44
wenzelm@11578
    45
while getopts "I:Pbq" OPT
wenzelm@8159
    46
do
wenzelm@8159
    47
  case "$OPT" in
wenzelm@8198
    48
    I)
wenzelm@8198
    49
      ISAMAKEFILE="$OPTARG"
wenzelm@8198
    50
      ;;
wenzelm@8211
    51
    P)
wenzelm@8211
    52
      PARENT=true
wenzelm@8211
    53
      ;;
wenzelm@8159
    54
    b)
wenzelm@8159
    55
      BUILD=true
wenzelm@8159
    56
      ;;
wenzelm@11578
    57
    q)
wenzelm@11578
    58
      QUIET=true
wenzelm@8159
    59
      ;;
wenzelm@8159
    60
    \?)
wenzelm@8159
    61
      usage
wenzelm@8159
    62
      ;;
wenzelm@8159
    63
  esac
wenzelm@8159
    64
done
wenzelm@8159
    65
wenzelm@8159
    66
shift $(($OPTIND - 1))
wenzelm@8159
    67
wenzelm@8159
    68
wenzelm@8159
    69
# args
wenzelm@8159
    70
wenzelm@8159
    71
wenzelm@9788
    72
if [ "$#" -eq 1 ]; then
wenzelm@8194
    73
  LOGIC="$ISABELLE_LOGIC"
wenzelm@8685
    74
  DIR_NAME="$1"; shift
wenzelm@9788
    75
elif [ "$#" -eq 2 ]; then
wenzelm@8194
    76
  LOGIC="$1"; shift
wenzelm@8685
    77
  DIR_NAME="$1"; shift
wenzelm@8194
    78
else
wenzelm@8194
    79
  usage
wenzelm@8194
    80
fi
wenzelm@8159
    81
wenzelm@8685
    82
DIR=$(dirname "$DIR_NAME")
wenzelm@8685
    83
NAME=$(basename "$DIR_NAME")
wenzelm@8159
    84
wenzelm@8159
    85
wenzelm@8159
    86
## main
wenzelm@8159
    87
wenzelm@11578
    88
[ -z "$QUIET" ] && echo "Preparing session \"$NAME\" ..."
wenzelm@11578
    89
wenzelm@11578
    90
wenzelm@8159
    91
# IsaMakefile
wenzelm@8159
    92
wenzelm@8685
    93
mkdir -p "$DIR" || fail "Bad directory: $DIR"
wenzelm@8685
    94
cd "$DIR"
wenzelm@8685
    95
wenzelm@8244
    96
DOCUMENT_ROOT=""
wenzelm@11846
    97
VERBOSE=""
wenzelm@11846
    98
[ -z "$QUIET" ] && VERBOSE="-v true "
wenzelm@8244
    99
wenzelm@8159
   100
if [ -n "$BUILD" ]; then
wenzelm@8159
   101
  IMAGES="$NAME"
wenzelm@8159
   102
  TEST=""
wenzelm@8159
   103
  TARGET="\$(OUT)/$NAME"
wenzelm@8244
   104
  ROOT_ML="ROOT.ML"
wenzelm@8579
   105
  SOURCES="*.thy"
wenzelm@11578
   106
  DOCUMENT_ROOT="document/root.tex"
wenzelm@8194
   107
  USEDIR="\$(USEDIR) -b -P http://isabelle.in.tum.de/library"
wenzelm@8159
   108
else
wenzelm@8159
   109
  IMAGES=""
wenzelm@8159
   110
  TEST="$NAME"
wenzelm@8211
   111
  TARGET="\$(LOG)/$LOGIC-$NAME.gz"
wenzelm@8244
   112
  ROOT_ML="$NAME/ROOT.ML"
wenzelm@8579
   113
  SOURCES="$NAME/*.thy"
wenzelm@11578
   114
  DOCUMENT_ROOT="$NAME/document/root.tex"
wenzelm@8194
   115
  USEDIR="\$(USEDIR)"
wenzelm@8159
   116
fi
wenzelm@8159
   117
wenzelm@8198
   118
if [ "$ISAMAKEFILE" != - -a -f "$ISAMAKEFILE" ]; then
wenzelm@11578
   119
  echo "keeping $DIR/$ISAMAKEFILE" >&2
wenzelm@8159
   120
else
wenzelm@11650
   121
  [ -z "$QUIET" -a -n "$ISAMAKEFILE" -a "$ISAMAKEFILE" != - ] && \
wenzelm@11650
   122
    echo "creating $DIR/$ISAMAKEFILE" >&2
wenzelm@8159
   123
  { echo
wenzelm@8159
   124
    echo "## targets"
wenzelm@8159
   125
    echo
wenzelm@8159
   126
    echo "default: $NAME"
wenzelm@8159
   127
    echo "images: $IMAGES"
wenzelm@8159
   128
    echo "test: $TEST"
wenzelm@8159
   129
    echo
wenzelm@8159
   130
    echo "all: images test"
wenzelm@8159
   131
    echo
wenzelm@8159
   132
    echo
wenzelm@8159
   133
    echo "## global settings"
wenzelm@8159
   134
    echo
wenzelm@8159
   135
    echo "SRC = \$(ISABELLE_HOME)/src"
wenzelm@8159
   136
    echo "OUT = \$(ISABELLE_OUTPUT)"
wenzelm@8159
   137
    echo "LOG = \$(OUT)/log"
wenzelm@11578
   138
    echo
wenzelm@28500
   139
    echo "USEDIR = \$(ISABELLE_TOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
wenzelm@8159
   140
    echo
wenzelm@8159
   141
    echo
wenzelm@8159
   142
    echo "## $NAME"
wenzelm@8159
   143
    echo ""
wenzelm@8162
   144
    if [ -n "$PARENT" ]; then
wenzelm@8162
   145
      echo "$NAME: $LOGIC $TARGET"
wenzelm@8162
   146
      echo
wenzelm@8162
   147
      echo "$LOGIC:"
wenzelm@28500
   148
      echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISABELLE_TOOL) make $LOGIC"
wenzelm@8162
   149
      echo
kleing@13946
   150
      echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT ## $SOURCES"
wenzelm@8194
   151
      echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
wenzelm@8162
   152
    else
wenzelm@8162
   153
      echo "$NAME: $TARGET"
wenzelm@8162
   154
      echo
kleing@13946
   155
      echo "$TARGET: ## $ROOT_ML $DOCUMENT_ROOT $SOURCES"
wenzelm@8194
   156
      echo -e "\t@$USEDIR $LOGIC $NAME"
wenzelm@8162
   157
    fi
wenzelm@8159
   158
    echo
wenzelm@8159
   159
    echo
wenzelm@8159
   160
    echo "## clean"
wenzelm@8159
   161
    echo
wenzelm@8159
   162
    echo "clean:"
wenzelm@8159
   163
    echo -e "\t@rm -f $TARGET"
wenzelm@8198
   164
  } | {
wenzelm@8198
   165
    if [ -z "$ISAMAKEFILE" -o "$ISAMAKEFILE" = - ]; then
wenzelm@8198
   166
      cat
wenzelm@8198
   167
    else
wenzelm@8198
   168
      cat > "$ISAMAKEFILE"
wenzelm@8198
   169
    fi
wenzelm@8198
   170
  }
wenzelm@8159
   171
fi
wenzelm@8159
   172
wenzelm@8159
   173
wenzelm@8159
   174
# base directory
wenzelm@8159
   175
wenzelm@8159
   176
if [ -z "$BUILD" ]; then
wenzelm@11578
   177
  mkdir -p "$NAME" || fail "Bad directory: $DIR/$NAME"
wenzelm@8159
   178
  cd "$NAME"
wenzelm@11578
   179
  PREFIX="$DIR/$NAME"
wenzelm@11578
   180
else
wenzelm@11578
   181
  PREFIX="$DIR"
wenzelm@8159
   182
fi
wenzelm@8159
   183
wenzelm@8159
   184
if [ -f ROOT.ML ]; then
wenzelm@11578
   185
  echo "keeping $PREFIX/ROOT.ML" >&2
wenzelm@8159
   186
else
wenzelm@11650
   187
  [ -z "$QUIET" ] && echo "creating $PREFIX/ROOT.ML" >&2
wenzelm@11578
   188
  cat >ROOT.ML <<EOF
wenzelm@11578
   189
(*
wenzelm@11578
   190
  no_document use_thy "ThisTheory";
wenzelm@11578
   191
  use_thy "ThatTheory";
wenzelm@11578
   192
*)
wenzelm@11578
   193
EOF
wenzelm@8159
   194
fi
wenzelm@8159
   195
wenzelm@8159
   196
wenzelm@8159
   197
# document directory
wenzelm@8159
   198
wenzelm@11578
   199
if [ -e document ]; then
wenzelm@11578
   200
  echo "keeping $PREFIX/document" >&2
wenzelm@11578
   201
else
wenzelm@11650
   202
  [ -z "$QUIET" ] && echo "creating $PREFIX/document" >&2
wenzelm@11578
   203
  mkdir document || fail "Bad directory: $PREFIX/document"
wenzelm@11650
   204
wenzelm@11650
   205
  [ -z "$QUIET" ] && echo "creating $PREFIX/document/root.tex" >&2
wenzelm@16482
   206
  TITLE=$(echo "$NAME" | tr _ - | tr -d '\\')
wenzelm@16482
   207
  AUTHOR=$(echo "By $USER" | tr _ - | tr -d '\\')
wenzelm@11578
   208
  cat >document/root.tex <<EOF
wenzelm@8159
   209
\documentclass[11pt,a4paper]{article}
wenzelm@11578
   210
\usepackage{isabelle,isabellesym}
wenzelm@8159
   211
wenzelm@16482
   212
% further packages required for unusual symbols (see also
wenzelm@16482
   213
% isabellesym.sty), use only when needed
wenzelm@16482
   214
wenzelm@16482
   215
%\usepackage{amssymb}
wenzelm@16482
   216
  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
wenzelm@16482
   217
  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
wenzelm@16482
   218
  %\<triangleq>, \<yen>, \<lozenge>
wenzelm@16482
   219
wenzelm@16482
   220
%\usepackage[greek,english]{babel}
wenzelm@16482
   221
  %option greek for \<euro>
wenzelm@16482
   222
  %option english (default language) for \<guillemotleft>, \<guillemotright>
wenzelm@16482
   223
wenzelm@16482
   224
%\usepackage[latin1]{inputenc}
wenzelm@16482
   225
  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
wenzelm@16482
   226
  %\<threesuperior>, \<threequarters>, \<degree>
wenzelm@16482
   227
wenzelm@16482
   228
%\usepackage[only,bigsqcap]{stmaryrd}
wenzelm@16482
   229
  %for \<Sqinter>
wenzelm@16482
   230
wenzelm@16482
   231
%\usepackage{eufrak}
wenzelm@16482
   232
  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
wenzelm@16482
   233
wenzelm@16482
   234
%\usepackage{textcomp}
wenzelm@16482
   235
  %for \<cent>, \<currency>
wenzelm@11578
   236
wenzelm@11578
   237
% this should be the last package used
wenzelm@11578
   238
\usepackage{pdfsetup}
wenzelm@11578
   239
kleing@13946
   240
% urls in roman style, theory text in math-similar italics
wenzelm@10021
   241
\urlstyle{rm}
wenzelm@10021
   242
\isabellestyle{it}
wenzelm@9656
   243
nipkow@28180
   244
% for uniform font size
nipkow@28180
   245
%\renewcommand{\isastyle}{\isastyleminor}
nipkow@28180
   246
wenzelm@11578
   247
wenzelm@8159
   248
\begin{document}
wenzelm@10353
   249
wenzelm@11578
   250
\title{$TITLE}
wenzelm@11578
   251
\author{$AUTHOR}
wenzelm@11578
   252
\maketitle
wenzelm@11578
   253
wenzelm@10308
   254
\tableofcontents
wenzelm@10353
   255
wenzelm@25172
   256
% sane default for proof documents
wenzelm@25410
   257
\parindent 0pt\parskip 0.5ex
wenzelm@11578
   258
wenzelm@14936
   259
% generated text of all theories
wenzelm@8159
   260
\input{session}
wenzelm@10353
   261
wenzelm@14936
   262
% optional bibliography
wenzelm@12104
   263
%\bibliographystyle{abbrv}
wenzelm@10353
   264
%\bibliography{root}
wenzelm@10353
   265
wenzelm@8159
   266
\end{document}
wenzelm@14936
   267
wenzelm@14936
   268
%%% Local Variables:
wenzelm@14936
   269
%%% mode: latex
wenzelm@14936
   270
%%% TeX-master: t
wenzelm@14936
   271
%%% End:
wenzelm@8159
   272
EOF
wenzelm@8159
   273
fi
wenzelm@11578
   274
wenzelm@11578
   275
wenzelm@11578
   276
# notes
wenzelm@11578
   277
wenzelm@11578
   278
if [ -z "$QUIET" ]; then
wenzelm@11650
   279
  cat >&2 <<EOF
wenzelm@11578
   280
wenzelm@11578
   281
Notes:
wenzelm@11578
   282
wenzelm@28504
   283
  * 'isabelle make' processes the session (including document preparation)
wenzelm@11578
   284
wenzelm@11650
   285
  * $DIR/IsaMakefile contains compilation options and file dependencies
wenzelm@11650
   286
wenzelm@11846
   287
  * $PREFIX/document/root.tex contains the LaTeX master document setup
wenzelm@11578
   288
wenzelm@11846
   289
  * $PREFIX/ROOT.ML needs to contain ML code to load all theories
wenzelm@11578
   290
wenzelm@11578
   291
EOF
wenzelm@11578
   292
fi