removed obsolete dry-run option;
authorwenzelm
Sun, 06 Jun 2010 18:29:10 +0200
changeset 37340 f3492868bbfd
parent 37339 5350cd2ae2c4
child 37342 7299d0bf82c5
removed obsolete dry-run option; just one archive for heaps, with the full cumulative collection (proper dependencies for rebuild);
Admin/makebin
--- a/Admin/makebin	Sun Jun 06 17:37:44 2010 +0200
+++ b/Admin/makebin	Sun Jun 06 18:29:10 2010 +0200
@@ -21,7 +21,6 @@
   echo
   echo "  Options are:"
   echo "    -l           produce library"
-  echo "    -n           dry run"
   echo
   echo "  Precompile Isabelle for the current platform."
   echo
@@ -40,7 +39,6 @@
 # options
 
 DO_LIBRARY=""
-DRY_RUN=""
 
 while getopts "ln" OPT
 do
@@ -48,9 +46,6 @@
     l)
       DO_LIBRARY=true
       ;;
-    n)
-      DRY_RUN=true
-      ;;
     \?)
       usage
       ;;
@@ -102,24 +97,12 @@
 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
 
-if [ -n "$DRY_RUN" ]; then
-  mkdir -p "heaps/$COMPILER/log"
-  touch "heaps/$COMPILER/HOL"
-  touch "heaps/$COMPILER/log/HOL.gz"
-  touch "heaps/$COMPILER/HOL-Nominal"
-  touch "heaps/$COMPILER/log/HOL-Nominal.gz"
-  touch "heaps/$COMPILER/HOLCF"
-  touch "heaps/$COMPILER/log/HOLCF.gz"
-  touch "heaps/$COMPILER/ZF"
-  touch "heaps/$COMPILER/log/ZF.gz"
-  mkdir browser_info
-elif [ -n "$DO_LIBRARY" ]; then
+if [ -n "$DO_LIBRARY" ]; then
   ./build -bait
 else
   ./build -b -m HOL-Nominal HOL
   ./build -b HOLCF
   ./build -b ZF
-  rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
 fi
 
 
@@ -131,18 +114,9 @@
 chgrp -R isabelle "$TMP"
 
 if [ -n "$DO_LIBRARY" ]; then
-  tar cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
-    gzip -f "${ISABELLE_NAME}_library.tar"
-    cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
+  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
 else
-  for IMG in HOL HOL-Nominal HOLCF ZF
-  do
-    tar cf "${IMG}_$PLATFORM.tar" \
-      "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
-      "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
-    gzip -f "${IMG}_$PLATFORM.tar"
-    cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
-  done
+  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"
 fi