Admin/Release/build_library
changeset 50899 506ff6abfde0
parent 50864 e932198be619
child 53913 5ff12177a067
equal deleted inserted replaced
50895:3a1edaa0dc6d 50899:506ff6abfde0
       
     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"