Admin/Release/build
author wenzelm
Tue, 02 Aug 2016 11:49:30 +0200
changeset 63578 e8990d0e3965
parent 61034 0776a4adc3d5
child 64144 ef20d2da71af
permissions -rwxr-xr-x
tuned;
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:"
57685
34ec8a580917 proper option -O;
wenzelm
parents: 56902
diff changeset
    21
  echo "    -O           official release (not release-candidate)"
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    22
  echo "    -j INT       maximum number of parallel jobs (default 1)"
56902
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
    23
  echo "    -l           build library"
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    24
  echo "    -r RELEASE   proper release with name"
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 "  Make Isabelle distribution DIR, using the local repository clone."
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    27
  echo
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    28
  echo "  VERSION identifies the snapshot, using usual Mercurial terminology;"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    29
  echo "  the default is RELEASE if given, otherwise \"tip\"."
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    30
  echo
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    31
  exit 1
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    32
}
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
function fail()
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    35
{
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    36
  echo "$1" >&2
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    37
  exit 2
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    38
}
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
function check_number()
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
  [ -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
    43
}
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    44
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
## process command line
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
# options
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    49
57685
34ec8a580917 proper option -O;
wenzelm
parents: 56902
diff changeset
    50
OFFICIAL_RELEASE=""
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    51
JOBS=""
56902
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
    52
LIBRARY=""
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    53
RELEASE=""
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    54
57685
34ec8a580917 proper option -O;
wenzelm
parents: 56902
diff changeset
    55
while getopts "Oj:lr:" OPT
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    56
do
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    57
  case "$OPT" in
57685
34ec8a580917 proper option -O;
wenzelm
parents: 56902
diff changeset
    58
    O)
34ec8a580917 proper option -O;
wenzelm
parents: 56902
diff changeset
    59
      OFFICIAL_RELEASE="-O"
34ec8a580917 proper option -O;
wenzelm
parents: 56902
diff changeset
    60
      ;;
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    61
    j)
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    62
      check_number "$OPTARG"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    63
      JOBS="-j $OPTARG"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    64
      ;;
56902
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
    65
    l)
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
    66
      LIBRARY="true"
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
    67
      ;;
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    68
    r)
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    69
      RELEASE="$OPTARG"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    70
      ;;
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
      usage
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    73
      ;;
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    74
  esac
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    75
done
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    76
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    77
shift $(($OPTIND - 1))
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    78
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    79
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    80
# args
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    81
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    82
BASE_DIR=""
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    83
[ "$#" -gt 0 ] && { BASE_DIR="$1"; shift; }
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    84
[ -z "$BASE_DIR" ] && usage
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
VERSION=""
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    87
[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    88
[ -z "$VERSION" ] && VERSION="$RELEASE"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    89
[ -z "$VERSION" ] && VERSION="tip"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    90
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    91
[ "$#" -gt 0 ] && usage
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    92
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    93
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    94
## Isabelle settings
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    95
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    96
ISABELLE_TOOL="$THIS/../../bin/isabelle"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    97
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
    98
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
    99
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   100
## main
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   101
56902
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   102
# make dist
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   103
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   104
if [ -z "$RELEASE" ]; then
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   105
  DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")"
57685
34ec8a580917 proper option -O;
wenzelm
parents: 56902
diff changeset
   106
  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   107
else
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   108
  DISTNAME="$RELEASE"
57685
34ec8a580917 proper option -O;
wenzelm
parents: 56902
diff changeset
   109
  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE -r "$RELEASE"
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   110
fi
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   111
[ "$?" = 0 ] || exit "$?"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   112
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   113
DISTBASE="$BASE_DIR/dist-${DISTNAME}"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   114
51064
9c425ed4a52c separate makedist_bundle for each platform family, which is more useful for manual use;
wenzelm
parents: 50899
diff changeset
   115
56902
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   116
# make bundles
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   117
61000
dd43980dc2c6 separate bundle for windows64;
wenzelm
parents: 60214
diff changeset
   118
for PLATFORM_FAMILY in linux windows windows64 macos
51064
9c425ed4a52c separate makedist_bundle for each platform family, which is more useful for manual use;
wenzelm
parents: 50899
diff changeset
   119
do
9c425ed4a52c separate makedist_bundle for each platform family, which is more useful for manual use;
wenzelm
parents: 50899
diff changeset
   120
9c425ed4a52c separate makedist_bundle for each platform family, which is more useful for manual use;
wenzelm
parents: 50899
diff changeset
   121
echo
9c425ed4a52c separate makedist_bundle for each platform family, which is more useful for manual use;
wenzelm
parents: 50899
diff changeset
   122
echo "*** $PLATFORM_FAMILY ***"
9c425ed4a52c separate makedist_bundle for each platform family, which is more useful for manual use;
wenzelm
parents: 50899
diff changeset
   123
9c425ed4a52c separate makedist_bundle for each platform family, which is more useful for manual use;
wenzelm
parents: 50899
diff changeset
   124
"$ISABELLE_TOOL" makedist_bundle "$DISTBASE/${DISTNAME}.tar.gz" "$PLATFORM_FAMILY"
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   125
[ "$?" = 0 ] || exit "$?"
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   126
51064
9c425ed4a52c separate makedist_bundle for each platform family, which is more useful for manual use;
wenzelm
parents: 50899
diff changeset
   127
done
9c425ed4a52c separate makedist_bundle for each platform family, which is more useful for manual use;
wenzelm
parents: 50899
diff changeset
   128
56902
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   129
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   130
# minimal index
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   131
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   132
cat > "$DISTBASE/index.html" <<EOF
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   133
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 3.2//EN">
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   134
<html>
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   135
<head>
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   136
<title>${DISTNAME}</title>
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   137
</head>
50899
506ff6abfde0 grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
diff changeset
   138
56902
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   139
<body>
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   140
<h1>${DISTNAME}</h1>
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   141
<ul>
61002
8c52177fb436 clarified linux application bundle;
wenzelm
parents: 61000
diff changeset
   142
<li><a href="${DISTNAME}_app.tar.gz">Linux</a></li>
61034
wenzelm
parents: 61002
diff changeset
   143
<li><a href="${DISTNAME}-win32.exe">Windows</a></li>
61000
dd43980dc2c6 separate bundle for windows64;
wenzelm
parents: 60214
diff changeset
   144
<li><a href="${DISTNAME}-win64.exe">Windows (64bit)</a></li>
56902
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   145
<li><a href="${DISTNAME}.dmg">Mac OS X</a></li>
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   146
</ul>
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   147
</body>
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   148
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   149
</html>
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   150
EOF
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   151
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   152
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   153
# HTML library
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   154
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   155
if [ -n "$LIBRARY" ]; then
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   156
  "$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   157
fi
f901a08c5653 explicit option to build library, which takes most of the time;
wenzelm
parents: 51064
diff changeset
   158