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