|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # makebin -- make Isabelle logic images for current platform |
|
4 |
|
5 |
|
6 ## global settings |
|
7 |
|
8 TMP="/var/tmp/isabelle-makebin$$" |
|
9 |
|
10 |
|
11 ## diagnostics |
|
12 |
|
13 PRG=$(basename "$0") |
|
14 |
|
15 function usage() |
|
16 { |
|
17 echo |
|
18 echo "Usage: $PRG [OPTIONS] ARCHIVE" |
|
19 echo |
|
20 echo " Options are:" |
|
21 echo " -l produce library" |
|
22 echo |
|
23 echo " Precompile Isabelle for the current platform." |
|
24 echo |
|
25 exit 1 |
|
26 } |
|
27 |
|
28 function fail() |
|
29 { |
|
30 echo "$1" >&2 |
|
31 exit 2 |
|
32 } |
|
33 |
|
34 |
|
35 ## process command line |
|
36 |
|
37 # options |
|
38 |
|
39 DO_LIBRARY="" |
|
40 |
|
41 while getopts "l" OPT |
|
42 do |
|
43 case "$OPT" in |
|
44 l) |
|
45 DO_LIBRARY=true |
|
46 ;; |
|
47 \?) |
|
48 usage |
|
49 ;; |
|
50 esac |
|
51 done |
|
52 |
|
53 shift $(($OPTIND - 1)) |
|
54 |
|
55 |
|
56 # args |
|
57 |
|
58 [ "$#" -gt 1 ] && usage |
|
59 |
|
60 ARCHIVE="$1"; shift |
|
61 |
|
62 |
|
63 ## main |
|
64 |
|
65 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE" |
|
66 ARCHIVE_BASE="$(basename "$ARCHIVE")" |
|
67 ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")" |
|
68 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE" |
|
69 |
|
70 ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)" |
|
71 ISABELLE_HOME="$TMP/$ISABELLE_NAME" |
|
72 |
|
73 |
|
74 # build logics |
|
75 |
|
76 mkdir "$TMP" || fail "Cannot create directory $TMP" |
|
77 |
|
78 cd "$TMP" |
|
79 tar xzf "$ARCHIVE_FULL" |
|
80 cd "$ISABELLE_NAME" |
|
81 |
|
82 perl -pi \ |
|
83 -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \ |
|
84 etc/settings |
|
85 |
|
86 if [ -n "$DO_LIBRARY" ]; then |
|
87 perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \ |
|
88 etc/settings |
|
89 fi |
|
90 |
|
91 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER) |
|
92 |
|
93 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER) |
|
94 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM) |
|
95 |
|
96 if [ -n "$DO_LIBRARY" ]; then |
|
97 ./build -bait -m all |
|
98 else |
|
99 ./build -b HOL |
|
100 fi |
|
101 |
|
102 |
|
103 # prepare result |
|
104 |
|
105 cd "$TMP" |
|
106 |
|
107 chmod -R g=o "$TMP" |
|
108 chgrp -R isabelle "$TMP" |
|
109 |
|
110 if [ -n "$DO_LIBRARY" ]; then |
|
111 tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info" |
|
112 else |
|
113 tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps" |
|
114 fi |
|
115 |
|
116 |
|
117 # clean up |
|
118 rm -rf "$TMP" |