Admin/makebin
author wenzelm
Mon Jul 14 21:07:57 2008 +0200 (2008-07-14)
changeset 27588 0dd8d4c558f9
parent 27587 6f469a8aff10
child 28504 7ad7d7d6df47
permissions -rwxr-xr-x
removed HOL-Complex, which has been discontinued after Isabelle2008;
wenzelm@12721
     1
#!/usr/bin/env bash
wenzelm@10082
     2
#
wenzelm@10082
     3
# $Id$
wenzelm@10082
     4
#
wenzelm@10082
     5
# makebin -- make Isabelle logic images for current platform.
wenzelm@10082
     6
wenzelm@10082
     7
wenzelm@10082
     8
## global settings
wenzelm@10082
     9
wenzelm@12427
    10
TMP="/var/tmp/isabelle-makebin$$"
wenzelm@10082
    11
wenzelm@10082
    12
TAR=tar
wenzelm@10082
    13
type -path gtar >/dev/null && TAR=gtar
wenzelm@10082
    14
wenzelm@27030
    15
export THIS_IS_ISABELLE_MAKEBIN=true
wenzelm@27030
    16
wenzelm@10082
    17
wenzelm@10082
    18
## diagnostics
wenzelm@10082
    19
wenzelm@10082
    20
PRG=$(basename "$0")
wenzelm@10082
    21
wenzelm@10082
    22
function usage()
wenzelm@10082
    23
{
wenzelm@10082
    24
  echo
wenzelm@12827
    25
  echo "Usage: $PRG [OPTIONS] ARCHIVE"
wenzelm@10082
    26
  echo
wenzelm@12827
    27
  echo "  Options are:"
wenzelm@13001
    28
  echo "    -l           produce library"
wenzelm@13001
    29
  echo "    -n           dry run"
wenzelm@12827
    30
  echo
wenzelm@12827
    31
  echo "  Precompile Isabelle for the current platform."
wenzelm@10082
    32
  echo
wenzelm@10082
    33
  exit 1
wenzelm@10082
    34
}
wenzelm@10082
    35
wenzelm@10082
    36
function fail()
wenzelm@10082
    37
{
wenzelm@10082
    38
  echo "$1" >&2
wenzelm@10082
    39
  exit 2
wenzelm@10082
    40
}
wenzelm@10082
    41
wenzelm@10082
    42
wenzelm@10082
    43
## process command line
wenzelm@10082
    44
wenzelm@12827
    45
# options
wenzelm@12827
    46
wenzelm@12827
    47
DO_LIBRARY=""
wenzelm@13001
    48
DRY_RUN=""
wenzelm@12827
    49
wenzelm@13001
    50
while getopts "ln" OPT
wenzelm@12827
    51
do
wenzelm@12827
    52
  case "$OPT" in
wenzelm@12827
    53
    l)
wenzelm@12827
    54
      DO_LIBRARY=true
wenzelm@12827
    55
      ;;
wenzelm@13001
    56
    n)
wenzelm@13001
    57
      DRY_RUN=true
wenzelm@12827
    58
      ;;
wenzelm@12827
    59
    \?)
wenzelm@12827
    60
      usage
wenzelm@12827
    61
      ;;
wenzelm@12827
    62
  esac
wenzelm@12827
    63
done
wenzelm@12827
    64
wenzelm@12827
    65
shift $(($OPTIND - 1))
wenzelm@12827
    66
wenzelm@12827
    67
wenzelm@12827
    68
# args
wenzelm@12827
    69
wenzelm@10082
    70
[ "$#" -gt 1 ] && usage
wenzelm@10082
    71
wenzelm@10082
    72
ARCHIVE="$1"; shift
wenzelm@10082
    73
wenzelm@10082
    74
wenzelm@10082
    75
## main
wenzelm@10082
    76
wenzelm@10082
    77
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
wenzelm@10082
    78
ARCHIVE_BASE=$(basename "$ARCHIVE")
wenzelm@10082
    79
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
wenzelm@10082
    80
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
wenzelm@10082
    81
