Admin/Release/build
author wenzelm
Mon, 11 Jul 2016 18:39:30 +0200
changeset 63448 998acd66fbd7
parent 61034 0776a4adc3d5
child 64144 ef20d2da71af
permissions -rwxr-xr-x
clarified keywords;

#!/usr/bin/env bash
#
# Author: Makarius
#
# build full Isabelle distribution from repository

THIS="$(cd "$(dirname "$0")"; pwd)"
PRG="$(basename "$0")"


## diagnostics

PRG="$(basename "$0")"

function usage()
{
  echo
  echo "Usage: isabelle $PRG [OPTIONS] DIR [VERSION]"
  echo
  echo "  Options are:"
  echo "    -O           official release (not release-candidate)"
  echo "    -j INT       maximum number of parallel jobs (default 1)"
  echo "    -l           build library"
  echo "    -r RELEASE   proper release with name"
  echo
  echo "  Make Isabelle distribution DIR, using the local repository clone."
  echo
  echo "  VERSION identifies the snapshot, using usual Mercurial terminology;"
  echo "  the default is RELEASE if given, otherwise \"tip\"."
  echo
  exit 1
}

function fail()
{
  echo "$1" >&2
  exit 2
}

function check_number()
{
  [ -n "$1" -a -z "$(echo "$1" | tr -d '[0-9]')" ] || fail "Bad number: \"$1\""
}


## process command line

# options

OFFICIAL_RELEASE=""
JOBS=""
LIBRARY=""
RELEASE=""

while getopts "Oj:lr:" OPT
do
  case "$OPT" in
    O)
      OFFICIAL_RELEASE="-O"
      ;;
    j)
      check_number "$OPTARG"
      JOBS="-j $OPTARG"
      ;;
    l)
      LIBRARY="true"
      ;;
    r)
      RELEASE="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

BASE_DIR=""
[ "$#" -gt 0 ] && { BASE_DIR="$1"; shift; }
[ -z "$BASE_DIR" ] && usage

VERSION=""
[ "$#" -gt 0 ] && { VERSION="$1"; shift; }
[ -z "$VERSION" ] && VERSION="$RELEASE"
[ -z "$VERSION" ] && VERSION="tip"

[ "$#" -gt 0 ] && usage


## Isabelle settings

ISABELLE_TOOL="$THIS/../../bin/isabelle"
ISABELLE_PLATFORM_FAMILY="$("$ISABELLE_TOOL" getenv -b ISABELLE_PLATFORM_FAMILY)"


## main

# make dist

if [ -z "$RELEASE" ]; then
  DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")"
  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE
else
  DISTNAME="$RELEASE"
  "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS $OFFICIAL_RELEASE -r "$RELEASE"
fi
[ "$?" = 0 ] || exit "$?"

DISTBASE="$BASE_DIR/dist-${DISTNAME}"


# make bundles

for PLATFORM_FAMILY in linux windows windows64 macos
do

echo
echo "*** $PLATFORM_FAMILY ***"

"$ISABELLE_TOOL" makedist_bundle "$DISTBASE/${DISTNAME}.tar.gz" "$PLATFORM_FAMILY"
[ "$?" = 0 ] || exit "$?"

done


# minimal index

cat > "$DISTBASE/index.html" <<EOF
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 3.2//EN">
<html>
<head>
<title>${DISTNAME}</title>
</head>

<body>
<h1>${DISTNAME}</h1>
<ul>
<li><a href="${DISTNAME}_app.tar.gz">Linux</a></li>
<li><a href="${DISTNAME}-win32.exe">Windows</a></li>
<li><a href="${DISTNAME}-win64.exe">Windows (64bit)</a></li>
<li><a href="${DISTNAME}.dmg">Mac OS X</a></li>
</ul>
</body>

</html>
EOF


# HTML library

if [ -n "$LIBRARY" ]; then
  "$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz"
fi