Admin/polyml/build
author wenzelm
Wed, 03 Nov 2010 21:53:56 +0100
changeset 40335 3e4bb6e7c3ca
parent 39620 ff694044a55b
child 46875 162b0c46c559
permissions -rwxr-xr-x
feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38468
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
     1
#!/usr/bin/env bash
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
     2
#
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
     3
# Multi-platform build script for Poly/ML
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
     4
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
     5
THIS="$(cd "$(dirname "$0")"; pwd)"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
     6
PRG="$(basename "$0")"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
     7
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
     8
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
     9
# diagnostics
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    10
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    11
function usage()
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    12
{
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    13
  echo
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    14
  echo "Usage: $PRG SOURCE TARGET [OPTIONS]"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    15
  echo
38472
3c5716b2e7b6 pro-forma support for further platforms;
wenzelm
parents: 38468
diff changeset
    16
  echo "  Build Poly/ML in SOURCE directory for given platform in TARGET,"
3c5716b2e7b6 pro-forma support for further platforms;
wenzelm
parents: 38468
diff changeset
    17
  echo "  using the usual Isabelle platform identifiers."
38468
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    18
  echo
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    19
  echo "  Additional options for ./configure may be given, e.g. --with-gmp"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    20
  echo
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    21
  exit 1
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    22
}
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    23
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    24
function fail()
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    25
{
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    26
  echo "$1" >&2
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    27
  exit 2
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    28
}
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    29
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    30
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    31
# command line args
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    32
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    33
[ "$#" -eq 0 ] && usage
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    34
SOURCE="$1"; shift
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    35
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    36
[ "$#" -eq 0 ] && usage
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    37
TARGET="$1"; shift
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    38
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    39
USER_OPTIONS=("$@")
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    40
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    41
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    42
# main
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    43
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    44
[ -d "$SOURCE" ] || fail "Bad source directory: \"$SOURCE\""
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    45
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    46
case "$TARGET" in
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    47
  x86-linux)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    48
    OPTIONS=()
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    49
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    50
  x86_64-linux)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    51
    OPTIONS=()
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    52
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    53
  x86-darwin)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    54
    OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3'
38585
62b414d8051c reactivated -segprot options, just to make double-sure;
wenzelm
parents: 38472
diff changeset
    55
      CXXFLAGS='-arch i686 -O3' CCASFLAGS='-arch i686 -O3'
62b414d8051c reactivated -segprot options, just to make double-sure;
wenzelm
parents: 38472
diff changeset
    56
      LDFLAGS='-segprot POLY rwx rwx')
38468
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    57
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    58
  x86_64-darwin)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    59
    OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3'
38585
62b414d8051c reactivated -segprot options, just to make double-sure;
wenzelm
parents: 38472
diff changeset
    60
      CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64'
62b414d8051c reactivated -segprot options, just to make double-sure;
wenzelm
parents: 38472
diff changeset
    61
      LDFLAGS='-segprot POLY rwx rwx')
38468
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    62
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    63
  x86-cygwin)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    64
    OPTIONS=()
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    65
    ;;
38472
3c5716b2e7b6 pro-forma support for further platforms;
wenzelm
parents: 38468
diff changeset
    66
  ppc-darwin | sparc-solaris | x86-solaris | x86-bsd)
3c5716b2e7b6 pro-forma support for further platforms;
wenzelm
parents: 38468
diff changeset
    67
    OPTIONS=()
3c5716b2e7b6 pro-forma support for further platforms;
wenzelm
parents: 38468
diff changeset
    68
    ;;
38468
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    69
  *)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    70
    fail "Bad platform identifier: \"$TARGET\""
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    71
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    72
esac
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    73
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    74
(
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    75
  cd "$SOURCE"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    76
  make distclean
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    77
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    78
  { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    79
    make compiler && \
39620
ff694044a55b make compiler doubly sure;
wenzelm
parents: 38585
diff changeset
    80
    make compiler && \
38468
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    81
    make install; } || fail "Build failed"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    82
)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    83
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    84
mkdir -p "$TARGET"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    85
mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    86
mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    87
rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    88
rm -rf "$SOURCE/$TARGET/share"