wenzelm@10082
    82
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
wenzelm@10082
    83
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
wenzelm@10082
    84
wenzelm@10082
    85
wenzelm@10082
    86
# build logics
wenzelm@10082
    87
wenzelm@10082
    88
mkdir "$TMP" || fail "Cannot create directory $TMP"
wenzelm@10082
    89
wenzelm@10082
    90
cd "$TMP"
wenzelm@10087
    91
"$TAR" xzf "$ARCHIVE_FULL"
wenzelm@10082
    92
cd "$ISABELLE_NAME"
wenzelm@10082
    93
wenzelm@17575
    94
perl -pi \
wenzelm@17575
    95
  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1":;' \
wenzelm@17575
    96
  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-p 2":;' \
wenzelm@17575
    97
  etc/settings
wenzelm@17575
    98
wenzelm@13001
    99
if [ -n "$DO_LIBRARY" ]; then
wenzelm@17575
   100
  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-p 1 -i true -d pdf -V outline=/proof,/ML":;' \
wenzelm@13001
   101
    etc/settings
wenzelm@13001
   102
fi
wenzelm@11576
   103
wenzelm@10082
   104
ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
wenzelm@10082
   105
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
wenzelm@10082
   106
  echo "### WARNING!  Personal Isabelle settings present. " >&2
wenzelm@10082
   107
wenzelm@10082
   108
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
wenzelm@10082
   109
PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
wenzelm@10082
   110
wenzelm@13001
   111
if [ -n "$DRY_RUN" ]; then
wenzelm@12827
   112
  mkdir -p "heaps/$COMPILER/log"
wenzelm@10082
   113
  touch "heaps/$COMPILER/HOL"
wenzelm@12827
   114
  touch "heaps/$COMPILER/log/HOL.gz"
wenzelm@27587
   115
  touch "heaps/$COMPILER/HOL-Nominal"
wenzelm@27587
   116
  touch "heaps/$COMPILER/log/HOL-Nominal.gz"
wenzelm@10082
   117
  touch "heaps/$COMPILER/ZF"
wenzelm@12827
   118
  touch "heaps/$COMPILER/log/ZF.gz"
wenzelm@12827
   119
  mkdir browser_info
wenzelm@13001
   120
elif [ -n "$DO_LIBRARY" ]; then
wenzelm@13001
   121
  ./build -bait
wenzelm@10082
   122
else
wenzelm@27587
   123
  ./build -b -m HOL-Nominal HOL
wenzelm@10082
   124
  ./build -b ZF
wenzelm@10082
   125
  rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
wenzelm@10082
   126
fi
wenzelm@10082
   127
wenzelm@10082
   128
wenzelm@10082
   129
# prepare result
wenzelm@10082
   130
wenzelm@10082
   131
cd "$TMP"
wenzelm@10082
   132
wenzelm@10082
   133
chmod -R g=o "$TMP"
wenzelm@10082
   134
chgrp -R isabelle "$TMP"
wenzelm@10082
   135
wenzelm@13001
   136
if [ -n "$DO_LIBRARY" ]; then
wenzelm@13001
   137
  "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
wenzelm@13001
   138
    gzip -f "${ISABELLE_NAME}_library.tar"
wenzelm@13001
   139
    cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
wenzelm@13001
   140
else
wenzelm@27588
   141
  for IMG in HOL HOL-Nominal ZF
wenzelm@13001
   142
  do
wenzelm@13001
   143
    "$TAR" cf "${IMG}_$PLATFORM.tar" \
wenzelm@13001
   144
      "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
wenzelm@13001
   145
      "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
wenzelm@13001
   146
    gzip -f "${IMG}_$PLATFORM.tar"
wenzelm@13001
   147
    cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
wenzelm@13001
   148
  done
wenzelm@13001
   149
fi
wenzelm@10082
   150
wenzelm@10082
   151
wenzelm@10082
   152
# clean up
wenzelm@10082
   153
cd /tmp
wenzelm@10082
   154
rm -rf "$TMP"