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
     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 export COPYFILE_DISABLE=true
    65 
    66 TMP="/var/tmp/isabelle-makedist$$"
    67 mkdir "$TMP" || fail "Cannot create directory: \"$TMP\""
    68 
    69 cd "$TMP"
    70 tar -x -z -f "$ARCHIVE_FULL"
    71 
    72 cd *
    73 ISABELLE_NAME="$(basename "$PWD")"
    74 
    75 echo "Z3_NON_COMMERCIAL=yes" >> etc/settings
    76 echo "ISABELLE_FULL_TEST=true" >> etc/settings
    77 
    78 echo -n > src/Doc/ROOT
    79 
    80 env ISABELLE_IDENTIFIER="${ISABELLE_NAME}-build" \
    81   ./bin/isabelle build $JOBS -s -c -a -o browser_info \
    82     -o "document=pdf" -o "document_variants=document:outline=/proof,/ML"
    83 RC="$?"
    84 
    85 cd ..
    86 
    87 if [ "$RC" = 0 ]; then
    88   chmod -R g=o "$ISABELLE_NAME"
    89   tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
    90 fi
    91 
    92 # clean up
    93 cd /tmp
    94 rm -rf "$TMP"
    95 
    96 exit "$RC"