Admin/polyml/build
author blanchet
Mon, 19 May 2014 23:43:53 +0200
changeset 57005 33f3d2ea803d
parent 56958 b2c2f74d1c93
child 60960 1fd5db0e2b34
permissions -rwxr-xr-x
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
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
    ;;
38468
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
    fail "Bad platform identifier: \"$TARGET\""
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
esac
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
(
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    78
  cd "$SOURCE"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    79
  make distclean
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
  { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    82
    make compiler && \
39620
ff694044a55b make compiler doubly sure;
wenzelm
parents: 38585
diff changeset
    83
    make compiler && \
38468
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    84
    make install; } || fail "Build failed"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    85
)
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    86
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    87
mkdir -p "$TARGET"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    88
mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    89
mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    90
rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
01d70ada9284 multi-platform build script for Poly/ML;
wenzelm
parents:
diff changeset
    91
rm -rf "$SOURCE/$TARGET/share"
51042
f024975be336 better apply peflags at build time, to avoid antivirus getting nervous about changing executables;
wenzelm
parents: 47763
diff changeset
    92
f024975be336 better apply peflags at build time, to avoid antivirus getting nervous about changing executables;
wenzelm
parents: 47763
diff changeset
    93
if [ "$TARGET" = x86-cygwin ]; then
f024975be336 better apply peflags at build time, to avoid antivirus getting nervous about changing executables;
wenzelm
parents: 47763
diff changeset
    94
  peflags -x8192000 -z500 "$TARGET/poly.exe"
f024975be336 better apply peflags at build time, to avoid antivirus getting nervous about changing executables;
wenzelm
parents: 47763
diff changeset
    95
fi