equal
deleted
inserted
replaced
19 echo |
19 echo |
20 echo "Usage: $PRG [OPTIONS] ARCHIVE" |
20 echo "Usage: $PRG [OPTIONS] ARCHIVE" |
21 echo |
21 echo |
22 echo " Options are:" |
22 echo " Options are:" |
23 echo " -l produce library" |
23 echo " -l produce library" |
24 echo " -n dry run" |
|
25 echo |
24 echo |
26 echo " Precompile Isabelle for the current platform." |
25 echo " Precompile Isabelle for the current platform." |
27 echo |
26 echo |
28 exit 1 |
27 exit 1 |
29 } |
28 } |
38 ## process command line |
37 ## process command line |
39 |
38 |
40 # options |
39 # options |
41 |
40 |
42 DO_LIBRARY="" |
41 DO_LIBRARY="" |
43 DRY_RUN="" |
|
44 |
42 |
45 while getopts "ln" OPT |
43 while getopts "ln" OPT |
46 do |
44 do |
47 case "$OPT" in |
45 case "$OPT" in |
48 l) |
46 l) |
49 DO_LIBRARY=true |
47 DO_LIBRARY=true |
50 ;; |
|
51 n) |
|
52 DRY_RUN=true |
|
53 ;; |
48 ;; |
54 \?) |
49 \?) |
55 usage |
50 usage |
56 ;; |
51 ;; |
57 esac |
52 esac |
100 echo "### WARNING! Personal Isabelle settings present. " >&2 |
95 echo "### WARNING! Personal Isabelle settings present. " >&2 |
101 |
96 |
102 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER) |
97 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER) |
103 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM) |
98 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM) |
104 |
99 |
105 if [ -n "$DRY_RUN" ]; then |
100 if [ -n "$DO_LIBRARY" ]; then |
106 mkdir -p "heaps/$COMPILER/log" |
|
107 touch "heaps/$COMPILER/HOL" |
|
108 touch "heaps/$COMPILER/log/HOL.gz" |
|
109 touch "heaps/$COMPILER/HOL-Nominal" |
|
110 touch "heaps/$COMPILER/log/HOL-Nominal.gz" |
|
111 touch "heaps/$COMPILER/HOLCF" |
|
112 touch "heaps/$COMPILER/log/HOLCF.gz" |
|
113 touch "heaps/$COMPILER/ZF" |
|
114 touch "heaps/$COMPILER/log/ZF.gz" |
|
115 mkdir browser_info |
|
116 elif [ -n "$DO_LIBRARY" ]; then |
|
117 ./build -bait |
101 ./build -bait |
118 else |
102 else |
119 ./build -b -m HOL-Nominal HOL |
103 ./build -b -m HOL-Nominal HOL |
120 ./build -b HOLCF |
104 ./build -b HOLCF |
121 ./build -b ZF |
105 ./build -b ZF |
122 rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL" |
|
123 fi |
106 fi |
124 |
107 |
125 |
108 |
126 # prepare result |
109 # prepare result |
127 |
110 |
129 |
112 |
130 chmod -R g=o "$TMP" |
113 chmod -R g=o "$TMP" |
131 chgrp -R isabelle "$TMP" |
114 chgrp -R isabelle "$TMP" |
132 |
115 |
133 if [ -n "$DO_LIBRARY" ]; then |
116 if [ -n "$DO_LIBRARY" ]; then |
134 tar cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \ |
117 tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info" |
135 gzip -f "${ISABELLE_NAME}_library.tar" |
|
136 cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR" |
|
137 else |
118 else |
138 for IMG in HOL HOL-Nominal HOLCF ZF |
119 tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps" |
139 do |
|
140 tar cf "${IMG}_$PLATFORM.tar" \ |
|
141 "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \ |
|
142 "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz" |
|
143 gzip -f "${IMG}_$PLATFORM.tar" |
|
144 cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR" |
|
145 done |
|
146 fi |
120 fi |
147 |
121 |
148 |
122 |
149 # clean up |
123 # clean up |
150 cd /tmp |
124 cd /tmp |