Admin/makedist
author huffman
Mon May 14 09:27:24 2007 +0200 (2007-05-14)
changeset 22961 e499ded5d0fc
parent 21712 8b2fd895a7fc
child 23149 ddc5800b699f
permissions -rwxr-xr-x
remove redundant lemmas
     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     * 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 
   128 
   129 # build docs
   130 
   131 echo "###"
   132 echo "### Building docs ..."
   133 echo "###"
   134 
   135 cd "$DISTBASE/$DISTNAME/Doc"
   136 PDFLATEX=$(type -path pdflatex)
   137 
   138 for DOC in $(cat Contents)
   139 do
   140   pushd "$DOC" > /dev/null
   141   make dvi || fail "DVI document for $DOC failed!"
   142   { [ -n "$PDFLATEX" ] && make clean pdf; } || fail "PDF document for $DOC failed!"
   143   popd
   144 done
   145 
   146 
   147 # prepare dist dir for release
   148 
   149 echo "###"
   150 echo "### Preparing distribution ..."
   151 echo "###"
   152 
   153 cd "$DISTBASE/$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
   154 
   155 cp -R Admin/website ..
   156 mkdir -p ../website/conf
   157 cat > ../website/conf/distinfo.mak <<EOF
   158 # this is a generated file - do not edit unless you know what you are doing!
   159 
   160 DISTNAME=$DISTNAME
   161 DISTIDENT=$DISTIDENT
   162 DISTBASE=$DISTBASE
   163 EOF
   164 
   165 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')
   166 mv -f $MOVE Distribution/doc
   167 rm Distribution/doc/Isa-logics.eps
   168 rm -rf Doc Tools
   169 
   170 mkdir src contrib
   171 mv $LOGICS src
   172 
   173 mv Distribution/* .
   174 rmdir Distribution
   175 
   176 ( cd lib/browser; make; ) || fail "Graph browser build failed!"
   177 
   178 cp doc/isabelle*.eps lib/logo
   179 
   180 
   181 if [ -n "$UNOFFICIAL" ]; then
   182   {
   183     echo
   184     echo "IMPORTANT NOTE"
   185     echo "=============="
   186     echo
   187     echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
   188     echo
   189   } >ANNOUNCE
   190 fi
   191 
   192 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
   193 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version
   194 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
   195 lynx -dump README.html >README
   196 
   197 ( cd src; ../Admin/maketags; )
   198 
   199 rm -rf Admin
   200 rm -f TODO
   201 
   202 
   203 # create archive
   204 
   205 echo "###"
   206 echo "### Creating archives ..."
   207 echo "###"
   208 
   209 cd "$DISTBASE"
   210 
   211 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
   212 
   213 rm -f Isabelle
   214 ln -s "$DISTNAME" Isabelle
   215 
   216 chown -R "$LOGNAME" "$DISTNAME"
   217 chmod -R u+w "$DISTNAME"
   218 chmod -R g=o "$DISTNAME"
   219 chgrp -R isabelle "$DISTNAME" Isabelle
   220 
   221 mkdir -p "pdf/$DISTNAME/doc"
   222 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
   223 
   224 sync; sleep 3
   225 
   226 echo "$DISTNAME.tar.gz"
   227 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
   228 gzip "$DISTNAME.tar"
   229 
   230 echo "${DISTNAME}_pdf.tar.gz"
   231 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
   232 gzip "${DISTNAME}_pdf.tar"
   233 
   234 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
   235 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
   236 
   237 
   238 # cleanup dist
   239 
   240 mv "$DISTNAME" "${DISTNAME}-old"
   241 mkdir "$DISTNAME"
   242 
   243 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
   244   "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
   245   "$DISTNAME"
   246 mkdir "$DISTNAME/doc"
   247 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
   248 
   249 chgrp -R isabelle "$DISTNAME"
   250 
   251 rm -rf "${DISTNAME}-old"
   252 
   253 
   254 # final note
   255 
   256 echo "###"
   257 echo "### Finished makedist."
   258 echo "###"