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