Admin/Release/makedist
author wenzelm
Tue Aug 14 10:44:03 2012 +0200 (2012-08-14)
changeset 48790 6e739225dd8a
parent 48606 4b6c90e121b1
child 48972 196520d51afd
permissions -rwxr-xr-x
always retain doc-src (as regular component);
wenzelm@28932
     1
#!/usr/bin/env bash
wenzelm@28932
     2
#
wenzelm@28932
     3
# makedist -- make Isabelle source distribution
wenzelm@28932
     4
wenzelm@28932
     5
## global settings
wenzelm@28932
     6
wenzelm@47887
     7
REPOS_NAME="isabelle"
haftmann@46929
     8
REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}"
wenzelm@47011
     9
DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
wenzelm@28932
    10
wenzelm@28932
    11
umask 022
wenzelm@28932
    12
wenzelm@28932
    13
wenzelm@28932
    14
## diagnostics
wenzelm@28932
    15
wenzelm@30885
    16
PRG="$(basename "$0")"
wenzelm@44152
    17
THIS="$(cd $(dirname "$0"); pwd)"
wenzelm@28932
    18
wenzelm@28932
    19
function usage()
wenzelm@28932
    20
{
wenzelm@28932
    21
  cat <<EOF
wenzelm@28932
    22
wenzelm@28932
    23
Usage: $PRG [OPTIONS] [VERSION]
wenzelm@28932
    24
wenzelm@28932
    25
  Options are:
wenzelm@43357
    26
    -j JEDIT_BUILD     build Isabelle/jEdit via given jedit_build component
wenzelm@28932
    27
    -r RELEASE         proper release with name"
wenzelm@28932
    28
wenzelm@28932
    29
  Make Isabelle distribution from the main Mercurial repository at TUM.
wenzelm@28932
    30
wenzelm@28932
    31
  VERSION identifies the snapshot, using usual Mercurial terminology;
wenzelm@28932
    32
  the default is RELEASE if given, otherwise "tip".
wenzelm@28932
    33
wenzelm@28932
    34
EOF
wenzelm@28932
    35
  exit 1
wenzelm@28932
    36
}
wenzelm@28932
    37
wenzelm@28932
    38
function fail()
wenzelm@28932
    39
{
wenzelm@28932
    40
  echo "$1" >&2
wenzelm@28932
    41
  exit 2
wenzelm@28932
    42
}
wenzelm@28932
    43
wenzelm@28932
    44
wenzelm@28932
    45
## process command line
wenzelm@28932
    46
wenzelm@28932
    47
# options
wenzelm@28932
    48
wenzelm@28932
    49
RELEASE=""
wenzelm@43357
    50
ISABELLE_JEDIT_BUILD_HOME=""
wenzelm@28932
    51
wenzelm@48790
    52
while getopts "j:r:" OPT
wenzelm@28932
    53
do
wenzelm@28932
    54
  case "$OPT" in
wenzelm@43357
    55
    j)
wenzelm@43357
    56
      ISABELLE_JEDIT_BUILD_HOME="$OPTARG"
wenzelm@43357
    57
      ;;
wenzelm@28932
    58
    r)
wenzelm@28932
    59
      RELEASE="$OPTARG"
wenzelm@28932
    60
      ;;
wenzelm@28932
    61
    \?)
wenzelm@28932
    62
      usage
wenzelm@28932
    63
      ;;
wenzelm@28932
    64
  esac
wenzelm@28932
    65
done
wenzelm@28932
    66
wenzelm@28932
    67
shift $(($OPTIND - 1))
wenzelm@28932
    68
wenzelm@28932
    69
wenzelm@28932
    70
# args
wenzelm@28932
    71
wenzelm@28932
    72
VERSION=""
wenzelm@28932
    73
