wenzelm@12721: #!/usr/bin/env bash wenzelm@2667: # wenzelm@2667: # $Id$ wenzelm@2667: # wenzelm@10077: # makedist -- make Isabelle source distribution. wenzelm@2667: wenzelm@2667: wenzelm@2667: ## global settings wenzelm@2667: wenzelm@17554: DISTPREFIX=${DISTPREFIX:-~/tmp/isadist} wenzelm@7993: LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL ZF" wenzelm@2667: wenzelm@17554: export CVSROOT=/usr/proj/isabelle-repository/archive wenzelm@17554: [ ! -d "$CVSROOT" ] && CVSROOT="sunbroy2.informatik.tu-muenchen.de:$CVSROOT" wenzelm@2667: wenzelm@9797: umask 022 wenzelm@9797: wenzelm@9920: TAR=tar wenzelm@9920: type -path gtar >/dev/null && TAR=gtar wenzelm@9920: wenzelm@9920: FIND=find wenzelm@9920: type -path gfind >/dev/null && FIND=gfind wenzelm@9920: wenzelm@2667: wenzelm@2667: ## diagnostics wenzelm@2667: wenzelm@9797: PRG=$(basename "$0") wenzelm@9797: THIS=$(cd $(dirname "$0"); echo "$PWD") wenzelm@2667: wenzelm@2667: function usage() wenzelm@2667: { wenzelm@2667: cat <&2 wenzelm@2667: exit 2 wenzelm@2667: } wenzelm@2667: wenzelm@2667: wenzelm@2667: ## process command line wenzelm@2667: wenzelm@17554: [ "$#" -ne 1 -a "$#" -ne 2 ] && usage wenzelm@17554: wenzelm@17554: VERSION="$1"; shift wenzelm@2667: wenzelm@17554: if [ "$#" -eq 0 ]; then wenzelm@17554: DISTNAME="" wenzelm@17554: else wenzelm@17554: DISTNAME="$1"; shift wenzelm@17554: fi wenzelm@2667: wenzelm@2667: wenzelm@2667: ## main wenzelm@2667: wenzelm@2667: # dist version wenzelm@2667: wenzelm@2667: DATE=$(date "+%d-%b-%Y") wenzelm@4979: DISTDATE=$(date "+%B %Y") wenzelm@2667: wenzelm@17554: if [ "$VERSION" = "-" ]; then wenzelm@17554: DISTIDENT="Isabelle_$DATE" wenzelm@17554: [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" wenzelm@9797: DISTVERSION="$DISTNAME" wenzelm@9797: EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle" wenzelm@17558: UNOFFICIAL=true wenzelm@2667: else wenzelm@17554: DISTIDENT="$VERSION" wenzelm@17554: [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT" wenzelm@4982: DISTVERSION="$DISTNAME: $DISTDATE" wenzelm@17561: EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle" wenzelm@2667: UNOFFICIAL="" wenzelm@2667: fi wenzelm@2667: wenzelm@9797: DISTBASE="$DISTPREFIX/dist-$DISTNAME" wenzelm@9797: mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!" wenzelm@9797: [ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!" wenzelm@9797: [ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!" wenzelm@2667: wenzelm@2667: wenzelm@9797: # export repository wenzelm@2667: wenzelm@9797: echo "###" wenzelm@17554: echo "### Exporting $DISTIDENT ..." wenzelm@9797: echo "###" wenzelm@2667: wenzelm@9797: cd "$DISTBASE" wenzelm@2667: kleing@13230: $EXPORT || fail "Export failed!" berghofe@15438: berghofe@15438: if [ -n "$CVS2CL" ]; then berghofe@15438: cd $DISTNAME berghofe@15438: $CVS2CL berghofe@15438: gzip ChangeLog berghofe@15438: mv ChangeLog.gz .. berghofe@15438: cd .. berghofe@15438: fi berghofe@15438: wenzelm@9920: $FIND . -name CVS -print | xargs rm -rf wenzelm@12986: $FIND . -name .cvsignore -print | xargs rm -rf wenzelm@17554: $FIND . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x wenzelm@2667: wenzelm@2667: wenzelm@9797: # build docs wenzelm@2667: wenzelm@9797: echo "###" wenzelm@9797: echo "### Building docs ..." wenzelm@9797: echo "###" wenzelm@9797: wenzelm@9797: cd "$DISTBASE/$DISTNAME/Doc" wenzelm@6630: PDFLATEX=$(type -path pdflatex) wenzelm@3169: wenzelm@3169: for DOC in $(cat Contents) wenzelm@2667: do wenzelm@9797: cd "$DOC" kleing@13230: make dvi || fail "DVI document for $DOC failed!" wenzelm@17554: { [ -n "$PDFLATEX" ] && make clean pdf; } || fail "PDF document for $DOC failed!" wenzelm@3169: cd .. wenzelm@2667: done wenzelm@2667: wenzelm@9052: wenzelm@9920: # prepare dist dir for release kleing@8059: wenzelm@9920: echo "###" wenzelm@9920: echo "### Preparing distribution ..." wenzelm@9920: echo "###" wenzelm@2667: wenzelm@17554: cd "$DISTBASE/$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME" wenzelm@2667: haftmann@16301: cp -R Admin/website .. haftmann@16301: mkdir -p ../website/conf haftmann@16301: cat > ../website/conf/distname.mak <ANNOUNCE wenzelm@2667: fi wenzelm@2667: wenzelm@8810: perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html wenzelm@17554: perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version wenzelm@4986: perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html wenzelm@3257: lynx -dump README.html >README wenzelm@3257: wenzelm@9052: ( cd src; ../Admin/maketags; ) wenzelm@10077: wenzelm@9052: rm -rf Admin wenzelm@16286: rm -f TODO wenzelm@9052: wenzelm@2667: wenzelm@2667: # create archive wenzelm@2667: wenzelm@9797: echo "###" wenzelm@9797: echo "### Creating archives ..." wenzelm@9797: echo "###" wenzelm@2667: wenzelm@9797: cd "$DISTBASE" wenzelm@9797: wenzelm@10087: echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST wenzelm@10087: wenzelm@10068: rm -f Isabelle wenzelm@10068: ln -s "$DISTNAME" Isabelle wenzelm@10068: wenzelm@9797: chown -R "$LOGNAME" "$DISTNAME" wenzelm@9797: chmod -R u+w "$DISTNAME" wenzelm@9797: chmod -R g=o "$DISTNAME" wenzelm@10077: chgrp -R isabelle "$DISTNAME" Isabelle wenzelm@2667: wenzelm@9797: mkdir -p "pdf/$DISTNAME/doc" wenzelm@9797: mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc" wenzelm@6748: haftmann@16508: #~ page/bin/mkcontents "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc/index" haftmann@16508: #~ cat > "pdf/$DISTNAME/doc/index.html" < haftmann@16508: #~ haftmann@16508: #~ $DISTNAME Documentation haftmann@16508: #~ haftmann@16508: #~ haftmann@16508: #~

