Admin/makebin
author huffman
Wed Oct 13 10:27:26 2010 -0700 (2010-10-13)
changeset 40010 d7fdd84b959f
parent 37340 f3492868bbfd
child 40779 24851517ef15
permissions -rwxr-xr-x
edit comments
wenzelm@12721
     1
#!/usr/bin/env bash
wenzelm@10082
     2
#
wenzelm@30862
     3
# makebin -- make Isabelle logic images for current platform
wenzelm@10082
     4
wenzelm@10082
     5
wenzelm@10082
     6
## global settings
wenzelm@10082
     7
wenzelm@12427
     8
TMP="/var/tmp/isabelle-makebin$$"
wenzelm@10082
     9
wenzelm@27030
    10
export THIS_IS_ISABELLE_MAKEBIN=true
wenzelm@27030
    11
wenzelm@10082
    12
wenzelm@10082
    13
## diagnostics
wenzelm@10082
    14
wenzelm@10082
    15
PRG=$(basename "$0")
wenzelm@10082
    16
wenzelm@10082
    17
function usage()
wenzelm@10082
    18
{
wenzelm@10082
    19
  echo
wenzelm@12827
    20
  echo "Usage: $PRG [OPTIONS] ARCHIVE"
wenzelm@10082
    21
  echo
wenzelm@12827
    22
  echo "  Options are:"
wenzelm@13001
    23
  echo "    -l           produce library"
wenzelm@12827
    24
  echo
wenzelm@12827
    25
  echo "  Precompile Isabelle for the current platform."
wenzelm@10082
    26
  echo
wenzelm@10082
    27
  exit 1
wenzelm@10082
    28
}
wenzelm@10082
    29
wenzelm@10082
    30
function fail()
wenzelm@10082
    31
{
wenzelm@10082
    32
  echo "$1" >&2
wenzelm@10082
    33
  exit 2
wenzelm@10082
    34
}
wenzelm@10082
    35
wenzelm@10082
    36
wenzelm@10082
    37
## process command line
wenzelm@10082
    38
wenzelm@12827
    39
# options
wenzelm@12827
    40
wenzelm@12827
    41
DO_LIBRARY=""
wenzelm@12827
    42
wenzelm@13001
    43
while getopts "ln" OPT
wenzelm@12827
    44
do
wenzelm@12827
    45
  case "$OPT" in
wenzelm@12827
    46
    l)
wenzelm@12827
    47
      DO_LIBRARY=true
wenzelm@12827
    48
      ;;
wenzelm@12827
    49
    \?)
wenzelm@12827
    50
      usage
wenzelm@12827
    51
      ;;
wenzelm@12827
    52
  esac
wenzelm@12827
    53
done
wenzelm@12827
    54
wenzelm@12827
    55
shift $(($OPTIND - 1))
wenzelm@12827
    56
wenzelm@12827
    57
wenzelm@12827
    58
# args
wenzelm@12827
    59
wenzelm@10082
    60
[ "$#" -gt 1 ] && usage
wenzelm@10082
    61
wenzelm@10082
    62
ARCHIVE="$1"; shift
wenzelm@10082
    63
wenzelm@10082
    64
wenzelm@10082
    65
## main
wenzelm@10082
    66
wenzelm@10082
    67
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
wenzelm@30862
    68
ARCHIVE_BASE="$(basename "$ARCHIVE")"
wenzelm@30862
    69
ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
wenzelm@10082
    70
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
wenzelm@10082
    71
wenzelm@30862
    72
ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
wenzelm@10082
    73
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
wenzelm@10082
    74
wenzelm@10082
    75
wenzelm@10082
    76
# build logics
wenzelm@10082
    77
wenzelm@10082
    78
mkdir "$TMP" || fail "Cannot create directory $TMP"
wenzelm@10082
    79
wenzelm@10082
    80
cd "$TMP"
wenzelm@30862
    81
tar xzf "$ARCHIVE_FULL"
wenzelm@10082
    82
cd "$ISABELLE_NAME"
wenzelm@10082
    83
wenzelm@17575
    84
perl -pi \
wenzelm@37286
    85
  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1":;' \
wenzelm@17575
    86
  etc/settings
wenzelm@17575
    87
wenzelm@13001
    88
if [ -n "$DO_LIBRARY" ]; then
wenzelm@37286
    89
  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -i true -d pdf -V outline=/proof,/ML":;' \
wenzelm@13001
    90
    etc/settings
wenzelm@13001
    91
fi
wenzelm@11576
    92
wenzelm@28504
    93
ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
wenzelm@10082
    94
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
wenzelm@10082
    95
  echo "### WARNING!  Personal Isabelle settings present. " >&2
wenzelm@10082
    96
wenzelm@28504
    97
COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
wenzelm@28504
    98
PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
wenzelm@10082
    99
wenzelm@37340
   100
if [ -n "$DO_LIBRARY" ]; then
wenzelm@13001
   101
  ./build -bait
wenzelm@10082
   102
else
wenzelm@27587
   103
  ./build -b -m HOL-Nominal HOL
wenzelm@33918
   104
  ./build -b HOLCF
wenzelm@10082
   105
  ./build -b ZF
wenzelm@10082
   106
fi
wenzelm@10082
   107
wenzelm@10082
   108
wenzelm@10082
   109
# prepare result
wenzelm@10082
   110
wenzelm@10082
   111
cd "$TMP"
wenzelm@10082
   112
wenzelm@10082
   113
chmod -R g=o "$TMP"
wenzelm@10082
   114
chgrp -R isabelle "$TMP"
wenzelm@10082
   115
wenzelm@13001
   116
if [ -n "$DO_LIBRARY" ]; then
wenzelm@37340
   117
  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_library.tar.gz" "$ISABELLE_NAME/browser_info"
wenzelm@13001
   118
else
wenzelm@37340
   119
  tar -c -z -f "$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" "$ISABELLE_NAME/heaps"
wenzelm@13001
   120
fi
wenzelm@10082
   121
wenzelm@10082
   122
wenzelm@10082
   123
# clean up
wenzelm@10082
   124
cd /tmp
wenzelm@10082
   125
rm -rf "$TMP"