Admin/makedist
author wenzelm
Tue Aug 11 15:53:13 2009 +0200 (2009-08-11)
changeset 32361 141e5151b918
parent 31842 af5221147455
child 33844 813b091dd63b
permissions -rwxr-xr-x
clarified situation about unidentified repository versions -- in a distributed setting there is not "the" repository;
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@30110
     7
REPOS="http://isabelle.in.tum.de/repos/isabelle"
wenzelm@28932
     8
wenzelm@28932
     9
DISTPREFIX=${DISTPREFIX:-~/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@30885
    17
THIS="$(cd $(dirname "$0"); echo "$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@28932
    26
    -r RELEASE         proper release with name"
wenzelm@28932
    27
wenzelm@28932
    28
  Make Isabelle distribution from the main Mercurial repository at TUM.
wenzelm@28932
    29
wenzelm@28932
    30
  VERSION identifies the snapshot, using usual Mercurial terminology;
wenzelm@28932
    31
  the default is RELEASE if given, otherwise "tip".
wenzelm@28932
    32
wenzelm@28932
    33
EOF
wenzelm@28932
    34
  exit 1
wenzelm@28932
    35
}
wenzelm@28932
    36
wenzelm@28932
    37
function fail()
wenzelm@28932
    38
{
wenzelm@28932
    39
  echo "$1" >&2
wenzelm@28932
    40
  exit 2
wenzelm@28932
    41
}
wenzelm@28932
    42
wenzelm@28932
    43
wenzelm@28932
    44
## process command line
wenzelm@28932
    45
wenzelm@28932
    46
# options
wenzelm@28932
    47
wenzelm@28932
    48
RELEASE=""
wenzelm@28932
    49
wenzelm@28932
    50
while getopts "r:" OPT
wenzelm@28932
    51
do
wenzelm@28932
    52
  case "$OPT" in
wenzelm@28932
    53
    r)
wenzelm@28932
    54
      RELEASE="$OPTARG"
wenzelm@28932
    55
      ;;
wenzelm@28932
    56
    \?)
wenzelm@28932
    57
      usage
wenzelm@28932
    58
      ;;
wenzelm@28932
    59
  esac
wenzelm@28932
    60
done
wenzelm@28932
    61
wenzelm@28932
    62
shift $(($OPTIND - 1))
wenzelm@28932
    63
wenzelm@28932
    64
wenzelm@28932
    65
# args
wenzelm@28932
    66
wenzelm@28932
    67
VERSION=""
wenzelm@28932
    68
