Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Admin/makebin
author wenzelm
Wed, 21 Sep 2005 21:00:57 +0200
changeset 17575 c45677c1aea0
parent 17573 4de614cc6509
child 17660 94bbe14c088e
permissions -rwxr-xr-x
tuned; 
     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 

    18 

    19 ## diagnostics

    20 

    21 PRG=$(basename "$0")

    22 

    23 function usage()

    24 {

    25   echo

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

    27   echo

    28   echo "  Options are:"

    29   echo "    -l           produce library"

    30   echo "    -n           dry run"

    31   echo

    32   echo "  Precompile Isabelle for the current platform."

    33   echo

    34   exit 1

    35 }

    36 

    37 function fail()

    38 {

    39   echo "$1" >&2

    40   exit 2

    41 }

    42 

    43 

    44 ## process command line

    45 

    46 # options

    47 

    48 DO_LIBRARY=""

    49 DRY_RUN=""

    50 

    51 while getopts "ln" OPT

    52 do

    53   case "$OPT" in

    54     l)

    55       DO_LIBRARY=true

    56       ;;

    57     n)

    58       DRY_RUN=true

    59       ;;

    60     \?)

    61       usage

    62       ;;

    63   esac

    64 done

    65 

    66 shift $(($OPTIND - 1))

    67 

    68 

    69 # args

    70 

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

    72 

    73 ARCHIVE="$1"; shift

    74 

    75 

    76 ## main

    77 

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

    79 ARCHIVE_BASE=$(basename "$ARCHIVE")

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

    81 ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"

    82 

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

    84 ISABELLE_HOME="$TMP/$ISABELLE_NAME"

    85 

    86 

    87 # build logics

    88 

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

    90 

    91 cd "$TMP"

    92 "$TAR" xzf "$ARCHIVE_FULL"

    93 cd "$ISABELLE_NAME"

    94 

    95 # FIXME: ugly hack to get proper HOL4 image

    96 # needs HOL4 proof terms installed in ~/isabelle/proofs

    97 # desperately needs fix for next release!

    98 cat > src/HOL/Import/HOL/ROOT.ML <<EOF

    99 with_path ".." use_thy "HOL4Compat";

   100 with_path ".." use_thy "HOL4Syntax";

   101 use_thy "HOL4Prob";

   102 use_thy "HOL4";

   103 EOF

   104 

   105 perl -pi \

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

   107   -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \

   108   etc/settings

   109 

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

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

   112     etc/settings

   113 fi

   114 

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

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

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

   118 

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

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

   121 

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

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

   124   touch "heaps/$COMPILER/HOL"

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

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

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

   128   touch "heaps/$COMPILER/HOL4"

   129   touch "heaps/$COMPILER/log/HOL4.gz"

   130   touch "heaps/$COMPILER/ZF"

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

   132   mkdir browser_info

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

   134   ./build -bait

   135 else

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

   137   ./build -b -m HOL4 HOL

   138   ./build -b ZF

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

   140 fi

   141 

   142 

   143 # prepare result

   144 

   145 cd "$TMP"

   146 

   147 chmod -R g=o "$TMP"

   148 chgrp -R isabelle "$TMP"

   149 

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

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

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

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

   154 else

   155   for IMG in HOL HOL-Complex HOL4 ZF

   156   do

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

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

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

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

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

   162   done

   163 fi

   164 

   165 

   166 # clean up

   167 cd /tmp

   168 rm -rf "$TMP"
wneuper/isa