Admin/Release/build
author wenzelm
Tue, 15 Jan 2013 12:30:23 +0100
changeset 50899 506ff6abfde0
child 51064 9c425ed4a52c
permissions -rwxr-xr-x
grand-unified Admin/Release/build script (excluding .app and .exe);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
     2
#
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
     3
# Author: Makarius
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
     4
#
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
     5
# build full Isabelle distribution from repository
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
     6
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
     7
THIS="$(cd "$(dirname "$0")"; pwd)"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
     8
PRG="$(basename "$0")"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
     9
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    10
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    11
## diagnostics
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    12
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    13
PRG="$(basename "$0")"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    14
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    15
function usage()
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    16
{
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    17
  echo
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    18
  echo "Usage: isabelle $PRG [OPTIONS] DIR [VERSION]"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    19
  echo
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    20
  echo "  Options are:"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    21
  echo "    -j INT       maximum number of parallel jobs (default 1)"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    22
  echo "    -r RELEASE   proper release with name"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    23
  echo
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    24
  echo "  Make Isabelle distribution DIR, using the local repository clone."
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    25
  echo
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    26
  echo "  VERSION identifies the snapshot, using usual Mercurial terminology;"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    27
  echo "  the default is RELEASE if given, otherwise \"tip\"."
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    28
  echo
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    29
  exit 1
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    30
}
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    31
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    32
function fail()
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    33
{
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    34
  echo "$1" >&2
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    35
  exit 2
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    36
}
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    37
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    38
function check_number()
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    39
{
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    40
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    41
}
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    42
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    43
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    44
## process command line
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    45
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    46
# options
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    47
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    48
JOBS=""
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    49
RELEASE=""
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    50
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    51
while getopts "j:r:" OPT
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    52
do
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    53
  case "$OPT" in
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    54
    j)
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    55
      check_number "$OPTARG"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    56
      JOBS="-j $OPTARG"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    57
      ;;
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    58
    r)
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    59
      RELEASE="$OPTARG"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    60
      ;;
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    61
    \?)
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    62
      usage
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    63
      ;;
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    64
  esac
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    65
done
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    66
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    67
shift $(($OPTIND - 1))
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    68
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    69
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    70
# args
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    71
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    72
BASE_DIR=""
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    73
[ "$#" -gt 0 ] && { BASE_DIR="$1"; shift; }
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    74
[ -z "$BASE_DIR" ] && usage
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    75
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    76
VERSION=""
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    77
[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    78
[ -z "$VERSION" ] && VERSION="$RELEASE"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    79
[ -z "$VERSION" ] && VERSION="tip"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    80
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    81
[ "$#" -gt 0 ] && usage
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    82
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    83
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    84
## Isabelle settings
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    85
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    86
ISABELLE_TOOL="$THIS/../../bin/isabelle"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    87
ISABELLE_PLATFORM_FAMILY="$("$ISABELLE_TOOL" getenv -b ISABELLE_PLATFORM_FAMILY)"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    88
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    89
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    90
## main
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    91
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    92
if [ -z "$RELEASE" ]; then
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    93
  DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    94
  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    95
else
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    96
  DISTNAME="$RELEASE"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    97
  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS -r "$RELEASE"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    98
fi
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    99
[ "$?" = 0 ] || exit "$?"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   100
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   101
DISTBASE="$BASE_DIR/dist-${DISTNAME}"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   102
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   103
"$ISABELLE_TOOL" makedist_bundles "$DISTBASE/${DISTNAME}.tar.gz"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   104
[ "$?" = 0 ] || exit "$?"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   105
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   106
"$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   107