[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
wenzelm@28932
    74
[ -z "$VERSION" ] && VERSION="$RELEASE"
wenzelm@28932
    75
[ -z "$VERSION" ] && VERSION="tip"
wenzelm@28932
    76
wenzelm@28932
    77
[ "$#" -gt 0 ] && usage
wenzelm@28932
    78
wenzelm@28932
    79
wenzelm@28932
    80
## main
wenzelm@28932
    81
wenzelm@28932
    82
# tmp
wenzelm@28932
    83
wenzelm@28932
    84
TMP="tmp-$USER$$"
wenzelm@28932
    85
function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
wenzelm@28932
    86
wenzelm@28932
    87
wenzelm@28932
    88
# retrieve archive and resolve version identifier
wenzelm@28932
    89
wenzelm@28932
    90
mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
wenzelm@28932
    91
cd "$DISTPREFIX/$TMP"
wenzelm@28932
    92
wenzelm@28932
    93
echo "###"
wenzelm@28932
    94
echo "### Retrieving Mercurial repository $VERSION"
wenzelm@28932
    95
echo "###"
wenzelm@28932
    96
haftmann@46930
    97
if expr match "$REPOS" "https\?://" > /dev/null
haftmann@46930
    98
then
haftmann@46930
    99
  { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
haftmann@46930
   100
    fail "Failed to retrieve $VERSION"
haftmann@46930
   101
else
haftmann@46930
   102
  { hg --repository "$REPOS" archive --type tgz - | tar -xzf -; } || \
haftmann@46930
   103
    fail "Failed to retrieve $VERSION"
haftmann@46930
   104
fi
wenzelm@28932
   105
wenzelm@33910
   106
IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
wenzelm@28932
   107
wenzelm@33909
   108
rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
wenzelm@33909
   109
rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
wenzelm@33909
   110
rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
wenzelm@33909
   111
rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
wenzelm@28932
   112
wenzelm@28932
   113
wenzelm@28932
   114
# dist name
wenzelm@28932
   115
wenzelm@28932
   116
DATE=$(env LC_ALL=C date "+%d-%b-%Y")
wenzelm@28932
   117
DISTDATE=$(env LC_ALL=C date "+%B %Y")
wenzelm@28932
   118
wenzelm@28932
   119
if [ -z "$RELEASE" ]; then
wenzelm@28932
   120
  DISTNAME="Isabelle_$DATE"
wenzelm@40573
   121
  DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
wenzelm@28932
   122
else
wenzelm@28932
   123
  DISTNAME="$RELEASE"
wenzelm@28932
   124
  DISTVERSION="$DISTNAME: $DISTDATE"
wenzelm@28932
   125
fi
wenzelm@28932
   126
wenzelm@28932
   127
DISTBASE="$DISTPREFIX/dist-$DISTNAME"
wenzelm@28932
   128
mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
wenzelm@28932
   129
[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
wenzelm@28932
   130
wenzelm@28932
   131
cd "$DISTBASE"
wenzelm@33909
   132
mv "$DISTPREFIX/$TMP/${REPOS_NAME}-${IDENT}" "$DISTNAME"
wenzelm@28932
   133
purge_tmp
wenzelm@28932
   134
wenzelm@28932
   135
cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
wenzelm@28932
   136
wenzelm@28932
   137
wenzelm@28932
   138
# prepare dist for release
wenzelm@28932
   139
wenzelm@28932
   140
echo "###"
wenzelm@28932
   141
echo "### Preparing distribution $DISTNAME"
wenzelm@28932
   142
echo "###"
wenzelm@28932
   143
wenzelm@30885
   144
rm -f .hgignore
wenzelm@47739
   145
find . "(" -name \*.thy -o -name \*.ML -o -name \*.scala ")" -perm +111 -print | xargs chmod -f -x
wenzelm@30885
   146
find . -print | xargs chmod -f u+rw
wenzelm@28932
   147
wenzelm@47010
   148
perl -pi -e 's/^(ISABELLE_SCALA_BUILD_OPTIONS=")/$1-optimise /,' etc/settings
wenzelm@47010
   149
wenzelm@48790
   150
cp -a doc-src doc-src.orig
wenzelm@48606
   151
wenzelm@28932
   152
./Admin/build all || fail "Failed to build distribution"
wenzelm@43357
   153
wenzelm@43357
   154
if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
wenzelm@43357
   155
  [ -d "$ISABELLE_JEDIT_BUILD_HOME" ] || fail "Bad jedit_build component directory: \"$ISABELLE_JEDIT_BUILD_HOME\""
wenzelm@43357
   156
  eval "$(fgrep ISABELLE_JEDIT_BUILD_VERSION "$ISABELLE_JEDIT_BUILD_HOME/etc/settings")"
wenzelm@43357
   157
  [ -n "$ISABELLE_JEDIT_BUILD_VERSION" ] || fail "Bad ISABELLE_JEDIT_BUILD_VERSION"
wenzelm@43357
   158
  export ISABELLE_JEDIT_BUILD_HOME ISABELLE_JEDIT_BUILD_VERSION
wenzelm@43357
   159
  ./bin/isabelle jedit -b || fail "Failed to build Isabelle/jEdit"
wenzelm@43357
   160
fi
wenzelm@43357
   161
wenzelm@28932
   162
rm -rf Admin
wenzelm@28932
   163
wenzelm@28932
   164
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')
wenzelm@28932
   165
mv -f $MOVE doc
wenzelm@28932
   166
rm doc/Isa-logics.eps
wenzelm@31842
   167
rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf
wenzelm@28932
   168
rm -rf doc-src
wenzelm@28932
   169
wenzelm@48790
   170
mv doc-src.orig doc-src
wenzelm@48606
   171
wenzelm@30140
   172
mkdir -p contrib
wenzelm@37369
   173
cat >contrib/README <<EOF
wenzelm@37369
   174
This directory contains add-on components that contribute to the main
wenzelm@37369
   175
Isabelle distribution.  Separate licensing conditions apply, see each
wenzelm@37369
   176
directory individually.
wenzelm@37369
   177
EOF
wenzelm@28932
   178
wenzelm@28932
   179
cp doc/isabelle*.eps lib/logo
wenzelm@28932
   180
wenzelm@28932
   181
if [ -z "$RELEASE" ]; then
wenzelm@28932
   182
  {
wenzelm@28932
   183
    echo
wenzelm@28932
   184
    echo "IMPORTANT NOTE"
wenzelm@28932
   185
    echo "=============="
wenzelm@28932
   186
    echo
wenzelm@28932
   187
    echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
wenzelm@28932
   188
    echo "See $REPOS/log/$IDENT for details."
wenzelm@28932
   189
    echo
wenzelm@28932
   190
  } >ANNOUNCE
wenzelm@28932
   191
else
wenzelm@28932
   192
  perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
wenzelm@28932
   193
fi
wenzelm@28932
   194
wenzelm@28932
   195
perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
wenzelm@41511
   196
perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings
wenzelm@28932
   197
perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
wenzelm@28932
   198
perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
wenzelm@32361
   199
perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
wenzelm@32361
   200
perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
wenzelm@28932
   201
wenzelm@28932
   202
wenzelm@37341
   203
# create archive
wenzelm@28932
   204
wenzelm@28932
   205
echo "###"
wenzelm@37341
   206
echo "### Creating archive ..."
wenzelm@28932
   207
echo "###"
wenzelm@28932
   208
wenzelm@28932
   209
cd "$DISTBASE"
wenzelm@28932
   210
wenzelm@28932
   211
echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
wenzelm@28932
   212
echo "$IDENT" >../ISABELLE_IDENT
wenzelm@28932
   213
wenzelm@28932
   214
chown -R "$LOGNAME" "$DISTNAME"
wenzelm@28932
   215
chmod -R u+w "$DISTNAME"
wenzelm@28932
   216
chmod -R g=o "$DISTNAME"
wenzelm@40713
   217
chgrp -R isabelle "$DISTNAME"
wenzelm@28932
   218
wenzelm@28932
   219
echo "$DISTNAME.tar.gz"
wenzelm@40713
   220
tar -czf "$DISTNAME.tar.gz" "$DISTNAME"
wenzelm@28932
   221
wenzelm@28932
   222
wenzelm@28932
   223
# cleanup dist
wenzelm@28932
   224
wenzelm@28932
   225
mv "$DISTNAME" "${DISTNAME}-old"
wenzelm@28932
   226
mkdir "$DISTNAME"
wenzelm@28932
   227
wenzelm@37368
   228
mv "${DISTNAME}-old/README" "${DISTNAME}-old/NEWS" "${DISTNAME}-old/ANNOUNCE" \
wenzelm@37368
   229
  "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" "$DISTNAME"
wenzelm@28932
   230
mkdir "$DISTNAME/doc"
wenzelm@28932
   231
mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
wenzelm@28932
   232
wenzelm@41984
   233
rm -f Isabelle && ln -sf "$DISTNAME" Isabelle
wenzelm@41984
   234
wenzelm@28932
   235
chgrp -R isabelle "$DISTNAME"
wenzelm@28932
   236
wenzelm@28932
   237
rm -rf "${DISTNAME}-old"
wenzelm@28932
   238
wenzelm@37341
   239
echo "DONE"