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