[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
wenzelm@28932
    69
[ -z "$VERSION" ] && VERSION="$RELEASE"
wenzelm@28932
    70
[ -z "$VERSION" ] && VERSION="tip"
wenzelm@28932
    71
wenzelm@28932
    72
[ "$#" -gt 0 ] && usage
wenzelm@28932
    73
wenzelm@28932
    74
wenzelm@28932
    75
## main
wenzelm@28932
    76
wenzelm@28932
    77
# tmp
wenzelm@28932
    78
wenzelm@28932
    79
TMP="tmp-$USER$$"
wenzelm@28932
    80
function purge_tmp () { rm -rf "$DISTPREFIX/$TMP"; }
wenzelm@28932
    81
wenzelm@28932
    82
wenzelm@28932
    83
# retrieve archive and resolve version identifier
wenzelm@28932
    84
wenzelm@28932
    85
mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
wenzelm@28932
    86
cd "$DISTPREFIX/$TMP"
wenzelm@28932
    87
wenzelm@28932
    88
echo "###"
wenzelm@28932
    89
echo "### Retrieving Mercurial repository $VERSION"
wenzelm@28932
    90
echo "###"
wenzelm@28932
    91
wenzelm@28932
    92
{ wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
wenzelm@28932
    93
  fail "Failed to retrieve $VERSION"
wenzelm@28932
    94
wenzelm@28932
    95
IDENT=$(echo * | sed 's/isabelle-//')
wenzelm@28932
    96
wenzelm@28932
    97
rm -f "isabelle-$IDENT/.hg_archival.txt"
wenzelm@28932
    98
rm -f "isabelle-$IDENT/.hgtags"
wenzelm@28932
    99
rm -f "isabelle-$IDENT/.hgignore"
wenzelm@28932
   100
rm -f "isabelle-$IDENT/README_REPOSITORY"
wenzelm@28932
   101
wenzelm@28932
   102
wenzelm@28932
   103
# dist name
wenzelm@28932
   104
wenzelm@28932
   105
DATE=$(env LC_ALL=C date "+%d-%b-%Y")
wenzelm@28932
   106
DISTDATE=$(env LC_ALL=C date "+%B %Y")
wenzelm@28932
   107
wenzelm@28932
   108
if [ -z "$RELEASE" ]; then
wenzelm@28932
   109
  DISTNAME="Isabelle_$DATE"
wenzelm@28932
   110
  DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
wenzelm@28932
   111
else
wenzelm@28932
   112
  DISTNAME="$RELEASE"
wenzelm@28932
   113
  DISTVERSION="$DISTNAME: $DISTDATE"
wenzelm@28932
   114
fi
wenzelm@28932
   115
wenzelm@28932
   116
DISTBASE="$DISTPREFIX/dist-$DISTNAME"
wenzelm@28932
   117
mkdir -p "$DISTBASE" || { purge_tmp; fail "Unable to create distribution base dir $DISTBASE!"; }
wenzelm@28932
   118
[ -e "$DISTBASE/$DISTNAME" ] && { purge_tmp; fail "$DISTBASE/$DISTNAME already exists!"; }
wenzelm@28932
   119
wenzelm@28932
   120
cd "$DISTBASE"
wenzelm@28932
   121
mv "$DISTPREFIX/$TMP/isabelle-$IDENT" "$DISTNAME"
wenzelm@28932
   122
purge_tmp
wenzelm@28932
   123
wenzelm@28932
   124
cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
wenzelm@28932
   125
wenzelm@28932
   126
wenzelm@28932
   127
# prepare dist for release
wenzelm@28932
   128
wenzelm@28932
   129
echo "###"
wenzelm@28932
   130
echo "### Preparing distribution $DISTNAME"
wenzelm@28932
   131
echo "###"
wenzelm@28932
   132
wenzelm@30885
   133
rm -f .hgignore
wenzelm@30287
   134
find . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -f -x
wenzelm@30885
   135
find . -print | xargs chmod -f u+rw
wenzelm@28932
   136
wenzelm@28932
   137
./Admin/build all || fail "Failed to build distribution"
wenzelm@28932
   138
rm -rf Admin
wenzelm@28932
   139
wenzelm@28932
   140
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
   141
mv -f $MOVE doc
wenzelm@28932
   142
rm doc/Isa-logics.eps
wenzelm@31842
   143
rm doc/adaptation.dvi doc/adaptation.pdf doc/architecture.dvi doc/architecture.pdf
wenzelm@28932
   144
rm -rf doc-src
wenzelm@28932
   145
wenzelm@30140
   146
mkdir -p contrib
wenzelm@28932
   147
wenzelm@28932
   148
cp doc/isabelle*.eps lib/logo
wenzelm@28932
   149
wenzelm@28932
   150
wenzelm@28932
   151
if [ -z "$RELEASE" ]; then
wenzelm@28932
   152
  {
wenzelm@28932
   153
    echo
wenzelm@28932
   154
    echo "IMPORTANT NOTE"
wenzelm@28932
   155
    echo "=============="
wenzelm@28932
   156
    echo
wenzelm@28932
   157
    echo "This is an unofficial snapshot of Isabelle, created by $LOGNAME $DATE."
wenzelm@28932
   158
    echo "See $REPOS/log/$IDENT for details."
wenzelm@28932
   159
    echo
wenzelm@28932
   160
  } >ANNOUNCE
wenzelm@28932
   161
else
wenzelm@28932
   162
  perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
wenzelm@28932
   163
fi
wenzelm@28932
   164
wenzelm@28932
   165
perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
wenzelm@28932
   166
perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
wenzelm@28932
   167
perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
wenzelm@32361
   168
perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
wenzelm@32361
   169
perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
wenzelm@28932
   170
wenzelm@28932
   171
wenzelm@28932
   172
# create archives
wenzelm@28932
   173
wenzelm@28932
   174
echo "###"
wenzelm@28932
   175
echo "### Creating archives ..."
wenzelm@28932
   176
echo "###"
wenzelm@28932
   177
wenzelm@28932
   178
cd "$DISTBASE"
wenzelm@28932
   179
wenzelm@28932
   180
echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST
wenzelm@28932
   181
echo "$IDENT" >../ISABELLE_IDENT
wenzelm@28932
   182
wenzelm@28932
   183
rm -f Isabelle
wenzelm@28932
   184
ln -s "$DISTNAME" Isabelle
wenzelm@28932
   185
wenzelm@28932
   186
chown -R "$LOGNAME" "$DISTNAME"
wenzelm@28932
   187
chmod -R u+w "$DISTNAME"
wenzelm@28932
   188
chmod -R g=o "$DISTNAME"
wenzelm@28932
   189
chgrp -R isabelle "$DISTNAME" Isabelle
wenzelm@28932
   190
wenzelm@28932
   191
echo "$DISTNAME.tar.gz"
wenzelm@28932
   192
tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
wenzelm@28932
   193
wenzelm@28932
   194
wenzelm@28932
   195
# cleanup dist
wenzelm@28932
   196
wenzelm@28932
   197
mv "$DISTNAME" "${DISTNAME}-old"
wenzelm@28932
   198
mkdir "$DISTNAME"
wenzelm@28932
   199
wenzelm@28932
   200
mv "${DISTNAME}-old/README" "${DISTNAME}-old/INSTALL" "${DISTNAME}-old/NEWS" \
wenzelm@28932
   201
  "${DISTNAME}-old/ANNOUNCE" "${DISTNAME}-old/COPYRIGHT" "${DISTNAME}-old/CONTRIBUTORS" \
wenzelm@28932
   202
  "$DISTNAME"
wenzelm@28932
   203
mkdir "$DISTNAME/doc"
wenzelm@28932
   204
mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc"
wenzelm@28932
   205
wenzelm@28932
   206
chgrp -R isabelle "$DISTNAME"
wenzelm@28932
   207
wenzelm@28932
   208
rm -rf "${DISTNAME}-old"
wenzelm@28932
   209