Admin/makedist
author wenzelm
Mon Jan 02 20:50:17 2006 +0100 (2006-01-02)
changeset 18539 35b9ed76b59a
parent 17942 68988fd2fd27
child 20990 0c1296049b47
permissions -rwxr-xr-x
ISABELLE_USER for remote cvs access;
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 #
     5 # makedist -- make Isabelle source distribution.
     6 
     7 
     8 ## global settings
     9 
    10 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
    11 LOGICS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents TFL ZF"
    12 
    13 export CVSROOT=/usr/proj/isabelle-repository/archive
    14 [ ! -d "$CVSROOT" ] && CVSROOT="${ISABELLE_USER:-$USER}@sunbroy2.informatik.tu-muenchen.de:$CVSROOT"
    15 
    16 umask 022
    17 
    18 TAR=tar
    19 type -path gtar >/dev/null && TAR=gtar
    20 
    21 FIND=find
    22 type -path gfind >/dev/null && FIND=gfind
    23 
    24 
    25 ## diagnostics
    26 
    27 PRG=$(basename "$0")
    28 THIS=$(cd $(dirname "$0"); echo "$PWD")
    29 
    30 function usage()
    31 {
    32   cat <<EOF
    33 
    34 Usage: $PRG VERSION [NAME]
    35 
    36   Make Isabelle distribution from the master sources at TUM.
    37 
    38   VERSION may be either a tag like "IsabelleXXXX" that specifies the
    39   release to be exported from the repository, or "-" to checkout the
    40   current sources as an unofficial release.
    41 
    42   NAME specifies an explicit distribution name, by default it is
    43   derived from VERSION.
    44 
    45   Checklist for official releases (before running this script):
    46 
    47     * Check Admin/website contents.
    48     * Check ANNOUNCE, README.html, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.
    49     * Try "isatool makeall all" with Poly/ML, SML/NJ, etc.
    50     * Tag the current repository version, e.g.:
    51         cvs -d /usr/proj/isabelle-repository/archive rtag IsabelleXXXX isabelle
    52       PLEASE DO NOT DO THIS UNLESS YOU KNOW WHAT YOU ARE DOING!
    53 
    54 EOF
    55   exit 1
    56 }
    57 
    58 function fail()
    59 {
    60   echo "$1" >&2
    61   exit 2
    62 }
    63 
    64 
    65 ## process command line
    66 
    67 [ "$#" -ne 1 -a "$#" -ne 2 ] && usage
    68 
    69 VERSION="$1"; shift
    70 
    71 if [ "$#" -eq 0 ]; then
    72   DISTNAME=""
    73 else
    74   DISTNAME="$1"; shift
    75 fi
    76 
    77 
    78 ## main
    79 
    80 # dist version
    81 
    82 DATE=$(date "+%d-%b-%Y")
    83 DISTDATE=$(date "+%B %Y")
    84 
    85 if [ "$VERSION" = "-" ]; then
    86   DISTIDENT="Isabelle_$DATE"
    87   [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
    88   DISTVERSION="$DISTNAME"
    89   EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle"
    90   UNOFFICIAL=true
    91 else
    92   DISTIDENT="$VERSION"
    93   [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
    94   DISTVERSION="$DISTNAME: $DISTDATE"
    95   EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle"
    96   UNOFFICIAL=""
    97 fi
    98 
    99 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
   100 mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!"
   101 [ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!"
   102 [ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!"
   103 
   104 
   105 # export repository
   106 
   107 echo "###"
   108 echo "### Exporting $DISTIDENT ..."
   109 echo "###"
   110 
   111 cd "$DISTBASE"
   112 
   113 $EXPORT || fail "Export failed!"
   114 
   115 if [ -n "$CVS2CL" ]; then
   116   cd $DISTNAME
   117   $CVS2CL
   118   gzip ChangeLog
   119   mv ChangeLog.gz ..
   120   cd ..
   121 fi
   122 
   123 $FIND . -name CVS -print | xargs rm -rf
   124 $FIND . -name .cvsignore -print | xargs rm -rf
   125 $FIND . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x
   126 
   127 
   128 # build docs
   129 
   130 echo "###"
   131 echo "### Building docs ..."
   132 echo "###"
   133 
   134 cd "$DISTBASE/$DISTNAME/Doc"
   135 PDFLATEX=$(type -path pdflatex)
   136 
   137 for DOC in $(cat Contents)
   138 do
   139   cd "$DOC"
   140   make dvi || fail "DVI document for $DOC failed!"
   141   { [ -n "$PDFLATEX" ] && make clean pdf; } || fail "PDF document for $DOC failed!"
   142   cd ..
   143 done
   144 
   145 
   146 # prepare dist dir for release
   147 
   148 echo "###"
   149 echo "### Preparing distribution ..."
   150 echo "###"
   151 
   152 cd "$DISTBASE/$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
   153 
   154 cp -R Admin/website ..
   155 mkdir -p ../website/conf
   156 cat > ../website/conf/distinfo.mak <<EOF
   157 # this is a generated file - do not edit unless you know what you are doing!
   158 
   159 DISTNAME=$DISTNAME
   160 DISTIDENT=$DISTIDENT
   161 DISTBASE=$DISTBASE
   162 EOF
   163 
   164 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')
   165 mv -f $MOVE Distribution/doc
   166 rm Distribution/doc/Isa-logics.eps
   167 rm -rf Doc Tools
   168 
   169 mkdir src contrib
   170 mv $LOGICS src
   171 
   172 mv Distribution/* .
   173 rmdir Distribution
   174 
   175 ( cd lib/browser; make; ) || fail "Graph browser build failed!"
   176 
   177 cp doc/isabelle*.eps lib/logo
   178 
   179 
   180 if [ -n "$UNOFFICIAL" ]; then
   181   {
   182     echo
   183     echo "IMPORTANT NOTE"
   184     echo "=============="
   185     echo
   186     echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
   187     echo
   188   } >ANNOUNCE
   189 fi
   190 
   191 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
   192 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version
   193 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
   194 lynx -dump README.html >README
   195 
   196 ( cd src; ../Admin/maketags; )
   197 
   198 rm -rf Admin
   199 rm -f TODO
   200 
   201 
   202 # create archive
   203 
   204 echo "###"
   205 echo "### Creating archives ..."
   206 echo "###"
   207 
   208 cd "$DISTBASE"
   209 
   210 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
   211 
   212 rm -f Isabelle
   213 ln -s "$DISTNAME" Isabelle
   214 
   215 chown -R "$LOGNAME" "$DISTNAME"
   216 chmod -R u+w "$DISTNAME"
   217 chmod -R g=o "$DISTNAME"
   218 chgrp -R isabelle "$DISTNAME" Isabelle
   219 
   220 mkdir -p "pdf/$DISTNAME/doc"
   221 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
   222 
   223 sync; sleep 3
   224 
   225 echo "$DISTNAME.tar.gz"
   226 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
   227 gzip "$DISTNAME.tar"
   228 
   229 echo "${DISTNAME}_pdf.tar.gz"
   230 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
   231 gzip "${DISTNAME}_pdf.tar"
   232 
   233 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
   234 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
   235 
   236 
   237 # cleanup dist
   238 
   239 mv "$DISTNAME" "${DISTNAME}-old"
   240 mkdir "$DISTNAME"
   241 
   242 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
   243   "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
   244   "$DISTNAME"
   245 mkdir "$DISTNAME/doc"
   246 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
   247 
   248 chgrp -R isabelle "$DISTNAME"
   249 
   250 rm -rf "${DISTNAME}-old"
   251 
   252 
   253 # final note
   254 
   255 echo "###"
   256 echo "### Finished makedist."
   257 echo "###"