$DISTNAME Documentation

haftmann@16508: #~ $(cat "pdf/$DISTNAME/doc/index") haftmann@16508: #~ haftmann@16508: #~ haftmann@16508: #~ EOF haftmann@16508: #~ rm "pdf/$DISTNAME/doc/index" wenzelm@10928: wenzelm@10096: echo "$DISTNAME.tar.gz" wenzelm@10077: "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME" wenzelm@10096: gzip "$DISTNAME.tar" wenzelm@10096: wenzelm@10096: echo "${DISTNAME}_pdf.tar.gz" wenzelm@10112: ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; ) wenzelm@10096: gzip "${DISTNAME}_pdf.tar" wenzelm@6748: wenzelm@10928: mv "pdf/$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc/index.html" "$DISTNAME/doc" wenzelm@9797: rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf wenzelm@6750: wenzelm@6304: wenzelm@9782: # cleanup dist wenzelm@9782: wenzelm@9797: mv "$DISTNAME" "${DISTNAME}-old" wenzelm@9797: mkdir "$DISTNAME" wenzelm@9782: haftmann@16328: mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \ wenzelm@17554: "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \ wenzelm@17554: "$DISTNAME" wenzelm@9797: mkdir "$DISTNAME/doc" wenzelm@10928: mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/index.html" "$DISTNAME/doc" wenzelm@9782: wenzelm@9867: chgrp -R isabelle "$DISTNAME" wenzelm@9867: wenzelm@9797: rm -rf "${DISTNAME}-old" wenzelm@9782: wenzelm@9782: wenzelm@2667: # final note wenzelm@2667: wenzelm@9797: echo "###" wenzelm@10112: echo "### Finished makedist." wenzelm@9797: echo "###"