wneuper/isa: Admin/makebin@9e7a4d4bba54

     1 #!/usr/bin/env bash

2 #

     3 # makebin -- make Isabelle logic images for current platform

     6 ## global settings

     8 TMP="/var/tmp/isabelle-makebin$$"

    10 export THIS_IS_ISABELLE_MAKEBIN=true

    13 ## diagnostics

    15 PRG=$(basename "$0")

    17 function usage()

    18 {

    19   echo

    20   echo "Usage: $PRG [OPTIONS] ARCHIVE"

    21   echo

    22   echo "  Options are:"

    23   echo "    -l           produce library"

    24   echo "    -n           dry run"

    25   echo

    26   echo "  Precompile Isabelle for the current platform."

    27   echo

    28   exit 1

    29 }

    31 function fail()

    32 {

    33   echo "$1" >&2

    34   exit 2

    35 }

    38 ## process command line

    40 # options

    42 DO_LIBRARY=""

    43 DRY_RUN=""

    45 while getopts "ln" OPT

    46 do

    47   case "$OPT" in

    48     l)

    49       DO_LIBRARY=true

    50       ;;

    51     n)

    52       DRY_RUN=true

    53       ;;

    54     \?)

    55       usage

    56       ;;

    57   esac

    58 done

    60 shift $(($OPTIND - 1))

    63 # args

    65 [ "$#" -gt 1 ] && usage

    67 ARCHIVE="$1"; shift

    70 ## main

    72 [ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"

    73 ARCHIVE_BASE="$(basename "$ARCHIVE")"

    74 ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"

    75 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"

    77 ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"

    78 ISABELLE_HOME="$TMP/$ISABELLE_NAME"

    81 # build logics

    83 mkdir "$TMP" || fail "Cannot create directory $TMP"

    85 cd "$TMP"

    86 tar xzf "$ARCHIVE_FULL"

    87 cd "$ISABELLE_NAME"

    89 perl -pi \

    90   -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \

    91   etc/settings

    93 if [ -n "$DO_LIBRARY" ]; then

    94   perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \

    95     etc/settings

    96 fi

    98 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)

    99 [ -f "$ISABELLE_HOME_USER/etc/settings" ] && \

   100   echo "### WARNING!  Personal Isabelle settings present. " >&2

   102 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)

   103 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)

   105 if [ -n "$DRY_RUN" ]; then

   106   mkdir -p "heaps/$COMPILER/log"

   107   touch "heaps/$COMPILER/HOL"

   108   touch "heaps/$COMPILER/log/HOL.gz"

   109   touch "heaps/$COMPILER/HOL-Nominal"

   110   touch "heaps/$COMPILER/log/HOL-Nominal.gz"

   111   touch "heaps/$COMPILER/HOLCF"

   112   touch "heaps/$COMPILER/log/HOLCF.gz"

   113   touch "heaps/$COMPILER/ZF"

   114   touch "heaps/$COMPILER/log/ZF.gz"

   115   mkdir browser_info

   116 elif [ -n "$DO_LIBRARY" ]; then

   117   ./build -bait

   118 else

   119   ./build -b -m HOL-Nominal HOL

   120   ./build -b HOLCF

   121   ./build -b ZF

   122   rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"

   123 fi

   126 # prepare result

   128 cd "$TMP"

   130 chmod -R g=o "$TMP"

   131 chgrp -R isabelle "$TMP"

   133 if [ -n "$DO_LIBRARY" ]; then

   134   tar cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \

   135     gzip -f "${ISABELLE_NAME}_library.tar"

   136     cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"

   137 else

   138   for IMG in HOL HOL-Nominal HOLCF ZF

   139   do

   140     tar cf "${IMG}_$PLATFORM.tar" \

   141       "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \

   142       "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"

   143     gzip -f "${IMG}_$PLATFORM.tar"

   144     cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"

   145   done

   146 fi

   149 # clean up

   150 cd /tmp

   151 rm -rf "$TMP"

author	wenzelm
	Wed, 02 Jun 2010 14:55:37 +0200
changeset 37283	9e7a4d4bba54
parent 34238	b28be884edda
child 37286	344468462338
permissions	-rwxr-xr-x