Admin/makedist

 # makedist -- make Isabelle source distribution.
 
 
 ## global settings
 
+DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
 LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL ZF"
 
-case $(hostname) in
-  *lapbroy*)
-    export CVSROOT=sunbroy2:/usr/proj/isabelle-repository/archive
-    ;;
-  *broy*)
-    export CVSROOT=/usr/proj/isabelle-repository/archive
-    ;;
-  *)
-    export CVSROOT=sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/archive
-    ;;
-esac
-
-DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
+export CVSROOT=/usr/proj/isabelle-repository/archive
+[ ! -d "$CVSROOT" ] && CVSROOT="sunbroy2.informatik.tu-muenchen.de:$CVSROOT"
 
 umask 022
 
 TAR=tar
 type -path gtar >/dev/null && TAR=gtar

 
 function usage()
 {
   cat <<EOF
 
-Usage: $PRG VERSION
+Usage: $PRG VERSION [NAME]
 
   Make Isabelle distribution from the master sources at TUM.
 
-  VERSION may be either a tag like "Isabelle2002-XX" that specifies the
+  VERSION may be either a tag like "Isabelle2005" that specifies the
   release to be exported from the repository, or "-" to checkout the
-  current sources as an unofficial release, or "--" to produce a
-  tentative release from the present copy of the Isabelle repository.
+  current sources as an unofficial release.
+
+  NAME specifies an explicit distribution name, by default it is
+  derived from VERSION.
 
   Checklist for official releases (before running this script):
 
-    * Check Admin/page contents.
-    * Check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.
+    * Check Admin/website contents.
+    * Check ANNOUNCE, README.html, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.
     * Try "isatool makeall all" with Poly/ML, SML/NJ, etc.
     * Tag the current repository version, e.g.:
-        cvs -d /usr/proj/isabelle-repository/archive rtag Isabelle2002 isabelle
+        cvs -d /usr/proj/isabelle-repository/archive rtag Isabelle2005 isabelle
       PLEASE DO NOT DO THIS UNLESS YOU KNOW WHAT YOU ARE DOING!
 
 EOF
   exit 1
 }

 }
 
 
 ## process command line
 
-[ "$#" -ne 1 ] && usage
-
-VERSION="$1"
-shift
+[ "$#" -ne 1 -a "$#" -ne 2 ] && usage
+
+VERSION="$1"; shift
+
+if [ "$#" -eq 0 ]; then
+  DISTNAME=""
+else
+  DISTNAME="$1"; shift
+fi
 
 
 ## main
 
 # dist version
 
 DATE=$(date "+%d-%b-%Y")
 DISTDATE=$(date "+%B %Y")
 
-if [ "$VERSION" = "--" ]; then
-  DISTNAME="Isabelle_$DATE"
-  DISTVERSION="$DISTNAME"
-  EXPORT="$THIS/cvs-copy $THIS/.. $DISTNAME"
-  UNOFFICIAL="unofficial test"
-elif [ "$VERSION" = "-" ]; then
-  DISTNAME="Isabelle_$DATE"
+if [ "$VERSION" = "-" ]; then
+  DISTIDENT="Isabelle_$DATE"
+  [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
   DISTVERSION="$DISTNAME"
   EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle"
   UNOFFICIAL="unofficial"
 else
-  DISTNAME="$VERSION"
+  DISTIDENT="$VERSION"
+  [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
   DISTVERSION="$DISTNAME: $DISTDATE"
-  EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle"
+  EXPORT="cvs -f -q export -P -r $VERSION -d $DISTNAME isabelle"
   UNOFFICIAL=""
 fi
 
 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
 mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!"

 
 
 # export repository
 
 echo "###"
-echo "### Exporting $DISTNAME ..."
+echo "### Exporting $DISTIDENT ..."
 echo "###"
 
 cd "$DISTBASE"
 
 $EXPORT || fail "Export failed!"

   cd ..
 fi
 
 $FIND . -name CVS -print | xargs rm -rf
 $FIND . -name .cvsignore -print | xargs rm -rf
-$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
-$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
-$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
-$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
-$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
+$FIND . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x
 
 
 # build docs
 
 echo "###"

 
 for DOC in $(cat Contents)
 do
   cd "$DOC"
   make dvi || fail "DVI document for $DOC failed!"
-  ([ -n "$PDFLATEX" ] && make clean pdf) || fail "PDF document for $DOC failed!"
+  { [ -n "$PDFLATEX" ] && make clean pdf; } || fail "PDF document for $DOC failed!"
   cd ..
 done
 
 
 # prepare dist dir for release
 
 echo "###"
 echo "### Preparing distribution ..."
 echo "###"
 
-cd "$DISTBASE/$DISTNAME" || fail "Something is wrong: dist directory doesn't exist!"
-
-#~ # old site framework
-#~ cp -R Admin/page ..
-#~ cp Distribution/doc/Contents ../page
-#~ cp Distribution/lib/logo/isabelle.gif ../page/main-content
-#~ cp Distribution/lib/logo/isabelle.gif ../page/dist-content
-#~ echo "$DISTNAME" > ../page/DISTNAME
-# new site framework
+cd "$DISTBASE/$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
+
 cp -R Admin/website ..
 mkdir -p ../website/conf
 cat > ../website/conf/distname.mak <<EOF
-# this is a generated file - do not edit unless you know what you are doing
+# this is a generated file - do not edit!
 
 DISTNAME=$DISTNAME
+DISTIDENT=$DISTIDENT
 EOF
 
 MOVE=$($FIND Doc \( -type f -a -not -type l -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
 mv -f $MOVE Distribution/doc
 rm Distribution/doc/Isa-logics.eps

   {
     echo
     echo "IMPORTANT NOTE"
     echo "=============="
     echo
-    echo "This is an $UNOFFICIAL release of Isabelle, created by $LOGNAME $DATE."
+    echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
     echo
   } >ANNOUNCE
 fi
 
 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
-perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML
-perl -pi -e "s/Isabelle repository version/$DISTVERSION/" lib/Tools/version
+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.html
 lynx -dump README.html >README
 
 ( cd src; ../Admin/maketags; )
 

 
 mv "$DISTNAME" "${DISTNAME}-old"
 mkdir "$DISTNAME"
 
 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
-   "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
-   "$DISTNAME"
+  "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
+  "$DISTNAME"
 mkdir "$DISTNAME/doc"
 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/index.html" "$DISTNAME/doc"
 
 chgrp -R isabelle "$DISTNAME"