Admin/lib/Tools/makedist
author wenzelm
Mon Oct 24 14:37:37 2016 +0200 (2016-10-24)
changeset 64373 5a3e35cb6f54
parent 64369 6a9816764b37
child 64404 d75397e0aad5
permissions -rwxr-xr-x
retain Admin component for isabelle tool invocation;
     1 #!/usr/bin/env bash
     2 #
     3 # Author: Makarius
     4 #
     5 # DESCRIPTION: make Isabelle distribution from repository
     6 
     7 ## global parameters
     8 
     9 umask 022
    10 
    11 HG="${HG:-hg}"
    12 
    13 DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
    14 
    15 
    16 ## diagnostics
    17 
    18 PRG="$(basename "$0")"
    19 
    20 function usage()
    21 {
    22   echo
    23   echo "Usage: isabelle $PRG [OPTIONS] [VERSION]"
    24   echo
    25   echo "  Options are:"
    26   echo "    -O           official release (not release-candidate)"
    27   echo "    -d DIR       global directory prefix (default: \"$DISTPREFIX\")"
    28   echo "    -j INT       maximum number of parallel jobs (default 1)"
    29   echo "    -r RELEASE   proper release with name"
    30   echo
    31   echo "  Make Isabelle distribution from the local repository clone."
    32   echo
    33   echo "  VERSION identifies the snapshot, using usual Mercurial terminology;"
    34   echo "  the default is RELEASE if given, otherwise \"tip\"."
    35   echo
    36   echo "  Add-on components are that of the running Isabelle version!"
    37   echo
    38   exit 1
    39 }
    40 
    41 function fail()
    42 {
    43   echo "$1" >&2
    44   exit 2
    45 }
    46 
    47 function check_number()
    48 {
    49   [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
    50 }
    51 
    52 
    53 ## process command line
    54 
    55 # options
    56 
    57 OFFICIAL_RELEASE="false"
    58 JOBS=""
    59 RELEASE=""
    60 
    61 while getopts "Od:j:r:" OPT
    62 do
    63   case "$OPT" in
    64     O)
    65       OFFICIAL_RELEASE="true"
    66       ;;
    67     d)
    68       DISTPREFIX="$OPTARG"
    69       ;;
    70     j)
    71       check_number "$OPTARG"
    72       JOBS="-j $OPTARG"
    73       ;;
    74     r)
    75       RELEASE="$OPTARG"
    76       ;;
    77     \?)
    78       usage
    79       ;;
    80   esac
    81 done
    82 
    83 shift $(($OPTIND - 1))
    84 
    85 
    86 # args
    87 
    88 VERSION=""
    89 [ "$#" -gt 0 ] && { VERSION="$1"; shift; }
    90 [ -z "$VERSION" ] && VERSION="$RELEASE"
    91 [ -z "$VERSION" ] && VERSION="tip"
    92 
    93 [ "$#" -gt 0 ] && usage
    94 
    95 IDENT=$("$HG" --repository "$ISABELLE_HOME" id -r "$VERSION" -i)
    96 [ -z "$IDENT" ] && fail "Bad repository version: \"$VERSION\""
    97 
    98 
    99 ## main
   100 
   101 # dist name
   102 
   103 DATE=$(env LC_ALL=C date "+%d-%b-%Y")
   104 DISTDATE=$(env LC_ALL=C date "+%B %Y")
   105 
   106 if [ -z "$RELEASE" ]; then
   107   DISTNAME="Isabelle_$DATE"
   108   DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
   109 else
   110   DISTNAME="$RELEASE"
   111   DISTVERSION="$DISTNAME: $DISTDATE"
   112 fi
   113 
   114 DISTPREFIX="$(cd "$DISTPREFIX"; pwd)"
   115 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
   116 mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir \"$DISTBASE\""
   117 
   118 DIR="$DISTBASE/$DISTNAME"
   119 [ -e "$DIR" ] && fail "Directory \"$DIR\" already exists"
   120 
   121 rm -f "$DISTPREFIX/ISABELLE_DIST" "$DISTPREFIX/ISABELLE_IDENT"
   122 
   123 
   124 # retrieve repository archive
   125 
   126 echo "### Retrieving Mercurial repository $VERSION"
   127 
   128 "$HG" --repository "$ISABELLE_HOME" archive --type files -r "$IDENT" "$DIR" || \
   129   fail "Failed to retrieve $VERSION"
   130 
   131 rm -f "$DIR/.hg_archival.txt"
   132 rm -f "$DIR/.hgtags"
   133 rm -f "$DIR/.hgignore"
   134 rm -f "$DIR/README_REPOSITORY"
   135 
   136 
   137 # partial context switch to new version
   138 
   139 cd "$DIR"
   140 
   141 unset ISABELLE_SETTINGS_PRESENT
   142 unset ISABELLE_SITE_SETTINGS_PRESENT
   143 
   144 if [ -z "$RELEASE" ]; then
   145   {
   146     echo
   147     echo "IMPORTANT NOTE"
   148     echo "=============="
   149     echo
   150     echo "This is a snapshot of Isabelle/${IDENT} from the repository."
   151     echo
   152   } >ANNOUNCE
   153 fi
   154 
   155 if [ -n "$RELEASE" -a "$OFFICIAL_RELEASE" = true ]; then
   156   IS_OFFICIAL="true"
   157 else
   158   IS_OFFICIAL="false"
   159 fi
   160 
   161 perl -pi \
   162   -e "s,val is_identified = false,val is_identified = true,g;" \
   163   -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g;" \
   164   src/Pure/System/distribution.ML src/Pure/System/distribution.scala
   165 
   166 perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
   167 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
   168 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
   169 perl -pi -e "s,unidentified repository version,$DISTVERSION,g" \
   170   src/Pure/System/distribution.ML src/Pure/System/distribution.scala lib/Tools/version
   171 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
   172 
   173 mkdir -p contrib
   174 cat >contrib/README <<EOF
   175 This directory contains add-on components that contribute to the main
   176 Isabelle distribution.  Separate licensing conditions apply, see each
   177 directory individually.
   178 EOF
   179 
   180 
   181 # prepare dist for release
   182 
   183 echo "### Preparing distribution $DISTNAME"
   184 
   185 find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -print | xargs chmod -f -x
   186 find . -print | xargs chmod -f u+rw
   187 
   188 export CLASSPATH="$ISABELLE_CLASSPATH"
   189 
   190 ./Admin/build all || fail "Failed to build distribution"
   191 
   192 ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
   193 
   194 cp -a src src.orig
   195 env ISABELLE_IDENTIFIER="${DISTNAME}-build" \
   196   ./bin/isabelle build_doc $JOBS -s -a || fail "Failed to build documentation"
   197 rm -rf src
   198 mv src.orig src
   199 
   200 ./bin/isabelle news
   201 
   202 rm -rf Admin browser_info heaps
   203 
   204 rmdir "$USER_HOME/.isabelle/${DISTNAME}-build"
   205 rmdir "$USER_HOME/.isabelle/${DISTNAME}"
   206 
   207 
   208 # create archive
   209 
   210 #GNU tar (notably on Mac OS X)
   211 type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
   212 
   213 echo "### Creating archive"
   214 
   215 cd "$DISTBASE"
   216 
   217 echo "$DISTBASE/$DISTNAME.tar.gz" > "$DISTPREFIX/ISABELLE_DIST"
   218 echo "$IDENT" > "$DISTPREFIX/ISABELLE_IDENT"
   219 
   220 chown -R "$LOGNAME" "$DISTNAME"
   221 chmod -R g=o "$DISTNAME"
   222 chmod -R u+w "$DISTNAME"
   223 find "$DISTNAME" -type f "(" -name '*.scala' -o -name '*.ML' -o -name '*.thy' ")" -print | xargs chmod -f u-w
   224 
   225 echo "$DISTBASE/$DISTNAME.tar.gz"
   226 tar -c -z -f "$DISTNAME.tar.gz" "$DISTNAME"
   227 [ "$?" = 0 ] || exit "$?"
   228 
   229 
   230 # cleanup dist
   231 
   232 mv "$DISTNAME" "${DISTNAME}-old"
   233 mkdir "$DISTNAME"
   234 
   235 mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
   236   "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
   237 mkdir "$DISTNAME/doc"
   238 mv "${DISTNAME}-old/doc/"*.pdf \
   239   "${DISTNAME}-old/doc/"*.html \
   240   "${DISTNAME}-old/doc/"*.css \
   241   "${DISTNAME}-old/doc/"*.ttf \
   242   "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
   243 
   244 rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
   245 
   246 rm -rf "${DISTNAME}-old"