Admin/makebin
author kleing
Tue Apr 20 04:09:19 2004 +0200 (2004-04-20)
changeset 14633 8553a957cffa
parent 14024 213dcc39358f
child 15971 c0c4088edccf
permissions -rwxr-xr-x
add HOL4 image, needs fixing
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@10082
    10
DISTBASE=~/tmp/isadist
wenzelm@12427
    11
TMP="/var/tmp/isabelle-makebin$$"
wenzelm@10082
    12
wenzelm@10082
    13
TAR=tar
wenzelm@10082
    14
type -path gtar >/dev/null && TAR=gtar
wenzelm@10082
    15
wenzelm@10097
    16
export THIS_IS_ISABELLE_BUILD=true
wenzelm@12985
    17
export THIS_IS_ISABELLE_ADMIN=true
wenzelm@10097
    18
wenzelm@10082
    19
wenzelm@10082
    20
## diagnostics
wenzelm@10082
    21
wenzelm@10082
    22
PRG=$(basename "$0")
wenzelm@10082
    23
wenzelm@10082
    24
function usage()
wenzelm@10082
    25
{
wenzelm@10082
    26
  echo
wenzelm@12827
    27
  echo "Usage: $PRG [OPTIONS] ARCHIVE"
wenzelm@10082
    28
  echo
wenzelm@12827
    29
  echo "  Options are:"
wenzelm@13001
    30
  echo "    -l           produce library"
wenzelm@13001
    31
  echo "    -n           dry run"
wenzelm@12827
    32
  echo
wenzelm@12827
    33
  echo "  Precompile Isabelle for the current platform."
wenzelm@10082
    34
  echo
wenzelm@10082
    35
  exit 1
wenzelm@10082
    36
}
wenzelm@10082
    37
wenzelm@10082
    38
function fail()
wenzelm@10082
    39
{
wenzelm@10082
    40
  echo "$1" >&2
wenzelm@10082
    41
  exit 2
wenzelm@10082
    42
}
wenzelm@10082
    43
wenzelm@10082
    44
wenzelm@10082
    45
## process command line
wenzelm@10082
    46
wenzelm@12827
    47
# options
wenzelm@12827
    48
wenzelm@12827
    49
DO_LIBRARY=""
wenzelm@13001
    50
DRY_RUN=""
wenzelm@12827
    51
wenzelm@13001
    52
while getopts "ln" OPT
wenzelm@12827
    53
do
wenzelm@12827
    54
  case "$OPT" in
wenzelm@12827
    55
    l)
wenzelm@12827
    56
      DO_LIBRARY=true
wenzelm@12827
    57
      ;;
wenzelm@13001
    58
    n)
wenzelm@13001
    59
      DRY_RUN=true
wenzelm@12827
    60
      ;;
wenzelm@12827
    61
    \?)
wenzelm@12827
    62
      usage
wenzelm@12827
    63
      ;;
wenzelm@12827
    64
  esac
wenzelm@12827
    65
done
wenzelm@12827
    66
wenzelm@12827
    67
shift $(($OPTIND - 1))
wenzelm@12827
    68
wenzelm@12827
    69
wenzelm@12827
    70
# args
wenzelm@12827
    71
wenzelm@10082
    72
[ "$#" -gt 1 ] && usage
wenzelm@10082
    73
wenzelm@10082
    74
ARCHIVE="$1"; shift
wenzelm@10082
    75
wenzelm@10082
    76
wenzelm@10082
    77
## main
wenzelm@10082
    78
wenzelm@10082
    79
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
wenzelm@10082
    80
ARCHIVE_BASE=$(basename "$ARCHIVE")
wenzelm@10082
    81
ARCHIVE_DIR=$(cd $(dirname "$ARCHIVE"); echo "$PWD")
wenzelm@10082
    82
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
wenzelm@10082
    83
wenzelm@10082
    84
ISABELLE_NAME=$(basename "$ARCHIVE_BASE" .tar.gz)
wenzelm@10082
    85
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
wenzelm@10082
    86
wenzelm@10082
    87
wenzelm@10082
    88
# build logics
wenzelm@10082
    89
wenzelm@10082
    90
mkdir "$TMP" || fail "Cannot create directory $TMP"
wenzelm@10082
    91
wenzelm@10082
    92
cd "$TMP"
wenzelm@10087
    93
"$TAR" xzf "$ARCHIVE_FULL"
wenzelm@10082
    94
cd "$ISABELLE_NAME"
wenzelm@10082
    95
kleing@14633
    96
# FIXME: ugly hack to get proper HOL4 image
kleing@14633
    97
