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