equal
deleted
inserted
replaced
89 |
89 |
90 cd "$TMP" |
90 cd "$TMP" |
91 "$TAR" xzf "$ARCHIVE_FULL" |
91 "$TAR" xzf "$ARCHIVE_FULL" |
92 cd "$ISABELLE_NAME" |
92 cd "$ISABELLE_NAME" |
93 |
93 |
94 # FIXME: ugly hack to get proper HOL4 image |
|
95 # needs HOL4 proof terms installed in ~/isabelle/proofs |
|
96 # desperately needs fix for next release! |
|
97 cat > src/HOL/Import/HOL/ROOT.ML <<EOF |
|
98 with_path ".." use_thy "HOL4Compat"; |
|
99 with_path ".." use_thy "HOL4Syntax"; |
|
100 use_thy "HOL4Prob"; |
|
101 use_thy "HOL4"; |
|
102 EOF |
|
103 |
|
104 perl -pi \ |
94 perl -pi \ |
105 -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \ |
95 -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \ |
106 -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \ |
96 -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \ |
107 etc/settings |
97 etc/settings |
108 |
98 |
122 mkdir -p "heaps/$COMPILER/log" |
112 mkdir -p "heaps/$COMPILER/log" |
123 touch "heaps/$COMPILER/HOL" |
113 touch "heaps/$COMPILER/HOL" |
124 touch "heaps/$COMPILER/log/HOL.gz" |
114 touch "heaps/$COMPILER/log/HOL.gz" |
125 touch "heaps/$COMPILER/HOL-Complex" |
115 touch "heaps/$COMPILER/HOL-Complex" |
126 touch "heaps/$COMPILER/log/HOL-Complex.gz" |
116 touch "heaps/$COMPILER/log/HOL-Complex.gz" |
127 touch "heaps/$COMPILER/HOL4" |
|
128 touch "heaps/$COMPILER/log/HOL4.gz" |
|
129 touch "heaps/$COMPILER/ZF" |
117 touch "heaps/$COMPILER/ZF" |
130 touch "heaps/$COMPILER/log/ZF.gz" |
118 touch "heaps/$COMPILER/log/ZF.gz" |
131 mkdir browser_info |
119 mkdir browser_info |
132 elif [ -n "$DO_LIBRARY" ]; then |
120 elif [ -n "$DO_LIBRARY" ]; then |
133 ./build -bait |
121 ./build -bait |
134 else |
122 else |
135 ./build -b -m HOL-Complex HOL |
123 ./build -b -m HOL-Complex HOL |
136 ./build -b -m HOL4 HOL |
|
137 ./build -b ZF |
124 ./build -b ZF |
138 rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL" |
125 rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL" |
139 fi |
126 fi |
140 |
127 |
141 |
128 |
149 if [ -n "$DO_LIBRARY" ]; then |
136 if [ -n "$DO_LIBRARY" ]; then |
150 "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \ |
137 "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \ |
151 gzip -f "${ISABELLE_NAME}_library.tar" |
138 gzip -f "${ISABELLE_NAME}_library.tar" |
152 cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR" |
139 cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR" |
153 else |
140 else |
154 for IMG in HOL HOL-Complex HOL4 ZF |
141 for IMG in HOL HOL-Complex ZF |
155 do |
142 do |
156 "$TAR" cf "${IMG}_$PLATFORM.tar" \ |
143 "$TAR" cf "${IMG}_$PLATFORM.tar" \ |
157 "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \ |
144 "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \ |
158 "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz" |
145 "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz" |
159 gzip -f "${IMG}_$PLATFORM.tar" |
146 gzip -f "${IMG}_$PLATFORM.tar" |