clarified -l option;
authorwenzelm
Fri Mar 01 22:31:48 2002 +0100 (2002-03-01)
changeset 1300140ba2eee948e
parent 13000 e56aedec11f3
child 13002 e844d0ee15d5
clarified -l option;
tuned;
Admin/makebin
     1.1 --- a/Admin/makebin	Fri Mar 01 22:30:01 2002 +0100
     1.2 +++ b/Admin/makebin	Fri Mar 01 22:31:48 2002 +0100
     1.3 @@ -27,8 +27,8 @@
     1.4    echo "Usage: $PRG [OPTIONS] ARCHIVE"
     1.5    echo
     1.6    echo "  Options are:"
     1.7 -  echo "    -l           include library"
     1.8 -  echo "    -t           test run -- no build phase"
     1.9 +  echo "    -l           produce library"
    1.10 +  echo "    -n           dry run"
    1.11    echo
    1.12    echo "  Precompile Isabelle for the current platform."
    1.13    echo
    1.14 @@ -47,16 +47,16 @@
    1.15  # options
    1.16  
    1.17  DO_LIBRARY=""
    1.18 -TEST_RUN=""
    1.19 +DRY_RUN=""
    1.20  
    1.21 -while getopts "lt" OPT
    1.22 +while getopts "ln" OPT
    1.23  do
    1.24    case "$OPT" in
    1.25      l)
    1.26        DO_LIBRARY=true
    1.27        ;;
    1.28 -    t)
    1.29 -      TEST_RUN=true
    1.30 +    n)
    1.31 +      DRY_RUN=true
    1.32        ;;
    1.33      \?)
    1.34        usage
    1.35 @@ -93,8 +93,13 @@
    1.36  "$TAR" xzf "$ARCHIVE_FULL"
    1.37  cd "$ISABELLE_NAME"
    1.38  
    1.39 -#activate default for precompiled distribution ...
    1.40 -perl -pi -e 's/#ISABELLE_USEDIR_OPTIONS/ISABELLE_USEDIR_OPTIONS/' etc/settings
    1.41 +if [ -n "$DO_LIBRARY" ]; then
    1.42 +  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-i true -d pdf"/' \
    1.43 +    etc/settings
    1.44 +else
    1.45 +  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 2"/' \
    1.46 +    etc/settings
    1.47 +fi
    1.48  
    1.49  ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
    1.50  [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
    1.51 @@ -103,7 +108,7 @@
    1.52  COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
    1.53  PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
    1.54  
    1.55 -if [ -n "$TEST_RUN" ]; then
    1.56 +if [ -n "$DRY_RUN" ]; then
    1.57    mkdir -p "heaps/$COMPILER/log"
    1.58    touch "heaps/$COMPILER/HOL"
    1.59    touch "heaps/$COMPILER/log/HOL.gz"
    1.60 @@ -112,10 +117,11 @@
    1.61    touch "heaps/$COMPILER/ZF"
    1.62    touch "heaps/$COMPILER/log/ZF.gz"
    1.63    mkdir browser_info
    1.64 +elif [ -n "$DO_LIBRARY" ]; then
    1.65 +  ./build -bait
    1.66  else
    1.67    ./build -b -m HOL-Real HOL
    1.68    ./build -b ZF
    1.69 -  [ -n "$DO_LIBRARY" ] && ./build -bait
    1.70    rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
    1.71  fi
    1.72  
    1.73 @@ -127,20 +133,20 @@
    1.74  chmod -R g=o "$TMP"
    1.75  chgrp -R isabelle "$TMP"
    1.76  
    1.77 -for IMG in HOL HOL-Real ZF
    1.78 -do
    1.79 -  "$TAR" cf "${IMG}_$PLATFORM.tar" \
    1.80 -    "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
    1.81 -    "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
    1.82 -  gzip -f "${IMG}_$PLATFORM.tar"
    1.83 -  cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
    1.84 -
    1.85 -  if [ -n "$DO_LIBRARY" ]; then
    1.86 -    "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
    1.87 -      gzip -f "${ISABELLE_NAME}_library.tar"
    1.88 -      cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
    1.89 -  fi
    1.90 -done
    1.91 +if [ -n "$DO_LIBRARY" ]; then
    1.92 +  "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
    1.93 +    gzip -f "${ISABELLE_NAME}_library.tar"
    1.94 +    cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
    1.95 +else
    1.96 +  for IMG in HOL HOL-Real ZF
    1.97 +  do
    1.98 +    "$TAR" cf "${IMG}_$PLATFORM.tar" \
    1.99 +      "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
   1.100 +      "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
   1.101 +    gzip -f "${IMG}_$PLATFORM.tar"
   1.102 +    cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
   1.103 +  done
   1.104 +fi
   1.105  
   1.106  
   1.107  # clean up