Admin/makebin
author wenzelm
Fri Apr 03 12:08:09 2009 +0200 (2009-04-03)
changeset 30862 dfd77f471c22
parent 28504 7ad7d7d6df47
child 33918 5945e023bab7
permissions -rwxr-xr-x
single-threaded build;
misc tuning and simplification;
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@13001
    24
  echo "    -n           dry run"
wenzelm@12827
    25
  echo
wenzelm@12827
    26
  echo "  Precompile Isabelle for the current platform."
wenzelm@10082
    27
  echo
wenzelm@10082
    28
  exit 1
wenzelm@10082
    29
}
wenzelm@10082
    30
wenzelm@10082
    31
function fail()
wenzelm@10082
    32
{
wenzelm@10082
    33
  echo "$1" >&2
wenzelm@10082
    34
  exit 2
wenzelm@10082
    35
}
wenzelm@10082
    36
wenzelm@10082
    37
wenzelm@10082
    38
## process command line
wenzelm@10082
    39
wenzelm@12827
    40
# options
wenzelm@12827
    41
wenzelm@12827
    42
DO_LIBRARY=""
wenzelm@13001
    43
DRY_RUN=""
wenzelm@12827
    44
wenzelm@13001
    45
while getopts "ln" OPT
wenzelm@12827
    46
do
wenzelm@12827
    47
  case "$OPT" in
wenzelm@12827
    48
    l)
wenzelm@12827
    49
      DO_LIBRARY=true
wenzelm@12827
    50
      ;;
wenzelm@13001
    51
    n)
wenzelm@13001
    52
      DRY_RUN=true
wenzelm@12827
    53
      ;;
wenzelm@12827
    54
    \?)
wenzelm@12827
    55
      usage
wenzelm@12827
    56
      ;;
wenzelm@12827
    57
  esac
wenzelm@12827
    58
done
wenzelm@12827
    59
wenzelm@12827
    60
shift $(($OPTIND - 1))
wenzelm@12827
    61
wenzelm@12827
    62
wenzelm@12827
    63
# args
wenzelm@12827
    64
wenzelm@10082
    65
[ "$#" -gt 1 ] && usage
wenzelm@10082
    66
wenzelm@10082
    67
ARCHIVE="$1"; shift
wenzelm@10082
    68
wenzelm@10082
    69
wenzelm@10082
    70
## main
wenzelm@10082
    71
wenzelm@10082
    72
[ ! -f "$ARCHIVE" ] && fail "Bad archive file $ARCHIVE"
wenzelm@30862
    73
ARCHIVE_BASE="$(basename "$ARCHIVE")"
wenzelm@30862
    74
ARCHIVE_DIR="$(cd $(dirname "$ARCHIVE"); echo "$PWD")"
wenzelm@10082
    75
ARCHIVE_FULL="$ARCHIVE_DIR/$ARCHIVE_BASE"
wenzelm@10082
    76
wenzelm@30862
    77
ISABELLE_NAME="$(basename "$ARCHIVE_BASE" .tar.gz)"
wenzelm@10082
    78
ISABELLE_HOME="$TMP/$ISABELLE_NAME"
wenzelm@10082
    79
wenzelm@10082
    80
wenzelm@10082
    81
# build logics
wenzelm@10082
    82
wenzelm@10082
    83
mkdir "$TMP" || fail "Cannot create directory $TMP"
wenzelm@10082
    84
wenzelm@10082
    85
cd "$TMP"
wenzelm@30862
    86
tar xzf "$ARCHIVE_FULL"
wenzelm@10082
    87
cd "$ISABELLE_NAME"
wenzelm@10082
    88
wenzelm@17575
    89
perl -pi \
wenzelm@30862
    90
  -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1":;' \
wenzelm@30862
    91
  -e 's:^HOL_USEDIR_OPTIONS=.*$:HOL_USEDIR_OPTIONS="-M 1 -p 2":;' \
