Admin/build

prove_common: include all sorts from context into statement, check shyps of result;
Drule.norm_hhf_eqs;

#!/usr/bin/env bash
#
# $Id$
#
# Administrative build for Isabelle source distribution.

## global environment

#paranoia setting for sunbroy
PATH="/usr/local/dist/DIR/j2sdk1.5.0/bin:$PATH"

PATH="/home/scala/scala/bin:$PATH"


## directory layout

ISABELLE_DIR="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"

if [ -d "$ISABELLE_DIR/Distribution" ]; then
  ISABELLE_TOOL="$ISABELLE_DIR/Distribution/bin/isabelle"
  ISABELLE_LIB="$ISABELLE_DIR/Distribution/lib"
  ISABELLE_SRC="$ISABELLE_DIR"
  ISABELLE_DOC_SRC="$ISABELLE_DIR/Doc"
else
  ISABELLE_TOOL="$ISABELLE_DIR/bin/isabelle"
  ISABELLE_LIB="$ISABELLE_DIR/lib"
  ISABELLE_SRC="$ISABELLE_DIR/src"
  ISABELLE_DOC_SRC="$ISABELLE_DIR/doc-src"
fi


## diagnostics

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

function usage()
{
  cat <<EOF

Usage: $PRG [MODULES]

  Produce Isabelle distribution modules from current repository sources.
  The MODULES list may contain any of the following:

    all             all modules below
    browser         graph browser (requires jdk)
    doc             documentation (requires latex and rail)
    jars            JVM components (requires jdk and scala)

EOF
  exit 1
}

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


## process command line

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

MODULES="$@"; shift "$#"


## modules

function build_all ()
{
  build_doc
  build_browser
  build_jars
}


function build_browser ()
{
  echo "###"
  echo "### Building graph browser ..."
  echo "###"

  cd "$ISABELLE_LIB/browser"
  make clean all || fail "Failed to build graph browser!"
}


function build_doc ()
{
  echo "###"
  echo "### Building documentation ..."
  echo "###"

  cd "$ISABELLE_DOC_SRC"
  for DOC in $(cat Dirs)
  do
    pushd "$DOC" >/dev/null
    make clean dvi || fail "DVI document for $DOC failed!"
    make clean pdf || fail "PDF document for $DOC failed!"
    popd >/dev/null
  done
}


function build_jars ()
{
  echo "###"
  echo "### Building JVM components ..."
  echo "###"

  type -p scalac >/dev/null || fail "Scala compiler unavailable"

  pushd "$ISABELLE_SRC/Pure" >/dev/null
  "$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!"
  popd >/dev/null

  if [ -d "$HOME/lib/jedit/current" ]; then
    pushd "$ISABELLE_LIB/jedit/plugin" >/dev/null
    ./mk
    [ -f ../isabelle.jar ] || fail "Failed to build jEdit plugin!"
    popd >/dev/null
  else
    echo "Warning: skipping jedit plugin"
  fi
}


## main

for MODULE in $MODULES
do
  case $MODULE in
    all) build_all;;
    browser) build_browser;;
    doc) build_doc;;
    jars) build_jars;;
    *) fail "Bad module $MODULE"
  esac
done