Admin/makedist
author wenzelm
Thu Oct 04 14:42:11 2007 +0200 (2007-10-04)
changeset 24829 e1214fa781ca
parent 23895 89f8bfdbc269
child 25214 91730b492a45
permissions -rwxr-xr-x
avoid gensym;
     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 SRCS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents Tools 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     * Symlink website to Admin/website
    48     * Check Admin/website contents.
    49     * Check ANNOUNCE, README.html, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS.
    50     * Try "isatool makeall all" with Poly/ML, SML/NJ, etc.
    51     * Tag the current repository version, e.g.:
    52         cvs -d /usr/proj/isabelle-repository/archive rtag IsabelleXXXX isabelle
    53       PLEASE DO NOT DO THIS UNLESS YOU KNOW WHAT YOU ARE DOING!
    54 
    55 EOF
    56   exit 1
    57 }
    58 
    59 function fail()
    60 {
    61   echo "$1" >&2
    62   exit 2
    63 }
    64 
    65 
    66 ## process command line
    67 
    68 [ "$#" -ne 1 -a "$#" -ne 2 ] && usage
    69 
    70 VERSION="$1"; shift
    71 
    72 if [ "$#" -eq 0 ]; then
    73   DISTNAME=""
    74 else
    75   DISTNAME="$1"; shift
    76 fi
    77 
    78 
    79 ## main
    80 
    81 # dist version
    82 
    83 DATE=$(env LC_ALL=C date "+%d-%b-%Y")
    84 DISTDATE=$(env LC_ALL=C date "+%B %Y")
    85 
    86 if [ "$VERSION" = "-" ]; then
    87   DISTIDENT="Isabelle_$DATE"
    88   [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
    89   DISTVERSION="$DISTNAME"
    90   EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle"
    91   UNOFFICIAL=true
    92 else
    93   DISTIDENT="$VERSION"
    94   [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
    95   DISTVERSION="$DISTNAME: $DISTDATE"
    96   EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle"
    97   UNOFFICIAL=""
    98 fi
    99 
   100 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
   101 mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!"
   102 [ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!"
   103 [ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!"
   104 
   105 
   106 # export repository
   107 
   108 echo "###"
   109 echo "### Exporting $DISTIDENT ..."
   110 echo "###"
   111 
   112 cd "$DISTBASE"
   113 
   114 $EXPORT || fail "Export failed!"
   115 
   116 if [ -n "$CVS2CL" ]; then
   117   cd $DISTNAME
   118   $CVS2CL
   119   gzip ChangeLog
   120   mv ChangeLog.gz ..
   121   cd ..
   122 fi
   123 
   124 $FIND . -name CVS -print | xargs rm -rf
   125 $FIND . -name .cvsignore -print | xargs rm -rf
   126 $FIND . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x
   127 $FIND . -print | xargs chmod u+rw
   128 
   129 
   130 # build docs
   131 
   132 echo "###"
   133 echo "### Building docs ..."
   134 echo "###"
   135 
   136 cd "$DISTBASE/$DISTNAME/Doc"
   137 PDFLATEX=$(type -path pdflatex)
   138 
   139 for DOC in $(cat Contents)
   140 do
   141   pushd "$DOC" > /dev/null
   142   make dvi || fail "DVI document for $DOC failed!"
   143   { [ -n "$PDFLATEX" ] && make clean pdf; } || fail "PDF document for $DOC failed!"
   144   popd
   145 done
   146 
   147 
   148 # prepare dist dir for release
   149 
   150 echo "###"
   151 echo "### Preparing distribution ..."
   152 echo "###"
   153 
   154 cd "$DISTBASE/$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
   155 
   156 cp -R Admin/website ..
   157 mkdir -p ../website/conf
   158 cat > ../website/conf/distinfo.mak <<EOF
   159 # this is a generated file - do not edit unless you know what you are doing!
   160 
   161 DISTNAME=$DISTNAME
   162 DISTIDENT=$DISTIDENT
   163 DISTBASE=$DISTBASE
   164 EOF
   165 
   166 MOVE=$($FIND Doc \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
   167 mv -f $MOVE Distribution/doc
   168 rm Distribution/doc/Isa-logics.eps
   169 rm -rf Doc
   170 
   171 mkdir src contrib
   172 mv $SRCS src
   173 
   174 mv Distribution/* .
   175 rmdir Distribution
   176 
   177 ( cd lib/browser; make; ) || fail "Graph browser build failed!"
   178 
   179 cp doc/isabelle*.eps lib/logo
   180 
   181 
   182 if [ -n "$UNOFFICIAL" ]; then
   183   {
   184     echo
   185     echo "IMPORTANT NOTE"
   186     echo "=============="
   187     echo
   188     echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
   189     echo
   190   } >ANNOUNCE
   191 fi
   192 
   193 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
   194 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version
   195 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
   196 lynx -dump README.html >README
   197 
   198 ( cd src; ../Admin/maketags; )
   199 
   200 rm -rf Admin
   201 rm -f TODO
   202 
   203 
   204 # create archive
   205 
   206 echo "###"
   207 echo "### Creating archives ..."
   208 echo "###"
   209 
   210 cd "$DISTBASE"
   211 
   212 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
   213 
   214 rm -f Isabelle
   215 ln -s "$DISTNAME" Isabelle
   216 
   217 chown -R "$LOGNAME" "$DISTNAME"
   218 chmod -R u+w "$DISTNAME"
   219 chmod -R g=o "$DISTNAME"
   220 chgrp -R isabelle "$DISTNAME" Isabelle
   221 
   222 mkdir -p "pdf/$DISTNAME/doc"
   223 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
   224 
   225 sync; sleep 3
   226 
   227 echo "$DISTNAME.tar.gz"
   228 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
   229 gzip "$DISTNAME.tar"
   230 
   231 echo "${DISTNAME}_pdf.tar.gz"
   232 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
   233 gzip "${DISTNAME}_pdf.tar"
   234 
   235 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
   236 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
   237 
   238 
   239 # cleanup dist
   240 
   241 mv "$DISTNAME" "${DISTNAME}-old"
   242 mkdir "$DISTNAME"
   243 
   244 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
   245   "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
   246   "$DISTNAME"
   247 mkdir "$DISTNAME/doc"
   248 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
   249 
   250 chgrp -R isabelle "$DISTNAME"
   251 
   252 rm -rf "${DISTNAME}-old"
   253 
   254 
   255 # final note
   256 
   257 echo "###"
   258 echo "### Finished makedist."
   259 echo "###"