Admin/Release/build_library

new documentation: How to Prove it

#!/usr/bin/env bash
#
# build Isabelle HTML library from platform bundle

## diagnostics

PRG=$(basename "$0")

function usage()
{
  echo
  echo "Usage: $PRG [OPTIONS] ARCHIVE"
  echo
  echo "  Options are:"
  echo "    -j INT       maximum number of parallel jobs (default 1)"
  echo
  echo "  Build Isabelle HTML library from platform bundle."
  echo
  exit 1
}

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


## process command line

# options

JOBS=""

while getopts "j:" OPT
do
  case "$OPT" in
    j)
      JOBS="-j $OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))


# args

[ "$#" -ne 1 ] && usage

ARCHIVE="$1"; shift

[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
ARCHIVE_BASE="$(basename "$ARCHIVE")"
ARCHIVE_DIR="$(cd "$(dirname "$ARCHIVE")"; echo "$PWD")"
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"


## main

#GNU tar (notably on Mac OS X)
if [ -x /usr/bin/gnutar ]; then
  function tar() { /usr/bin/gnutar "$@"; }
fi

TMP="/var/tmp/isabelle-makedist$$"
mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""

cd "$TMP"
tar -x -z -f "$ARCHIVE_FULL"

cd *
ISABELLE_NAME="$(basename "$PWD")"

echo "Z3_NON_COMMERCIAL=yes" >> etc/settings
echo "ISABELLE_FULL_TEST=true" >> etc/settings

echo -n > src/Doc/ROOT

env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
  ./bin/isabelle build $JOBS -s -c -a -o browser_info \
    -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
RC="$?"

cd ..

if [ "$RC" = 0 ]; then
  chmod -R g=o "$ISABELLE_NAME"
  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
fi

# clean up
cd /tmp
rm -rf "$TMP"

exit "$RC"