Admin/Release/build_library
author hoelzl
Tue Mar 26 12:20:55 2013 +0100 (2013-03-26)
changeset 51521 36fa825e0ea7
parent 50899 506ff6abfde0
child 53913 5ff12177a067
permissions -rwxr-xr-x
merge RComplete into RealDef
wenzelm@12721
     1
#!/usr/bin/env bash
wenzelm@10082
     2
#
wenzelm@50899
     3
# build Isabelle HTML library from platform bundle
wenzelm@10082
     4
wenzelm@10082
     5
## diagnostics
wenzelm@10082
     6
wenzelm@10082
     7
PRG=$(basename "$0")
wenzelm@10082
     8
wenzelm@10082
     9
function usage()
wenzelm@10082
    10
{
wenzelm@10082
    11
  echo
wenzelm@12827
    12
  echo "Usage: $PRG [OPTIONS] ARCHIVE"
wenzelm@10082
    13
  echo
wenzelm@12827
    14
  echo "  Options are:"
wenzelm@50864
    15
  echo "    -j INT       maximum number of parallel jobs (default 1)"
wenzelm@12827
    16
  echo
wenzelm@50864
    17
  echo "  Build Isabelle HTML library from platform bundle."
wenzelm@10082
    18
  echo
wenzelm@10082
    19
  exit 1
wenzelm@10082
    20
}
wenzelm@10082
    21
wenzelm@10082
    22
function fail()
wenzelm@10082
    23
{
wenzelm@10082
    24
  echo "$1" >&2
wenzelm@10082
    25
  exit 2
wenzelm@10082
    26
}
wenzelm@10082
    27
wenzelm@10082
    28
wenzelm@10082
    29
## process command line
wenzelm@10082
    30
wenzelm@12827
    31
# options
wenzelm@12827
    32
wenzelm@50864
    33
JOBS=""
wenzelm@12827
    34
wenzelm@50864
    35
while getopts "j:" OPT
wenzelm@12827
    36
do
wenzelm@12827
    37
  case "$OPT" in
wenzelm@50864
    38
    j)
wenzelm@50864
    39
      JOBS="-j $OPTARG"
wenzelm@12827
    40
      ;;
wenzelm@12827
    41
    \?)
wenzelm@12827
    42
      usage
wenzelm@12827
    43
      ;;
wenzelm@12827
    44
  esac
wenzelm@12827
    45
done
wenzelm@12827
    46
wenzelm@12827
    47
shift $(($OPTIND - 1))
wenzelm@12827
    48
wenzelm@12827
    49
wenzelm@12827
    50
# args
wenzelm@12827
    51
wenzelm@50864
    52
[ "$#" -ne 1 ] && usage
wenzelm@10082
    53
wenzelm@10082
    54
ARCHIVE="$1"; shift
wenzelm@10082
    55
wenzelm@50864
    56
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
wenzelm@50864
    57
ARCHIVE_BASE="$(basename "$ARCHIVE")"
wenzelm@50864
    58
ARCHIVE_DIR="$(cd "$(dirname "$ARCHIVE")"; echo "$PWD")"
wenzelm@50864
    59
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
wenzelm@50864
    60
wenzelm@10082
    61
wenzelm@10082
    62
## main
wenzelm@10082
    63
wenzelm@50864
    64
export COPYFILE_DISABLE=true
wenzelm@10082
    65
wenzelm@50864
    66
TMP="/var/tmp/isabelle-makedist$$"
wenzelm@50864
    67
mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
wenzelm@10082
    68
wenzelm@10082
    69
cd "$TMP"
wenzelm@50864
    70
tar -x -z -f "$ARCHIVE_FULL"
wenzelm@50864
    71
wenzelm@50864
    72
cd *
wenzelm@50864
    73
ISABELLE_NAME="$(basename "$PWD")"
wenzelm@50864
    74
wenzelm@50864
    75
echo "Z3_NON_COMMERCIAL=yes" >> etc/settings
wenzelm@50864
    76
echo "ISABELLE_FULL_TEST=true" >> etc/settings
wenzelm@50864
    77
wenzelm@50864
    78
echo -n > src/Doc/ROOT
wenzelm@10082
    79
wenzelm@50864
    80
env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
wenzelm@50864
    81
  ./bin/isabelle build $JOBS -s -c -a -o browser_info \
wenzelm@50864
    82
    -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
wenzelm@50864
    83
RC="$?"
wenzelm@17575
    84
wenzelm@50864
    85
cd ..
wenzelm@50864
    86
wenzelm@50864
    87
if [ "$RC" = 0 ]; then
wenzelm@50864
    88
  chmod -R g=o "$ISABELLE_NAME"
wenzelm@50864
    89
  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
wenzelm@13001
    90
fi
wenzelm@11576
    91
wenzelm@50864
    92
# clean up
wenzelm@50864
    93
cd /tmp
wenzelm@50864
    94
rm -rf "$TMP"
wenzelm@10082
    95
wenzelm@50864
    96
exit "$RC"