Mercurialisabelle / file revision
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
Admin/makebin
author paulson
Mon Jul 21 13:02:07 2003 +0200 (2003-07-21)
changeset 14120 3a73850c6c7d
parent 14024 213dcc39358f
child 14633 8553a957cffa
permissions -rwxr-xr-x
Tidied some examples 
     1 #!/usr/bin/env bash

     2 #

     3 # $Id$

     4 #

     5 # makebin -- make Isabelle logic images for current platform.

     6 

     7 

     8 ## global settings

     9 

    10 DISTBASE=~/tmp/isadist

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

    12 

    13 TAR=tar

    14 type -path gtar >/dev/null && TAR=gtar

    15 

    16 export THIS_IS_ISABELLE_BUILD=true

    17 export THIS_IS_ISABELLE_ADMIN=true

    18 

    19 

    20 ## diagnostics

    21 

    22 PRG=$(basename "$0")

    23 

    24 function usage()

    25 {

    26   echo

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

    28   echo

    29   echo "  Options are:"

    30   echo "    -l           produce library"

    31   echo "    -n           dry run"

    32   echo

    33   echo "  Precompile Isabelle for the current platform."

    34   echo

    35   exit 1

    36 }

    37 

    38 function fail()

    39 {

    40   echo "$1" >&2

    41   exit 2

    42 }

    43 

    44 

    45 ## process command line

    46 

    47 # options

    48 

    49 DO_LIBRARY=""

    50 DRY_RUN=""

    51 

    52 while getopts "ln" OPT

    53 do

    54   case "$OPT" in

    55     l)

    56       DO_LIBRARY=true

    57       ;;

    58     n)

    59       DRY_RUN=true

    60       ;;

    61     \?)

    62       usage

    63       ;;

    64   esac

    65 done

    66 

    67 shift $(($OPTIND - 1))

    68 

    69 

    70 # args

    71 

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

    73 

    74 ARCHIVE="$1"; shift

    75 

    76 

    77 ## main

    78 

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

    80 ARCHIVE_BASE=$(basename "$ARCHIVE")

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

    82 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"

    83 

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

    85 ISABELLE_HOME="$TMP/$ISABELLE_NAME"

    86 

    87 

    88 # build logics

    89 

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

    91 

    92 cd "$TMP"

    93 "$TAR" xzf "$ARCHIVE_FULL"

    94 cd "$ISABELLE_NAME"

    95 

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

    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

   103 

   104 ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)

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

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

   107 

   108 COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)

   109 PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)

   110 

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

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

   113   touch "heaps/$COMPILER/HOL"

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

   115   touch "heaps/$COMPILER/HOL-Complex"

   116   touch "heaps/$COMPILER/log/HOL-Complex.gz"

   117   touch "heaps/$COMPILER/ZF"

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

   119   mkdir browser_info

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

   121   ./build -bait

   122 else

   123   ./build -b -m HOL-Complex HOL

   124   ./build -b ZF

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

   126 fi

   127 

   128 

   129 # prepare result

   130 

   131 cd "$TMP"

   132 

   133 chmod -R g=o "$TMP"

   134 chgrp -R isabelle "$TMP"

   135 

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

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

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

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

   140 else

   141   for IMG in HOL HOL-Complex ZF

   142   do

   143     "$TAR" cf "${IMG}_$PLATFORM.tar" \

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

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

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

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

   148   done

   149 fi

   150 

   151 

   152 # clean up

   153 cd /tmp

   154 rm -rf "$TMP"
isabelle