# needs HOL4 proof terms installed in ~/isabelle/proofs
kleing@14633
    98
# desperately needs fix for next release!
kleing@14633
    99
cat > src/HOL/Import/HOL/ROOT.ML <<EOF
kleing@14633
   100
with_path ".." use_thy "HOL4Compat";
kleing@14633
   101
with_path ".." use_thy "HOL4Syntax";
kleing@14633
   102
use_thy "HOL4Prob";
kleing@14633
   103
use_thy "HOL4";
kleing@14633
   104
EOF
kleing@14633
   105
wenzelm@13001
   106
if [ -n "$DO_LIBRARY" ]; then
wenzelm@13001
   107
  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-i true -d pdf"/' \
wenzelm@13001
   108
    etc/settings
wenzelm@13001
   109
else
wenzelm@13001
   110
  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 2"/' \
wenzelm@13001
   111
    etc/settings
wenzelm@13001
   112
fi
wenzelm@11576
   113
wenzelm@10082
   114
ISABELLE_HOME_USER=$(./bin/isatool getenv -b ISABELLE_HOME_USER)
wenzelm@10082
   115
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
wenzelm@10082
   116
  echo "### WARNING!  Personal Isabelle settings present. " >&2
wenzelm@10082
   117
wenzelm@10082
   118
COMPILER=$(./bin/isatool getenv -b ML_IDENTIFIER)
wenzelm@10082
   119
PLATFORM=$(./bin/isatool getenv -b ML_PLATFORM)
wenzelm@10082
   120
wenzelm@13001
   121
if [ -n "$DRY_RUN" ]; then
wenzelm@12827
   122
  mkdir -p "heaps/$COMPILER/log"
wenzelm@10082
   123
  touch "heaps/$COMPILER/HOL"
wenzelm@12827
   124
  touch "heaps/$COMPILER/log/HOL.gz"
kleing@14024
   125
  touch "heaps/$COMPILER/HOL-Complex"
kleing@14024
   126
  touch "heaps/$COMPILER/log/HOL-Complex.gz"
kleing@14633
   127
  touch "heaps/$COMPILER/HOL4"
kleing@14633
   128
  touch "heaps/$COMPILER/log/HOL4.gz"
wenzelm@10082
   129
  touch "heaps/$COMPILER/ZF"
wenzelm@12827
   130
  touch "heaps/$COMPILER/log/ZF.gz"
wenzelm@12827
   131
  mkdir browser_info
wenzelm@13001
   132
elif [ -n "$DO_LIBRARY" ]; then
wenzelm@13001
   133
  ./build -bait
wenzelm@10082
   134
else
kleing@14024
   135
  ./build -b -m HOL-Complex HOL
wenzelm@10082
   136
  ./build -b ZF
kleing@14633
   137
  perl -pi -e 's/^ISABELLE_USEDIR_OPTIONS=.*$/ISABELLE_USEDIR_OPTIONS="-p 1"/' \
kleing@14633
   138
    etc/settings
kleing@14633
   139
  ./build -b -m HOL4 HOL
wenzelm@10082
   140
  rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
wenzelm@10082
   141
fi
wenzelm@10082
   142
wenzelm@10082
   143
wenzelm@10082
   144
# prepare result
wenzelm@10082
   145
wenzelm@10082
   146
cd "$TMP"
wenzelm@10082
   147
wenzelm@10082
   148
chmod -R g=o "$TMP"
wenzelm@10082
   149
chgrp -R isabelle "$TMP"
wenzelm@10082
   150
wenzelm@13001
   151
if [ -n "$DO_LIBRARY" ]; then
wenzelm@13001
   152
  "$TAR" cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
wenzelm@13001
   153
    gzip -f "${ISABELLE_NAME}_library.tar"
wenzelm@13001
   154
    cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
wenzelm@13001
   155
else
kleing@14633
   156
  for IMG in HOL HOL-Complex HOL4 ZF
wenzelm@13001
   157
  do
wenzelm@13001
   158
    "$TAR" cf "${IMG}_$PLATFORM.tar" \
wenzelm@13001
   159
      "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
wenzelm@13001
   160
      "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
wenzelm@13001
   161
    gzip -f "${IMG}_$PLATFORM.tar"
wenzelm@13001
   162
    cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
wenzelm@13001
   163
  done
wenzelm@13001
   164
fi
wenzelm@10082
   165
wenzelm@10082
   166
wenzelm@10082
   167
# clean up
wenzelm@10082
   168
cd /tmp
wenzelm@10082
   169
rm -rf "$TMP"