Admin/makedist
changeset 28940 043a42ba2a4d
parent 27647 ee452b218407
parent 28932 ccaa3355f7d3
child 29637 da018485b89d
     1.1 --- a/Admin/makedist	Mon Dec 01 19:41:16 2008 +0100
     1.2 +++ b/Admin/makedist	Mon Dec 01 19:42:26 2008 +0100
     1.3 @@ -2,18 +2,13 @@
     1.4  #
     1.5  # $Id$
     1.6  #
     1.7 -# makedist -- make Isabelle source distribution.
     1.8 -
     1.9 +# makedist -- make Isabelle source distribution
    1.10  
    1.11  ## global settings
    1.12  
    1.13 +REPOS="http://isabelle.in.tum.de/repos/isabelle"
    1.14 +
    1.15  DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
    1.16 -SRCS="CCL CTT Cube FOL FOLP HOL HOLCF LCF Provers Pure Sequents Tools ZF"
    1.17 -
    1.18 -export CVSROOT=/home/isabelle-repository/archive
    1.19 -[ ! -d "$CVSROOT" ] && CVSROOT="${ISABELLE_USER:-$USER}@atbroy100.informatik.tu-muenchen.de:$CVSROOT"
    1.20 -
    1.21 -[ -z "$CVS2CL" ] && type -path cvs2cl >/dev/null && CVS2CL=cvs2cl
    1.22  
    1.23  umask 022
    1.24  
    1.25 @@ -27,16 +22,15 @@
    1.26  {
    1.27    cat <<EOF
    1.28  
    1.29 -Usage: $PRG VERSION [NAME]
    1.30 +Usage: $PRG [OPTIONS] [VERSION]
    1.31  
    1.32 -  Make Isabelle distribution from the master sources at TUM.
    1.33 +  Options are:
    1.34 +    -r RELEASE         proper release with name"
    1.35  
    1.36 -  VERSION may be either a tag like "IsabelleXXXX" that specifies the
    1.37 -  release to be exported from the repository, or "-" to checkout the
    1.38 -  current sources as an unofficial release.
    1.39 +  Make Isabelle distribution from the main Mercurial repository at TUM.
    1.40  
    1.41 -  NAME specifies an explicit distribution name, by default it is
    1.42 -  derived from VERSION.
    1.43 +  VERSION identifies the snapshot, using usual Mercurial terminology;
    1.44 +  the default is RELEASE if given, otherwise "tip".
    1.45  
    1.46  EOF
    1.47    exit 1
    1.48 @@ -51,131 +45,146 @@
    1.49  
    1.50  ## process command line
    1.51  
    1.52 -[ "$#" -ne 1 -a "$#" -ne 2 ] && usage
    1.53 +# options
    1.54  
    1.55 -VERSION="$1"; shift
    1.56 +RELEASE=""
    1.57  
    1.58 -if [ "$#" -eq 0 ]; then
    1.59 -  DISTNAME=""
    1.60 -else
    1.61 -  DISTNAME="$1"; shift
    1.62 -fi
    1.63 +while getopts "r:" OPT
    1.64 +do
    1.65 +  case "$OPT" in
    1.66 +    r)
    1.67 +      RELEASE="$OPTARG"
    1.68 +      ;;
    1.69 +    \?)
    1.70 +      usage
    1.71 +      ;;
    1.72 +  esac
    1.73 +done
    1.74 +
    1.75 +shift $(($OPTIND - 1))
    1.76 +
    1.77 +
    1.78 +# args
    1.79 +
    1.80 +VERSION=""
    1.81 +[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
    1.82 +[ -z "$VERSION" ] && VERSION="$RELEASE"
    1.83 +[ -z "$VERSION" ] && VERSION="tip"
    1.84 +
    1.85 +[ "$#" -gt 0 ] && usage
    1.86  
    1.87  
    1.88  ## main
    1.89  
    1.90 -# dist version
    1.91 +# tmp
    1.92 +
    1.93 +TMP="tmp-$USER$$"
    1.94 +function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
    1.95 +
    1.96 +
    1.97 +# retrieve archive and resolve version identifier
    1.98 +
    1.99 +mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
   1.100 +cd "$DISTPREFIX/$TMP"
   1.101 +
   1.102 +echo "###"
   1.103 +echo "### Retrieving Mercurial repository $VERSION"
   1.104 +echo "###"
   1.105 +
   1.106 +{ wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
   1.107 +  fail "Failed to retrieve $VERSION"
   1.108 +
   1.109 +IDENT=$(echo * | sed 's/isabelle-//')
   1.110 +
   1.111 +rm -f "isabelle-$IDENT/.hg_archival.txt"
   1.112 +rm -f "isabelle-$IDENT/.hgtags"
   1.113 +rm -f "isabelle-$IDENT/.hgignore"
   1.114 +rm -f "isabelle-$IDENT/README_REPOSITORY"
   1.115 +
   1.116 +
   1.117 +# dist name
   1.118  
   1.119  DATE=$(env LC_ALL=C date "+%d-%b-%Y")
   1.120  DISTDATE=$(env LC_ALL=C date "+%B %Y")
   1.121  
   1.122 -if [ "$VERSION" = "-" ]; then
   1.123 -  DISTIDENT="Isabelle_$DATE"
   1.124 -  [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
   1.125 -  DISTVERSION="$DISTNAME"
   1.126 -  EXPORT="cvs -f -q checkout -P -d $DISTNAME isabelle"
   1.127 -  UNOFFICIAL=true
   1.128 +if [ -z "$RELEASE" ]; then
   1.129 +  DISTNAME="Isabelle_$DATE"
   1.130 +  DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
   1.131  else
   1.132 -  DISTIDENT="$VERSION"
   1.133 -  [ -z "$DISTNAME" ] && DISTNAME="$DISTIDENT"
   1.134 +  DISTNAME="$RELEASE"
   1.135    DISTVERSION="$DISTNAME: $DISTDATE"
   1.136 -  EXPORT="cvs -f -q export -r $VERSION -d $DISTNAME isabelle"
   1.137 -  UNOFFICIAL=""
   1.138  fi
   1.139  
   1.140  DISTBASE="$DISTPREFIX/dist-$DISTNAME"
   1.141 -mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir $DISTBASE!"
   1.142 -[ -e "$DISTBASE/$DISTNAME" ] && fail "$DISTBASE/$DISTNAME already exists!"
   1.143 -[ -e "$DISTBASE/pdf/$DISTNAME" ] && fail "$DISTBASE/pdf/$DISTNAME already exists!"
   1.144 +mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
   1.145 +[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
   1.146 +[ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; }
   1.147  
   1.148 +cd "$DISTBASE"
   1.149 +mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
   1.150 +purge_tmp
   1.151  
   1.152 -# export repository
   1.153 +cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
   1.154 +
   1.155 +
   1.156 +# website
   1.157 +
   1.158 +mkdir -p ../website
   1.159 +cat > ../website/distinfo.mak <<EOF
   1.160 +# this is a generated file - do not edit unless you know what you are doing!
   1.161 +DISTNAME=$DISTNAME
   1.162 +DISTBASE=$DISTBASE
   1.163 +EOF
   1.164 +
   1.165 +cp lib/html/library_index_content.template ../website/
   1.166 +
   1.167 +
   1.168 +# prepare dist for release
   1.169  
   1.170  echo "###"
   1.171 -echo "### Exporting $DISTIDENT ..."
   1.172 +echo "### Preparing distribution $DISTNAME"
   1.173  echo "###"
   1.174  
   1.175 -cd "$DISTBASE"
   1.176 -
   1.177 -$EXPORT || fail "Export failed!"
   1.178 -
   1.179 -if [ -n "$CVS2CL" -a -n "$UNOFFICIAL" ]; then
   1.180 -  cd $DISTNAME
   1.181 -  $CVS2CL
   1.182 -  gzip ChangeLog
   1.183 -  cp ChangeLog.gz ..
   1.184 -  cd ..
   1.185 -fi
   1.186 -
   1.187 -find . -name CVS -print | xargs rm -rf
   1.188  find . -name .cvsignore -print | xargs rm -rf
   1.189  find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x
   1.190  find . -print | xargs chmod u+rw
   1.191  
   1.192 +./Admin/build all || fail "Failed to build distribution"
   1.193 +rm -rf Admin
   1.194  
   1.195 -# build components
   1.196 +MOVE=$(find doc-src \( -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')
   1.197 +mv -f $MOVE doc
   1.198 +rm doc/Isa-logics.eps
   1.199 +rm doc/codegen_process.pdf
   1.200 +rm -rf doc-src
   1.201  
   1.202 -"$DISTBASE/$DISTNAME/Admin/build" all || fail "Failed to build distribution"
   1.203 -
   1.204 -
   1.205 -# prepare dist dir for release
   1.206 -
   1.207 -echo "###"
   1.208 -echo "### Preparing distribution ..."
   1.209 -echo "###"
   1.210 -
   1.211 -cd "$DISTBASE/$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
   1.212 -
   1.213 -mkdir -p ../website
   1.214 -cat > ../website/distinfo.mak <<EOF
   1.215 -# this is a generated file - do not edit unless you know what you are doing!
   1.216 -
   1.217 -DISTNAME=$DISTNAME
   1.218 -DISTIDENT=$DISTIDENT
   1.219 -DISTBASE=$DISTBASE
   1.220 -EOF
   1.221 -
   1.222 -cp Distribution/lib/html/library_index_content.template ../website/
   1.223 -
   1.224 -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')
   1.225 -mv -f $MOVE Distribution/doc
   1.226 -rm Distribution/doc/Isa-logics.eps
   1.227 -rm Distribution/doc/codegen_process.pdf
   1.228 -rm -rf Doc
   1.229 -
   1.230 -mkdir src contrib
   1.231 -mv $SRCS src
   1.232 -
   1.233 -mv Distribution/* .
   1.234 -rmdir Distribution
   1.235 -
   1.236 +mkdir contrib
   1.237  
   1.238  cp doc/isabelle*.eps lib/logo
   1.239  
   1.240  
   1.241 -if [ -n "$UNOFFICIAL" ]; then
   1.242 +if [ -z "$RELEASE" ]; then
   1.243    {
   1.244      echo
   1.245      echo "IMPORTANT NOTE"
   1.246      echo "=============="
   1.247      echo
   1.248      echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
   1.249 +    echo "See $REPOS/log/$IDENT for details."
   1.250      echo
   1.251    } >ANNOUNCE
   1.252  else
   1.253 -  perl -pi -e "s/val is_official = false/val is_official = true/" src/Pure/ROOT.ML
   1.254 +  perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
   1.255  fi
   1.256  
   1.257 -perl -pi -e "s/ISABELLE_IDENTIFIER=\"\"/ISABELLE_IDENTIFIER=\"$DISTNAME\"/g;" lib/scripts/getsettings
   1.258 -perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/library_index_header.template
   1.259 -perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version
   1.260 -perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README
   1.261 +perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
   1.262 +perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
   1.263 +perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
   1.264 +perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
   1.265 +perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README
   1.266  
   1.267  
   1.268 -rm -rf Admin
   1.269 -
   1.270 -
   1.271 -# create archive
   1.272 +# create archives
   1.273  
   1.274  echo "###"
   1.275  echo "### Creating archives ..."
   1.276 @@ -184,6 +193,7 @@
   1.277  cd "$DISTBASE"
   1.278  
   1.279  echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
   1.280 +echo "$IDENT" >../ISABELLE_IDENT
   1.281  
   1.282  rm -f Isabelle
   1.283  ln -s "$DISTNAME" Isabelle
   1.284 @@ -197,12 +207,10 @@
   1.285  mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
   1.286  
   1.287  echo "$DISTNAME.tar.gz"
   1.288 -tar cf "$DISTNAME.tar" Isabelle "$DISTNAME"
   1.289 -gzip "$DISTNAME.tar"
   1.290 +tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
   1.291  
   1.292  echo "${DISTNAME}_pdf.tar.gz"
   1.293 -( cd pdf; tar cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
   1.294 -gzip "${DISTNAME}_pdf.tar"
   1.295 +tar -C pdf -czf "${DISTNAME}_pdf.tar.gz" "$DISTNAME"
   1.296  
   1.297  mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
   1.298  rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
   1.299 @@ -223,7 +231,3 @@
   1.300  
   1.301  rm -rf "${DISTNAME}-old"
   1.302  
   1.303 -
   1.304 -echo "###"
   1.305 -echo "### Finished makedist."
   1.306 -echo "###"