Admin/makedist
author wenzelm
Fri Oct 12 12:05:46 2001 +0200 (2001-10-12)
changeset 11724 f727aa96ae2e
parent 11392 3078f52ee552
child 11981 ad67e8d2c75f
permissions -rwxr-xr-x
declare impE iffD1 iffD2 as elim of Pure;
     1 #!/bin/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   *broy*)
    14     export CVSROOT=/usr/proj/isabelle-repository/archive
    15     ;;
    16   *.cl.cam.ac.uk)
    17     export CVSROOT=sunbroy1.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/archive
    18     ;;
    19 esac
    20 
    21 DISTPREFIX=~/tmp/isadist
    22 
    23 umask 022
    24 
    25 TAR=tar
    26 type -path gtar >/dev/null && TAR=gtar
    27 
    28 FIND=find
    29 type -path gfind >/dev/null && FIND=gfind
    30 
    31 
    32 ## diagnostics
    33 
    34 PRG=$(basename "$0")
    35 THIS=$(cd $(dirname "$0"); echo "$PWD")
    36 
    37 function usage()
    38 {
    39   cat <<EOF
    40 
    41 Usage: $PRG VERSION
    42 
    43   Make Isabelle distribution from the master sources at TUM.
    44 
    45   VERSION may be either a tag like "Isabelle99-XX" that specifies the
    46   release to be exported from the repository, or "-" to checkout the
    47   current sources as an unofficial release, or "--" to produce a
    48   tentative release from the present copy of the Isabelle repository.
    49 
    50   Checklist for official releases (before running this script):
    51 
    52     * Check Admin/page contents.
    53     * Check ANNOUNCE, README, INSTALL, NEWS.
    54     * Try "isatool makeall all" with Poly/ML, SML/NJ, etc.
    55     * Tag the current repository version, e.g.:
    56         cvs -d /usr/proj/isabelle-repository/archive rtag Isabelle99-X isabelle
    57       PLEASE DO NOT DO THIS UNLESS YOU KNOW WHAT YOU ARE DOING!
    58 
    59 EOF
    60   exit 1
    61 }
    62 
    63 function fail()
    64 {
    65   echo "$1" >&2
    66   exit 2
    67 }
    68 
    69 
    70 ## process command line
    71 
    72 [ "$#" -ne 1 ] && usage
    73 
    74 VERSION="$1"
    75 shift
    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   DISTNAME="Isabelle_$DATE"
    87   DISTVERSION="$DISTNAME"
    88   EXPORT="$THIS/cvs-copy $THIS/.. $DISTNAME"
    89   UNOFFICIAL="unofficial test"
    90 elif [ "$VERSION" = "-" ]; then
    91   DISTNAME="Isabelle_$DATE"
    92   DISTVERSION="$DISTNAME"
    93   EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle"
    94   UNOFFICIAL="unofficial"
    95 else
    96   DISTNAME="$VERSION"
    97   DISTVERSION="$DISTNAME: $DISTDATE"
    98   EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle"
    99   UNOFFICIAL=""
   100 fi
   101 
   102 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
   103 mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!"
   104 [ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!"
   105 [ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!"
   106 
   107 
   108 # export repository
   109 
   110 echo "###"
   111 echo "### Exporting $DISTNAME ..."
   112 echo "###"
   113 
   114 cd "$DISTBASE"
   115 
   116 $EXPORT
   117 $FIND . -name CVS -print | xargs rm -rf
   118 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
   119 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
   120 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
   121 
   122 
   123 # build docs
   124 
   125 echo "###"
   126 echo "### Building docs ..."
   127 echo "###"
   128 
   129 cd "$DISTBASE/$DISTNAME/Doc"
   130 PDFLATEX=$(type -path pdflatex)
   131 
   132 for DOC in $(cat Contents)
   133 do
   134   cd "$DOC"
   135   make dvi
   136   [ -n "$PDFLATEX" ] && make clean pdf
   137   cd ..
   138 done
   139 
   140 
   141 # prepare dist dir for release
   142 
   143 echo "###"
   144 echo "### Preparing distribution ..."
   145 echo "###"
   146 
   147 cd "$DISTBASE/$DISTNAME"
   148 
   149 cp -R Admin/page ..
   150 cp Distribution/doc/Contents ../page
   151 cp Distribution/lib/logo/isabelle.gif ../page/main-content
   152 cp Distribution/lib/logo/isabelle.gif ../page/dist-content
   153 echo "$DISTNAME" > ../page/DISTNAME
   154 
   155 MOVE=$($FIND Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
   156 mv -f $MOVE Distribution/doc
   157 rm Distribution/doc/Isa-logics.eps
   158 rm -rf Doc Tools
   159 
   160 mkdir src contrib
   161 mv $LOGICS src
   162 
   163 mv Distribution/* .
   164 rmdir Distribution
   165 
   166 ( cd lib/browser; make; )
   167 
   168 cp doc/isabelle*.eps lib/logo
   169 
   170 
   171 if [ -n "$UNOFFICIAL" ]; then
   172   {
   173     echo
   174     echo "IMPORTANT NOTE"
   175     echo "=============="
   176     echo
   177     echo "This is an $UNOFFICIAL release of Isabelle, created by $LOGNAME $DATE."
   178     echo
   179   } >ANNOUNCE
   180 fi
   181 
   182 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
   183 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML
   184 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
   185 lynx -dump README.html >README
   186 
   187 ( cd src; ../Admin/maketags; )
   188 
   189 rm -rf Admin
   190 
   191 
   192 # create archive
   193 
   194 echo "###"
   195 echo "### Creating archives ..."
   196 echo "###"
   197 
   198 cd "$DISTBASE"
   199 
   200 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
   201 
   202 rm -f Isabelle
   203 ln -s "$DISTNAME" Isabelle
   204 
   205 chown -R "$LOGNAME" "$DISTNAME"
   206 chmod -R u+w "$DISTNAME"
   207 chmod -R g=o "$DISTNAME"
   208 chgrp -R isabelle "$DISTNAME" Isabelle
   209 
   210 mkdir -p "pdf/$DISTNAME/doc"
   211 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
   212 
   213 page/bin/mkcontents "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc/index"
   214 cat > "pdf/$DISTNAME/doc/index.html" <<EOF
   215 <html>
   216 <head>
   217 <title>$DISTNAME Documentation</title>
   218 </head>
   219 <body>
   220 <h1>$DISTNAME Documentation</h1>
   221 $(cat "pdf/$DISTNAME/doc/index")
   222 </body>
   223 </html>
   224 EOF
   225 rm "pdf/$DISTNAME/doc/index"
   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 "pdf/$DISTNAME/doc/index.html" "$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" "${DISTNAME}-old/ANNOUNCE" "$DISTNAME"
   245 mkdir "$DISTNAME/doc"
   246 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/index.html" "$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 "###"