Admin/makebin
changeset 13001 40ba2eee948e
parent 12985 9db054a40247
child 14024 213dcc39358f
equal deleted inserted replaced
13000:e56aedec11f3 13001:40ba2eee948e
    25 {
    25 {
    26   echo
    26   echo
    27   echo "Usage: $PRG [OPTIONS] ARCHIVE"
    27   echo "Usage: $PRG [OPTIONS] ARCHIVE"
    28   echo
    28   echo
    29   echo "  Options are:"
    29   echo "  Options are:"
    30   echo "    -l           include library"
    30   echo "    -l           produce library"
    31   echo "    -t           test run -- no build phase"
    31   echo "    -n           dry run"
    32   echo
    32   echo
    33   echo "  Precompile Isabelle for the current platform."
    33   echo "  Precompile Isabelle for the current platform."
    34   echo
    34   echo
    35   exit 1
    35   exit 1
    36 }
    36 }
    45 ## process command line
    45 ## process command line
    46 
    46 
    47 # options
    47 # options
    48 
    48 
    49 DO_LIBRARY=""
    49 DO_LIBRARY=""
    50 TEST_RUN=""
    50 DRY_RUN=""
    51 
    51 
    52 while getopts "lt" OPT
    52 while getopts "ln" OPT
    53 do
    53 do
    54   case "$OPT" in
    54   case "$OPT" in
    55     l)
    55     l)
    56       DO_LIBRARY=true
    56       DO_LIBRARY=true
    57       ;;
    57       ;;
    58     t)
    58     n)
    59       TEST_RUN=true
    59       DRY_RUN=true
    60       ;;
    60       ;;
    61     \?)
    61     \?)
    62       usage
    62       usage
    63       ;;
    63       ;;
    64   esac
    64   esac
    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 #activate default for precompiled distribution ...
    96 if [ -n "$DO_LIBRARY" ]; then
    97 perl -pi -e 's/#ISABELLE_USEDIR_OPTIONS/ISABELLE_USEDIR_OPTIONS/' etc/settings
    97   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-i true -d pdf"/' \
       
    98     etc/settings
       
    99 else
       
   100   perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 2"/' \
       
   101     etc/settings
       
   102 fi
    98 
   103 
    99 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
   104 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
   100 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   105 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
   101   echo "### WARNING!  Personal Isabelle settings present. " >&2
   106   echo "### WARNING!  Personal Isabelle settings present. " >&2
   102 
   107 
   103 COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
   108 COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
   104 PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
   109 PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
   105 
   110 
   106 if [ -n "$TEST_RUN" ]; then
   111 if [ -n "$DRY_RUN" ]; then
   107   mkdir -p "heaps/$COMPILER/log"
   112   mkdir -p "heaps/$COMPILER/log"
   108   touch "heaps/$COMPILER/HOL"
   113   touch "heaps/$COMPILER/HOL"
   109   touch "heaps/$COMPILER/log/HOL.gz"
   114   touch "heaps/$COMPILER/log/HOL.gz"
   110   touch "heaps/$COMPILER/HOL-Real"
   115   touch "heaps/$COMPILER/HOL-Real"
   111   touch "heaps/$COMPILER/log/HOL-Real.gz"
   116   touch "heaps/$COMPILER/log/HOL-Real.gz"
   112   touch "heaps/$COMPILER/ZF"
   117   touch "heaps/$COMPILER/ZF"
   113   touch "heaps/$COMPILER/log/ZF.gz"
   118   touch "heaps/$COMPILER/log/ZF.gz"
   114   mkdir browser_info
   119   mkdir browser_info
       
   120 elif [ -n "$DO_LIBRARY" ]; then
       
   121   ./build -bait
   115 else
   122 else
   116   ./build -b -m HOL-Real HOL
   123   ./build -b -m HOL-Real HOL
   117   ./build -b ZF
   124   ./build -b ZF
   118   [ -n "$DO_LIBRARY" ] && ./build -bait
       
   119   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   125   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
   120 fi
   126 fi
   121 
   127 
   122 
   128 
   123 # prepare result
   129 # prepare result
   125 cd "$TMP"
   131 cd "$TMP"
   126 
   132 
   127 chmod -R g=o "$TMP"
   133 chmod -R g=o "$TMP"
   128 chgrp -R isabelle "$TMP"
   134 chgrp -R isabelle "$TMP"
   129 
   135 
   130 for IMG in HOL HOL-Real ZF
   136 if [ -n "$DO_LIBRARY" ]; then
   131 do
   137   "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
   132   "$TAR" cf "${IMG}_$PLATFORM.tar" \
   138     gzip -f "${ISABELLE_NAME}_library.tar"
   133     "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
   139     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
   134     "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
   140 else
   135   gzip -f "${IMG}_$PLATFORM.tar"
   141   for IMG in HOL HOL-Real ZF
   136   cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
   142   do
   137 
   143     "$TAR" cf "${IMG}_$PLATFORM.tar" \
   138   if [ -n "$DO_LIBRARY" ]; then
   144       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
   139     "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
   145       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
   140       gzip -f "${ISABELLE_NAME}_library.tar"
   146     gzip -f "${IMG}_$PLATFORM.tar"
   141       cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
   147     cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
   142   fi
   148   done
   143 done
   149 fi
   144 
   150 
   145 
   151 
   146 # clean up
   152 # clean up
   147 cd /tmp
   153 cd /tmp
   148 rm -rf "$TMP"
   154 rm -rf "$TMP"