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