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