Admin/makedist_mercurial
author ballarin
Fri Aug 01 18:10:52 2008 +0200 (2008-08-01)
changeset 27717 21bbd410ba04
parent 27654 0f8e2dcabbf9
child 27725 6d133c2b681f
permissions -rwxr-xr-x
Generalised polynomial lemmas from cring to ring.
     1 #!/usr/bin/env bash
     2 #
     3 # $Id$
     4 #
     5 # makedist_mercurial -- make Isabelle source distribution (via Mercurial)
     6 
     7 ## global settings
     8 
     9 REPOS="http://isabelle.in.tum.de/isabelle-bin/mercurial.cgi"
    10 
    11 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
    12 
    13 umask 022
    14 
    15 
    16 ## diagnostics
    17 
    18 PRG=$(basename "$0")
    19 THIS=$(cd $(dirname "$0"); echo "$PWD")
    20 
    21 function usage()
    22 {
    23   cat <<EOF
    24 
    25 Usage: $PRG [OPTIONS] [VERSION]
    26 
    27   Options are:
    28     -r RELEASE         proper release with name"
    29 
    30   Make Isabelle distribution from the main Mercurial repository at TUM.
    31 
    32   VERSION identifies the snapshot, using usual Mercurial terminology;
    33   the default is RELEASE if given, otherwise "tip".
    34 
    35 EOF
    36   exit 1
    37 }
    38 
    39 function fail()
    40 {
    41   echo "$1" >&2
    42   exit 2
    43 }
    44 
    45 
    46 ## process command line
    47 
    48 # options
    49 
    50 RELEASE=""
    51 
    52 while getopts "r:" OPT
    53 do
    54   case "$OPT" in
    55     r)
    56       RELEASE="$OPTARG"
    57       ;;
    58     \?)
    59       usage
    60       ;;
    61   esac
    62 done
    63 
    64 shift $(($OPTIND - 1))
    65 
    66 
    67 # args
    68 
    69 VERSION=""
    70 [ "$#" -gt 0 ] && { VERSION="$1"; shift; }
    71 [ -z "$VERSION" ] && VERSION="$RELEASE"
    72 [ -z "$VERSION" ] && VERSION="tip"
    73 
    74 [ "$#" -gt 0 ] && usage
    75 
    76 
    77 ## main
    78 
    79 # tmp
    80 
    81 TMP="tmp-$USER$$"
    82 function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
    83 
    84 
    85 # retrieve archive and resolve version identifier
    86 
    87 mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
    88 cd "$DISTPREFIX/$TMP"
    89 
    90 echo "###"
    91 echo "### Retrieving Mercurial snapshot $VERSION"
    92 echo "###"
    93 
    94 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
    95   fail "Failed to retrieve $VERSION"
    96 
    97 IDENT=$(echo * | sed 's/Isabelle-repository-//')
    98 
    99 rm -f "Isabelle-repository-$IDENT/.hg_archival.txt"
   100 rm -f "Isabelle-repository-$IDENT/.hgtags"
   101 
   102 
   103 # dist name
   104 
   105 DATE=$(env LC_ALL=C date "+%d-%b-%Y")
   106 DISTDATE=$(env LC_ALL=C date "+%B %Y")
   107 
   108 if [ -z "$RELEASE" ]; then
   109   DISTNAME="Isabelle_$DATE"
   110   DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
   111 else
   112   DISTNAME="$RELEASE"
   113   DISTVERSION="$DISTNAME: $DISTDATE"
   114 fi
   115 
   116 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
   117 mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
   118 [ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
   119 [ -e "$DISTBASE/pdf/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/pdf/$DISTNAME already exists!"; }
   120 
   121 cd "$DISTBASE"
   122 mv "$DISTPREFIX/$TMP/Isabelle-repository-$IDENT" "$DISTNAME"
   123 purge_tmp
   124 
   125 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
   126 
   127 
   128 # website
   129 
   130 mkdir -p ../website
   131 cat > ../website/distinfo.mak <<EOF
   132 # this is a generated file - do not edit unless you know what you are doing!
   133 DISTNAME=$DISTNAME
   134 DISTBASE=$DISTBASE
   135 EOF
   136 
   137 cp lib/html/library_index_content.template ../website/
   138 
   139 
   140 # prepare dist for release
   141 
   142 echo "###"
   143 echo "### Preparing distribution $DISTNAME"
   144 echo "###"
   145 
   146 find . -name .cvsignore -print | xargs rm -rf
   147 find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x
   148 find . -print | xargs chmod u+rw
   149 
   150 ./Admin/build all || fail "Failed to build distribution"
   151 rm -rf Admin
   152 
   153 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')
   154 mv -f $MOVE doc
   155 rm doc/Isa-logics.eps
   156 rm doc/codegen_process.pdf
   157 rm -rf doc-src
   158 
   159 mkdir contrib
   160 
   161 cp doc/isabelle*.eps lib/logo
   162 
   163 
   164 if [ -z "$RELEASE" ]; then
   165   {
   166     echo
   167     echo "IMPORTANT NOTE"
   168     echo "=============="
   169     echo
   170     echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
   171     echo "See $REPOS/log/$IDENT for details."
   172     echo
   173   } >ANNOUNCE
   174 else
   175   perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
   176 fi
   177 
   178 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
   179 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
   180 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
   181 perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
   182 perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README
   183 
   184 
   185 # create archives
   186 
   187 echo "###"
   188 echo "### Creating archives ..."
   189 echo "###"
   190 
   191 cd "$DISTBASE"
   192 
   193 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
   194 echo "$IDENT" >../ISABELLE_IDENT
   195 
   196 rm -f Isabelle
   197 ln -s "$DISTNAME" Isabelle
   198 
   199 chown -R "$LOGNAME" "$DISTNAME"
   200 chmod -R u+w "$DISTNAME"
   201 chmod -R g=o "$DISTNAME"
   202 chgrp -R isabelle "$DISTNAME" Isabelle
   203 
   204 mkdir -p "pdf/$DISTNAME/doc"
   205 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
   206 
   207 echo "$DISTNAME.tar.gz"
   208 tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
   209 
   210 echo "${DISTNAME}_pdf.tar.gz"
   211 tar -C pdf -czf "${DISTNAME}_pdf.tar.gz" "$DISTNAME"
   212 
   213 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
   214 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
   215 
   216 
   217 # cleanup dist
   218 
   219 mv "$DISTNAME" "${DISTNAME}-old"
   220 mkdir "$DISTNAME"
   221 
   222 mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
   223   "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
   224   "$DISTNAME"
   225 mkdir "$DISTNAME/doc"
   226 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
   227 
   228 chgrp -R isabelle "$DISTNAME"
   229 
   230 rm -rf "${DISTNAME}-old"
   231