Admin/polyml/build
author wenzelm
Tue, 17 Aug 2010 18:04:08 +0200
changeset 38469 5c6c5d63f3c3
parent 38468 01d70ada9284
child 38472 3c5716b2e7b6
permissions -rwxr-xr-x
updated for prospective Poly/ML 5.4;
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
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    16
  echo "  Build Poly/ML in SOURCE directory for given platform in TARGET"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    17
  echo "  which is identified as follows:"
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 "    x86-linux    x86_64-linux"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    20
  echo "    x86-darwin   x86_64-darwin"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    21
  echo "    x86-cygwin"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    22
  echo
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    23
  echo "  Additional options for ./configure may be given, e.g. --with-gmp"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    24
  echo
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    25
  exit 1
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    26
}
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    27
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    28
function fail()
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
  echo "$1" >&2
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    31
  exit 2
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
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    34
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    35
# command line args
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    36
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    37
[ "$#" -eq 0 ] && usage
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    38
SOURCE="$1"; shift
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    39
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    40
[ "$#" -eq 0 ] && usage
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    41
TARGET="$1"; shift
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    42
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    43
USER_OPTIONS=("$@")
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    44
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
# main
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    47
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    48
[ -d "$SOURCE" ] || fail "Bad source directory: \"$SOURCE\""
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
case "$TARGET" in
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    51
  x86-linux)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    52
    OPTIONS=()
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    53
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    54
  x86_64-linux)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    55
    OPTIONS=()
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    56
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    57
  x86-darwin)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    58
    OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3'
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    59
      CXXFLAGS='-arch i686 -O3' CCASFLAGS='-arch i686 -O3')
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    60
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    61
  x86_64-darwin)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    62
    OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3'
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    63
      CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64')
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    64
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    65
  x86-cygwin)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    66
    OPTIONS=()
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    67
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    68
  *)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    69
    fail "Bad platform identifier: \"$TARGET\""
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    70
    ;;
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    71
esac
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    72
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
  cd "$SOURCE"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    75
  make distclean
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    76
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    77
  { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    78
    make compiler && \
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    79
    make install; } || fail "Build failed"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    80
)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    81
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    82
mkdir -p "$TARGET"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    83
mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    84
mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    85
rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    86
rm -rf "$SOURCE/$TARGET/share"