diff --git a/Admin/makedist b/Admin/makedist --- a/Admin/makedist +++ b/Admin/makedist @@ -1,258 +1,258 @@ #!/usr/bin/env bash # # $Id$ # # makedist -- make Isabelle source distribution. ## global settings DISTPREFIX=${DISTPREFIX:-~/tmp/isadist} SRCS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents Tools ZF" export CVSROOT=/usr/proj/isabelle-repository/archive [ ! -d "$CVSROOT" ] && CVSROOT="${ISABELLE_USER:-$USER}@sunbroy2.informatik.tu-muenchen.de:$CVSROOT" umask 022 TAR=tar type -path gtar >/dev/null && TAR=gtar FIND=find type -path gfind >/dev/null && FIND=gfind ## diagnostics PRG=$(basename "$0") THIS=$(cd $(dirname "$0"); echo "$PWD") function usage() { cat <&2 exit 2 } ## process command line [ "$#" -ne 1 -a "$#" -ne 2 ] && usage VERSION="$1"; shift if [ "$#" -eq 0 ]; then DISTNAME="" else DISTNAME="$1"; shift fi ## main # dist version DATE=$(env LC_ALL=C date "+%d-%b-%Y") DISTDATE=$(env LC_ALL=C date "+%B %Y") if [ "$VERSION" = "-" ]; then DISTIDENT="Isabelle_$DATE" [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" DISTVERSION="$DISTNAME" EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle" UNOFFICIAL=true else DISTIDENT="$VERSION" [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" DISTVERSION="$DISTNAME: $DISTDATE" EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle" UNOFFICIAL="" fi DISTBASE="$DISTPREFIX/dist-$DISTNAME" mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!" [ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!" [ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!" # export repository echo "###" echo "### Exporting $DISTIDENT ..." echo "###" cd "$DISTBASE" $EXPORT || fail "Export failed!" if [ -n "$CVS2CL" ]; then cd $DISTNAME $CVS2CL gzip ChangeLog mv ChangeLog.gz .. cd .. fi $FIND . -name CVS -print | xargs rm -rf $FIND . -name .cvsignore -print | xargs rm -rf $FIND . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x $FIND . -print | xargs chmod u+rw # build docs echo "###" echo "### Building docs ..." echo "###" cd "$DISTBASE/$DISTNAME/Doc" PDFLATEX=$(type -path pdflatex) for DOC in $(cat Contents) do pushd "$DOC" > /dev/null make dvi || fail "DVI document for $DOC failed!" { [ -n "$PDFLATEX" ] && make clean pdf; } || fail "PDF document for $DOC failed!" popd done # prepare dist dir for release echo "###" echo "### Preparing distribution ..." echo "###" cd "$DISTBASE/$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME" cp -R Admin/website .. mkdir -p ../website/conf cat > ../website/conf/distinfo.mak <ANNOUNCE fi -perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html +perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/library_index_header.html perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README ( cd src; ../Admin/maketags; ) rm -rf Admin rm -f TODO # create archive echo "###" echo "### Creating archives ..." echo "###" cd "$DISTBASE" echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST rm -f Isabelle ln -s "$DISTNAME" Isabelle chown -R "$LOGNAME" "$DISTNAME" chmod -R u+w "$DISTNAME" chmod -R g=o "$DISTNAME" chgrp -R isabelle "$DISTNAME" Isabelle mkdir -p "pdf/$DISTNAME/doc" mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" sync; sleep 3 echo "$DISTNAME.tar.gz" "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME" gzip "$DISTNAME.tar" echo "${DISTNAME}_pdf.tar.gz" ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) gzip "${DISTNAME}_pdf.tar" mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc" rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf # cleanup dist mv "$DISTNAME" "${DISTNAME}-old" mkdir "$DISTNAME" mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \ "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \ "$DISTNAME" mkdir "$DISTNAME/doc" mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" chgrp -R isabelle "$DISTNAME" rm -rf "${DISTNAME}-old" # final note echo "###" echo "### Finished makedist." echo "###" diff --git a/lib/Tools/usedir b/lib/Tools/usedir --- a/lib/Tools/usedir +++ b/lib/Tools/usedir @@ -1,256 +1,256 @@ #!/usr/bin/env bash # # $Id$ # Author: Markus Wenzel, TU Muenchen # # DESCRIPTION: build object-logic or run examples ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: $PRG [OPTIONS] LOGIC NAME" echo echo " Options are:" echo " -C BOOL copy existing document directory to -D PATH (default true)" echo " -D PATH dump generated document sources into PATH" echo " -M MAX multithreading: maximum number of worker threads (default 1)" echo " -P PATH set path for remote theory browsing information" echo " -T LEVEL multithreading: trace level (default 0)" echo " -V VERSION declare alternative document VERSION" echo " -b build mode (output heap image, using current dir)" echo " -c BOOL tell ML system to compress output image (default true)" echo " -d FORMAT build document as FORMAT (default false)" echo " -f NAME use ML file NAME (default ROOT.ML)" echo " -g BOOL generate session graph image for document (default false)" echo " -i BOOL generate HTML and graph browser information (default false)" echo " -m MODE add print mode for output" echo " -p LEVEL set level of detail for proof objects" echo " -r reset session path" echo " -s NAME override session NAME" echo " -v BOOL be verbose (default false)" echo echo " Build object-logic or run examples. Also creates browsing" echo " information (HTML etc.) according to settings." echo echo " ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS" echo " HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS" echo exit 1 } function fail() { echo "$1" >&2 exit 2 } function check_bool() { [ "$1" = true -o "$1" = false ] || fail "Bad boolean: \"$1\"" } function check_number() { [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\"" } ## process command line # options COPY_DUMP=true DUMP="" MAXTHREADS="1" RPATH="" TRACETHREADS="0" DOCUMENT_VERSIONS="" BUILD="" COMPRESS=true DOCUMENT=false ROOT_FILE="ROOT.ML" DOCUMENT_GRAPH=false INFO=false MODES="" RESET=false SESSION="" PROOFS=0 VERBOSE=false function getoptions() { OPTIND=1 while getopts "C:D:M:P:T:V:bc:d:f:g:i:m:p:rs:v:" OPT do case "$OPT" in C) check_bool "$OPTARG" COPY_DUMP="$OPTARG" ;; D) DUMP="$OPTARG" ;; M) check_number "$OPTARG" MAXTHREADS="$OPTARG" ;; P) RPATH="$OPTARG" ;; T) check_number "$OPTARG" TRACETHREADS="$OPTARG" ;; V) if [ -z "$DOCUMENT_VERSIONS" ]; then DOCUMENT_VERSIONS="\"$OPTARG\"" else DOCUMENT_VERSIONS="$DOCUMENT_VERSIONS, \"$OPTARG\"" fi ;; b) BUILD=true ;; c) check_bool "$OPTARG" COMPRESS="$OPTARG" ;; d) DOCUMENT="$OPTARG" ;; f) ROOT_FILE="$OPTARG" ;; g) check_bool "$OPTARG" DOCUMENT_GRAPH="$OPTARG" ;; i) check_bool "$OPTARG" INFO="$OPTARG" ;; m) if [ -z "$MODES" ]; then MODES="\"$OPTARG\"" else MODES="\"$OPTARG\", $MODES" fi ;; p) check_number "$OPTARG" PROOFS="$OPTARG" ;; r) RESET=true ;; s) SESSION="$OPTARG" ;; v) check_bool "$OPTARG" VERBOSE="$OPTARG" ;; \?) usage ;; esac done } getoptions $ISABELLE_USEDIR_OPTIONS getoptions "$@" shift $(($OPTIND - 1)) # args [ "$#" -ne 2 ] && usage LOGIC="$1"; shift NAME="$1"; shift [ -z "$SESSION" ] && SESSION=$(basename "$NAME") ## main # prepare browser info dir -if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/library_index_header.html" ]; then +if [ "$INFO" = "true" -a ! -f "$ISABELLE_BROWSER_INFO/index.html" ]; then mkdir -p "$ISABELLE_BROWSER_INFO" cp "$ISABELLE_HOME/lib/logo/isabelle.gif" "$ISABELLE_BROWSER_INFO/isabelle.gif" cat "$ISABELLE_HOME/lib/html/library_index_header.template" \ "$ISABELLE_HOME/lib/html/library_index_content.template" \ "$ISABELLE_HOME/lib/html/library_index_footer.template"> "$ISABELLE_BROWSER_INFO/index.html" fi # prepare log dir LOGDIR="$ISABELLE_OUTPUT/log" mkdir -p "$LOGDIR" # run isabelle PARENT=$(basename "$LOGIC") if [ -z "$BUILD" ]; then cd "$NAME" || fail "Bad session directory '$NAME'" fi if [ "$DOCUMENT" != false ]; then DOC="$DOCUMENT" else DOC="" fi . "$ISABELLE_HOME/lib/scripts/timestart.bash" if [ -n "$BUILD" ]; then ITEM="$SESSION" echo "Building $ITEM ..." >&2 LOG="$LOGDIR/$ITEM" OPT_C="" [ "$COMPRESS" = true ] && OPT_C="-c" "$ISABELLE" \ -e "Session.use_dir \"$ROOT_FILE\" true [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS;" \ $OPT_C -q -w $LOGIC $NAME > "$LOG" RC="$?" else ITEM=$(basename "$LOGIC")-"$SESSION" echo "Running $ITEM ..." >&2 LOG="$LOGDIR/$ITEM" "$ISABELLE" \ -e "Session.use_dir \"$ROOT_FILE\" false [$MODES] $RESET $INFO \"$DOC\" $DOCUMENT_GRAPH [$DOCUMENT_VERSIONS] \"$PARENT\" \"$SESSION\" ($COPY_DUMP, \"$DUMP\") \"$RPATH\" $PROOFS $VERBOSE $MAXTHREADS $TRACETHREADS; quit();" \ -r -q "$LOGIC" > "$LOG" RC="$?" cd .. fi . "$ISABELLE_HOME/lib/scripts/timestop.bash" # exit status if [ "$RC" -eq 0 ]; then echo "Finished $ITEM ($TIMES_REPORT)" >&2 gzip --force "$LOG" else { echo "$ITEM FAILED"; echo "(see also $LOG)"; echo; tail "$LOG"; echo; } >&2 fi exit "$RC" diff --git a/lib/html/index.html b/lib/html/index.html deleted file mode 100644 --- a/lib/html/index.html +++ /dev/null @@ -1,76 +0,0 @@ - - - - - - - - - - The {ISABELLE} Library - - - -
- - - - - - -
[Isabelle] - - - - -
The {ISABELLE} Library
-
-
-
- - - - - - - - diff --git a/lib/html/library_index_content.template b/lib/html/library_index_content.template new file mode 100644 --- /dev/null +++ b/lib/html/library_index_content.template @@ -0,0 +1,44 @@ + + + + + + diff --git a/lib/html/library_index_footer.template b/lib/html/library_index_footer.template new file mode 100644 --- /dev/null +++ b/lib/html/library_index_footer.template @@ -0,0 +1,2 @@ + + diff --git a/lib/html/library_index_header.template b/lib/html/library_index_header.template new file mode 100644 --- /dev/null +++ b/lib/html/library_index_header.template @@ -0,0 +1,28 @@ + + + + + + + + The {ISABELLE} Library + + + +
+ + + + + + +
[Isabelle] + + + + +
The {ISABELLE} Library
+
+
+