Admin/polyml/build
author wenzelm
Sat Nov 13 12:32:21 2010 +0100 (2010-11-13 ago)
changeset 40521 8896bd93488e
parent 39620 ff694044a55b
child 46875 162b0c46c559
permissions -rwxr-xr-x
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
wenzelm@38468
     1
#!/usr/bin/env bash
wenzelm@38468
     2
#
wenzelm@38468
     3
# Multi-platform build script for Poly/ML
wenzelm@38468
     4
wenzelm@38468
     5
THIS="$(cd "$(dirname "$0")"; pwd)"
wenzelm@38468
     6
PRG="$(basename "$0")"
wenzelm@38468
     7
wenzelm@38468
     8
wenzelm@38468
     9
# diagnostics
wenzelm@38468
    10
wenzelm@38468
    11
function usage()
wenzelm@38468
    12
{
wenzelm@38468
    13
  echo
wenzelm@38468
    14
  echo "Usage: $PRG SOURCE TARGET [OPTIONS]"
wenzelm@38468
    15
  echo
wenzelm@38472
    16
  echo "  Build Poly/ML in SOURCE directory for given platform in TARGET,"
wenzelm@38472
    17
  echo "  using the usual Isabelle platform identifiers."
wenzelm@38468
    18
  echo
wenzelm@38468
    19
  echo "  Additional options for ./configure may be given, e.g. --with-gmp"
wenzelm@38468
    20
  echo
wenzelm@38468
    21
  exit 1
wenzelm@38468
    22
}
wenzelm@38468
    23
wenzelm@38468
    24
function fail()
wenzelm@38468
    25
{
wenzelm@38468
    26
  echo "$1" >&2
wenzelm@38468
    27
  exit 2
wenzelm@38468
    28
}
wenzelm@38468
    29
wenzelm@38468
    30
wenzelm@38468
    31
# command line args
wenzelm@38468
    32
wenzelm@38468
    33
[ "$#" -eq 0 ] && usage
wenzelm@38468
    34
SOURCE="$1"; shift
wenzelm@38468
    35
wenzelm@38468
    36
[ "$#" -eq 0 ] && usage
wenzelm@38468
    37
TARGET="$1"; shift
wenzelm@38468
    38
wenzelm@38468
    39
USER_OPTIONS=("$@")
wenzelm@38468
    40
wenzelm@38468
    41
wenzelm@38468
    42
# main
wenzelm@38468
    43
wenzelm@38468
    44
[ -d "$SOURCE" ] || fail "Bad source directory: \"$SOURCE\""
wenzelm@38468
    45
wenzelm@38468
    46
case "$TARGET" in
wenzelm@38468
    47
  x86-linux)
wenzelm@38468
    48
    OPTIONS=()
wenzelm@38468
    49
    ;;
wenzelm@38468
    50
  x86_64-linux)
wenzelm@38468
    51
    OPTIONS=()
wenzelm@38468
    52
    ;;
wenzelm@38468
    53
  x86-darwin)
wenzelm@38468
    54
    OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3'
wenzelm@38585
    55
      CXXFLAGS='-arch i686 -O3' CCASFLAGS='-arch i686 -O3'
wenzelm@38585
    56
      LDFLAGS='-segprot POLY rwx rwx')
wenzelm@38468
    57
    ;;
wenzelm@38468
    58
  x86_64-darwin)
wenzelm@38468
    59
    OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3'
wenzelm@38585
    60
      CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64'
wenzelm@38585
    61
      LDFLAGS='-segprot POLY rwx rwx')
wenzelm@38468
    62
    ;;
wenzelm@38468
    63
  x86-cygwin)
wenzelm@38468
    64
    OPTIONS=()
wenzelm@38468
    65
    ;;
wenzelm@38472
    66
  ppc-darwin | sparc-solaris | x86-solaris | x86-bsd)
wenzelm@38472
    67
    OPTIONS=()
wenzelm@38472
    68
    ;;
wenzelm@38468
    69
  *)
wenzelm@38468
    70
    fail "Bad platform identifier: \"$TARGET\""
wenzelm@38468
    71
    ;;
wenzelm@38468
    72
esac
wenzelm@38468
    73
wenzelm@38468
    74
(
wenzelm@38468
    75
  cd "$SOURCE"
wenzelm@38468
    76
  make distclean
wenzelm@38468
    77
wenzelm@38468
    78
  { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
wenzelm@38468
    79
    make compiler && \
wenzelm@39620
    80
    make compiler && \
wenzelm@38468
    81
    make install; } || fail "Build failed"
wenzelm@38468
    82
)
wenzelm@38468
    83
wenzelm@38468
    84
mkdir -p "$TARGET"
wenzelm@38468
    85
mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
wenzelm@38468
    86
mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
wenzelm@38468
    87
rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
wenzelm@38468
    88
rm -rf "$SOURCE/$TARGET/share"