Admin/makedist
author mehta
Fri Apr 16 15:46:50 2004 +0200 (2004-04-16)
changeset 14591 7be4d5dadf15
parent 13803 84cb1ff80f25
child 15438 dfc7d2a824d6
permissions -rwxr-xr-x
lemma drop_Suc_conv_tl added.
     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.
    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 $FIND . -name CVS -print | xargs rm -rf
   121 $FIND . -name .cvsignore -print | xargs rm -rf
   122 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
   123 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
   124 $FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
   125 
   126 
   127 # build docs
   128 
   129 echo "###"
   130 echo "### Building docs ..."
   131 echo "###"
   132 
   133 cd "$DISTBASE/$DISTNAME/Doc"
   134 PDFLATEX=$(type -path pdflatex)
   135 
   136 for DOC in $(cat Contents)
   137 do
   138   cd "$DOC"
   139   make dvi || fail "DVI document for $DOC failed!"
   140   ([ -n "$PDFLATEX" ] && make clean pdf) || fail "PDF document for $DOC failed!"
   141   cd ..
   142 done
   143 
   144 
   145 # prepare dist dir for release
   146 
   147 echo "###"
   148 echo "### Preparing distribution ..."
   149 echo "###"
   150 
   151 cd "$DISTBASE/$DISTNAME" || fail "Something is wrong: dist directory doesn't exist!"
   152 
   153 cp -R Admin/page ..
   154 cp Distribution/doc/Contents ../page
   155 cp Distribution/lib/logo/isabelle.gif ../page/main-content
   156 cp Distribution/lib/logo/isabelle.gif ../page/dist-content
   157 echo "$DISTNAME" > ../page/DISTNAME
   158 
   159 MOVE=$($FIND Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
   160 mv -f $MOVE Distribution/doc
   161 rm Distribution/doc/Isa-logics.eps
   162 rm -rf Doc Tools
   163 
   164 mkdir src contrib
   165 mv $LOGICS src
   166 
   167 mv Distribution/* .
   168 rmdir Distribution
   169 
   170 ( cd lib/browser; make; ) || fail "Graph browser build failed!"
   171 
   172 cp doc/isabelle*.eps lib/logo
   173 
   174 
   175 if [ -n "$UNOFFICIAL" ]; then
   176   {
   177     echo
   178     echo "IMPORTANT NOTE"
   179     echo "=============="
   180     echo
   181     echo "This is an $UNOFFICIAL release of Isabelle, created by $LOGNAME $DATE."
   182     echo
   183   } >ANNOUNCE
   184 fi
   185 
   186 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
   187 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML
   188 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" lib/Tools/version
   189 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
   190 lynx -dump README.html >README
   191 
   192 ( cd src; ../Admin/maketags; )
   193 
   194 rm -rf Admin
   195 
   196 
   197 # create archive
   198 
   199 echo "###"
   200 echo "### Creating archives ..."
   201 echo "###"
   202 
   203 cd "$DISTBASE"
   204 
   205 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
   206 
   207 rm -f Isabelle
   208 ln -s "$DISTNAME" Isabelle
   209 
   210 chown -R "$LOGNAME" "$DISTNAME"
   211 chmod -R u+w "$DISTNAME"
   212 chmod -R g=o "$DISTNAME"
   213 chgrp -R isabelle "$DISTNAME" Isabelle
   214 
   215 mkdir -p "pdf/$DISTNAME/doc"
   216 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
   217 
   218 page/bin/mkcontents "$DISTNAME/doc/Contents" "pdf/$DISTNAME/doc/index"
   219 cat > "pdf/$DISTNAME/doc/index.html" <<EOF
   220 <html>
   221 <head>
   222 <title>$DISTNAME Documentation</title>
   223 </head>
   224 <body>
   225 <h1>$DISTNAME Documentation</h1>
   226 $(cat "pdf/$DISTNAME/doc/index")
   227 </body>
   228 </html>
   229 EOF
   230 rm "pdf/$DISTNAME/doc/index"
   231 
   232 echo "$DISTNAME.tar.gz"
   233 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
   234 gzip "$DISTNAME.tar"
   235 
   236 echo "${DISTNAME}_pdf.tar.gz"
   237 ( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
   238 gzip "${DISTNAME}_pdf.tar"
   239 
   240 mv "pdf/$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc/index.html" "$DISTNAME/doc"
   241 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
   242 
   243 
   244 # cleanup dist
   245 
   246 mv "$DISTNAME" "${DISTNAME}-old"
   247 mkdir "$DISTNAME"
   248 
   249 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" "$DISTNAME"
   250 mkdir "$DISTNAME/doc"
   251 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/index.html" "$DISTNAME/doc"
   252 
   253 chgrp -R isabelle "$DISTNAME"
   254 
   255 rm -rf "${DISTNAME}-old"
   256 
   257 
   258 # final note
   259 
   260 echo "###"
   261 echo "### Finished makedist."
   262 echo "###"