author | wenzelm |
Tue, 15 Jan 2013 12:30:23 +0100 | |
changeset 50899 | 506ff6abfde0 |
parent 50864 | Admin/Release/makedist_library@e932198be619 |
child 53913 | 5ff12177a067 |
permissions | -rwxr-xr-x |
12721 | 1 |
#!/usr/bin/env bash |
10082 | 2 |
# |
50899
506ff6abfde0
grand-unified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
50864
diff
changeset
|
3 |
# build Isabelle HTML library from platform bundle |
10082 | 4 |
|
5 |
## diagnostics |
|
6 |
||
7 |
PRG=$(basename "$0") |
|
8 |
||
9 |
function usage() |
|
10 |
{ |
|
11 |
echo |
|
12827 | 12 |
echo "Usage: $PRG [OPTIONS] ARCHIVE" |
10082 | 13 |
echo |
12827 | 14 |
echo " Options are:" |
50864 | 15 |
echo " -j INT maximum number of parallel jobs (default 1)" |
12827 | 16 |
echo |
50864 | 17 |
echo " Build Isabelle HTML library from platform bundle." |
10082 | 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 |
||
12827 | 31 |
# options |
32 |
||
50864 | 33 |
JOBS="" |
12827 | 34 |
|
50864 | 35 |
while getopts "j:" OPT |
12827 | 36 |
do |
37 |
case "$OPT" in |
|
50864 | 38 |
j) |
39 |
JOBS="-j $OPTARG" |
|
12827 | 40 |
;; |
41 |
\?) |
|
42 |
usage |
|
43 |
;; |
|
44 |
esac |
|
45 |
done |
|
46 |
||
47 |
shift $(($OPTIND - 1)) |
|
48 |
||
49 |
||
50 |
# args |
|
51 |
||
50864 | 52 |
[ "$#" -ne 1 ] && usage |
10082 | 53 |
|
54 |
ARCHIVE="$1"; shift |
|
55 |
||
50864 | 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 |
||
10082 | 61 |
|
62 |
## main |
|
63 |
||
50864 | 64 |
export COPYFILE_DISABLE=true |
10082 | 65 |
|
50864 | 66 |
TMP="/var/tmp/isabelle-makedist$$" |
67 |
mkdir "$TMP" || fail "Cannot create directory: \"$TMP\"" |
|
10082 | 68 |
|
69 |
cd "$TMP" |
|
50864 | 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 |
|
10082 | 79 |
|
50864 | 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="$?" |
|
17575 | 84 |
|
50864 | 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" |
|
13001 | 90 |
fi |
11576
c418146c4763
activate default ISABELLE_USEDIR_OPTIONS for precompiled distribution;
wenzelm
parents:
10307
diff
changeset
|
91 |
|
50864 | 92 |
# clean up |
93 |
cd /tmp |
|
94 |
rm -rf "$TMP" |
|
10082 | 95 |
|
50864 | 96 |
exit "$RC" |