wenzelm@17575
    92
  etc/settings
wenzelm@17575
    93
wenzelm@13001
    94
if [ -n "$DO_LIBRARY" ]; then
wenzelm@30862
    95
  perl -pi -e 's:^ISABELLE_USEDIR_OPTIONS=.*$:ISABELLE_USEDIR_OPTIONS="-M 1 -p 1 -i true -d pdf -V outline=/proof,/ML":;' \
wenzelm@13001
    96
    etc/settings
wenzelm@13001
    97
fi
wenzelm@11576
    98
wenzelm@28504
    99
ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
wenzelm@10082
   100
[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
wenzelm@10082
   101
  echo "### WARNING!  Personal Isabelle settings present. " >&2
wenzelm@10082
   102
wenzelm@28504
   103
COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
wenzelm@28504
   104
PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
wenzelm@10082
   105
wenzelm@13001
   106
if [ -n "$DRY_RUN" ]; then
wenzelm@12827
   107
  mkdir -p "heaps/$COMPILER/log"
wenzelm@10082
   108
  touch "heaps/$COMPILER/HOL"
wenzelm@12827
   109
  touch "heaps/$COMPILER/log/HOL.gz"
wenzelm@27587
   110
  touch "heaps/$COMPILER/HOL-Nominal"
wenzelm@27587
   111
  touch "heaps/$COMPILER/log/HOL-Nominal.gz"
wenzelm@10082
   112
  touch "heaps/$COMPILER/ZF"
wenzelm@12827
   113
  touch "heaps/$COMPILER/log/ZF.gz"
wenzelm@12827
   114
  mkdir browser_info
wenzelm@13001
   115
elif [ -n "$DO_LIBRARY" ]; then
wenzelm@13001
   116
  ./build -bait
wenzelm@10082
   117
else
wenzelm@27587
   118
  ./build -b -m HOL-Nominal HOL
wenzelm@10082
   119
  ./build -b ZF
wenzelm@10082
   120
  rm -f "heaps/$COMPILER/Pure" "heaps/$COMPILER/FOL"
wenzelm@10082
   121
fi
wenzelm@10082
   122
wenzelm@10082
   123
wenzelm@10082
   124
# prepare result
wenzelm@10082
   125
wenzelm@10082
   126
cd "$TMP"
wenzelm@10082
   127
wenzelm@10082
   128
chmod -R g=o "$TMP"
wenzelm@10082
   129
chgrp -R isabelle "$TMP"
wenzelm@10082
   130
wenzelm@13001
   131
if [ -n "$DO_LIBRARY" ]; then
wenzelm@30862
   132
  tar cf "${ISABELLE_NAME}_library.tar" $ISABELLE_NAME/browser_info && \
wenzelm@13001
   133
    gzip -f "${ISABELLE_NAME}_library.tar"
wenzelm@13001
   134
    cp -f "${ISABELLE_NAME}_library.tar.gz" "$ARCHIVE_DIR"
wenzelm@13001
   135
else
wenzelm@27588
   136
  for IMG in HOL HOL-Nominal ZF
wenzelm@13001
   137
  do
wenzelm@30862
   138
    tar cf "${IMG}_$PLATFORM.tar" \
wenzelm@13001
   139
      "$ISABELLE_NAME/heaps/$COMPILER/$IMG" \
wenzelm@13001
   140
      "$ISABELLE_NAME/heaps/$COMPILER/log/$IMG.gz"
wenzelm@13001
   141
    gzip -f "${IMG}_$PLATFORM.tar"
wenzelm@13001
   142
    cp -f "${IMG}_$PLATFORM.tar.gz" "$ARCHIVE_DIR"
wenzelm@13001
   143
  done
wenzelm@13001
   144
fi
wenzelm@10082
   145
wenzelm@10082
   146
wenzelm@10082
   147
# clean up
wenzelm@10082
   148
cd /tmp
wenzelm@10082
   149
rm -rf "$TMP"