73 |
68 |
74 |
69 |
75 ## main |
70 ## main |
76 |
71 |
77 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE" |
72 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE" |
78 ARCHIVE_BASE=$(basename "$ARCHIVE") |
73 ARCHIVE_BASE="$(basename "$ARCHIVE")" |
79 ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD") |
74 ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")" |
80 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE" |
75 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE" |
81 |
76 |
82 ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz) |
77 ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)" |
83 ISABELLE_HOME="$TMP/$ISABELLE_NAME" |
78 ISABELLE_HOME="$TMP/$ISABELLE_NAME" |
84 |
79 |
85 |
80 |
86 # build logics |
81 # build logics |
87 |
82 |
88 mkdir "$TMP" || fail "Cannot create directory $TMP" |
83 mkdir "$TMP" || fail "Cannot create directory $TMP" |
89 |
84 |
90 cd "$TMP" |
85 cd "$TMP" |
91 "$TAR" xzf "$ARCHIVE_FULL" |
86 tar xzf "$ARCHIVE_FULL" |
92 cd "$ISABELLE_NAME" |
87 cd "$ISABELLE_NAME" |
93 |
88 |
94 perl -pi \ |
89 perl -pi \ |
95 -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \ |
90 -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \ |
96 -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \ |
91 -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-M 1 -p 2":;' \ |
97 etc/settings |
92 etc/settings |
98 |
93 |
99 if [ -n "$DO_LIBRARY" ]; then |
94 if [ -n "$DO_LIBRARY" ]; then |
100 perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \ |
95 perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \ |
101 etc/settings |
96 etc/settings |
102 fi |
97 fi |
103 |
98 |
104 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER) |
99 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER) |
105 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \ |
100 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \ |
132 |
127 |
133 chmod -R g=o "$TMP" |
128 chmod -R g=o "$TMP" |
134 chgrp -R isabelle "$TMP" |
129 chgrp -R isabelle "$TMP" |
135 |
130 |
136 if [ -n "$DO_LIBRARY" ]; then |
131 if [ -n "$DO_LIBRARY" ]; then |
137 "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \ |
132 tar cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \ |
138 gzip -f "${ISABELLE_NAME}_library.tar" |
133 gzip -f "${ISABELLE_NAME}_library.tar" |
139 cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR" |
134 cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR" |
140 else |
135 else |
141 for IMG in HOL HOL-Nominal ZF |
136 for IMG in HOL HOL-Nominal ZF |
142 do |
137 do |
143 "$TAR" cf "${IMG}_$PLATFORM.tar" \ |
138 tar cf "${IMG}_$PLATFORM.tar" \ |
144 "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \ |
139 "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \ |
145 "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz" |
140 "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz" |
146 gzip -f "${IMG}_$PLATFORM.tar" |
141 gzip -f "${IMG}_$PLATFORM.tar" |
147 cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR" |
142 cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR" |
148 done |
143 done |