Admin/polyml/build
author wenzelm
Sun, 20 Jan 2013 13:59:13 +0100
changeset 50990 11996ea98bbe
parent 47763 15936c7b2fa3
child 51042 f024975be336
permissions -rwxr-xr-x
tuned;
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)
46875
162b0c46c559 updated polyml/build option to prefer included libffi;
wenzelm
parents: 39620
diff changeset
    54
    OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3 -I../libffi/include'
162b0c46c559 updated polyml/build option to prefer included libffi;
wenzelm
parents: 39620
diff changeset
    55
      CXXFLAGS='-arch i686 -O3 -I../libffi/include' CCASFLAGS='-arch i686 -O3'
38585
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)
46875
162b0c46c559 updated polyml/build option to prefer included libffi;
wenzelm
parents: 39620
diff changeset
    59
   OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3 -I../libffi/include'
162b0c46c559 updated polyml/build option to prefer included libffi;
wenzelm
parents: 39620
diff changeset
    60
     CXXFLAGS='-arch x86_64 -O3 -I../libffi/include' CCASFLAGS='-arch x86_64'
162b0c46c559 updated polyml/build option to prefer included libffi;
wenzelm
parents: 39620
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
    ;;
47763
15936c7b2fa3 mingw is windows (still inactive);
wenzelm
parents: 47458
diff changeset
    66
  x86-windows)
15936c7b2fa3 mingw is windows (still inactive);
wenzelm
parents: 47458
diff changeset
    67
    OPTIONS=()
15936c7b2fa3 mingw is windows (still inactive);
wenzelm
parents: 47458
diff changeset
    68
    ;;
15936c7b2fa3 mingw is windows (still inactive);
wenzelm
parents: 47458
diff changeset
    69
  x86_64-windows)
47458
29b3f9cba73d minimal support for x86-mingw;
wenzelm
parents: 46875
diff changeset
    70
    OPTIONS=()
29b3f9cba73d minimal support for x86-mingw;
wenzelm
parents: 46875
diff changeset
    71
    ;;
38472
3c5716b2e7b6 pro-forma support for further platforms;
wenzelm
parents: 38468
diff changeset
    72
  ppc-darwin | sparc-solaris | x86-solaris | x86-bsd)
3c5716b2e7b6 pro-forma support for further platforms;
wenzelm
parents: 38468
diff changeset
    73
    OPTIONS=()
3c5716b2e7b6 pro-forma support for further platforms;
wenzelm
parents: 38468
diff changeset
    74
    ;;
38468
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    75
  *)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    76
    fail "Bad platform identifier: \"$TARGET\""
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
esac
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    79
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
  cd "$SOURCE"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    82
  make distclean
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
  { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    85
    make compiler && \
39620
ff694044a55b make compiler doubly sure;
wenzelm
parents: 38585
diff changeset
    86
    make compiler && \
38468
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    87
    make install; } || fail "Build failed"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    88
)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    89
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    90
mkdir -p "$TARGET"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    91
mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    92
mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    93
rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    94
rm -rf "$SOURCE/$TARGET/share"