updated Poly/ML repository test version (08-Dec-2016);
authorwenzelm
Sat Dec 10 15:45:16 2016 +0100 (21 months ago)
changeset 64544d23b7c9b9dd4
parent 64543 6b13586ef1a2
child 64545 25045094d7bb
updated Poly/ML repository test version (08-Dec-2016);
Admin/components/components.sha1
Admin/polyml/README
Admin/polyml/build
Admin/polyml/settings
src/Pure/Admin/isabelle_cronjob.scala
     1.1 --- a/Admin/components/components.sha1	Thu Dec 08 17:22:51 2016 +0100
     1.2 +++ b/Admin/components/components.sha1	Sat Dec 10 15:45:16 2016 +0100
     1.3 @@ -138,6 +138,7 @@
     1.4  5b70c12c95a90d858f90c1945011289944ea8e17  polyml-5.6-20160118.tar.gz
     1.5  5b19dc93082803b82aa553a5cfb3e914606c0ffd  polyml-5.6.tar.gz
     1.6  853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e  polyml-test-7a7b742897e9.tar.gz
     1.7 +c629cd499a724bbe37b962f727e4ff340c50299d  polyml-test-8529546198aa.tar.gz
     1.8  8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
     1.9  847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
    1.10  8e0b2b432755ef11d964e20637d1bc567d1c0477  ProofGeneral-4.2-1.tar.gz
     2.1 --- a/Admin/polyml/README	Thu Dec 08 17:22:51 2016 +0100
     2.2 +++ b/Admin/polyml/README	Sat Dec 10 15:45:16 2016 +0100
     2.3 @@ -1,32 +1,27 @@
     2.4  Poly/ML for Isabelle
     2.5  ====================
     2.6  
     2.7 -This compilation of Poly/ML 5.6 (http://www.polyml.org) is based on the source
     2.8 -distribution from https://github.com/polyml/polyml/releases/tag/v5.6/.
     2.9 +This compilation of Poly/ML (http://www.polyml.org) is based on the repository
    2.10 +version https://github.com/polyml/polyml/commit/8529546198aa
    2.11  
    2.12 -On Linux the sources have changed as follows, in order to evade a
    2.13 -potential conflict of /bin/bash versus /bin/sh -> dash (notably on
    2.14 -Ubuntu and Debian):
    2.15 +The Isabelle repository provides the administrative tool "build_polyml", which
    2.16 +can be used in the polyml component directory as follows.
    2.17  
    2.18 -diff -r src-orig/libpolyml/process_env.cpp src/libpolyml/process_env.cpp
    2.19 -228c228
    2.20 -<                 execve("/bin/sh", argv, environ);
    2.21 ----
    2.22 ->                 execvp("bash", argv);
    2.23 +* Linux:
    2.24  
    2.25 +  isabelle build_polyml -m32 -s sha1 src --with-gmp
    2.26 +  isabelle build_polyml -m64 -s sha1 src --with-gmp
    2.27  
    2.28 -The included build script is used like this:
    2.29 +* Mac OS X:
    2.30  
    2.31 -  ./build src x86-linux --with-gmp
    2.32 -  ./build src x86_64-linux --with-gmp
    2.33 -  ./build src x86-darwin --without-gmp
    2.34 -  ./build src x86_64-darwin --without-gmp
    2.35 -  ./build src x86-windows --with-gmp
    2.36 -  ./build src x86_64-windows --with-gmp
    2.37 +  isabelle build_polyml -m32 -s sha1 src --without-gmp
    2.38 +  isabelle build_polyml -m64 -s sha1 src --without-gmp
    2.39  
    2.40 -Also note that the separate "sha1" library module is required for
    2.41 -efficient digestion of strings according to SHA-1.
    2.42 +* Windows (Cygwin shell)
    2.43 +
    2.44 +  isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src --with-gmp
    2.45 +  isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src --with-gmp
    2.46  
    2.47  
    2.48          Makarius
    2.49 -        11-Feb-2016
    2.50 +        10-Dec-2016
     3.1 --- a/Admin/polyml/build	Thu Dec 08 17:22:51 2016 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,117 +0,0 @@
     3.4 -#!/usr/bin/env bash
     3.5 -#
     3.6 -# Multi-platform build script for Poly/ML
     3.7 -
     3.8 -THIS="$(cd "$(dirname "$0")"; pwd)"
     3.9 -PRG="$(basename "$0")"
    3.10 -
    3.11 -
    3.12 -# diagnostics
    3.13 -
    3.14 -function usage()
    3.15 -{
    3.16 -  echo
    3.17 -  echo "Usage: $PRG SOURCE TARGET [OPTIONS]"
    3.18 -  echo
    3.19 -  echo "  Build Poly/ML in SOURCE directory for given platform in TARGET,"
    3.20 -  echo "  using the usual Isabelle platform identifiers."
    3.21 -  echo
    3.22 -  echo "  Additional options for ./configure may be given, e.g. --with-gmp"
    3.23 -  echo
    3.24 -  exit 1
    3.25 -}
    3.26 -
    3.27 -function fail()
    3.28 -{
    3.29 -  echo "$1" >&2
    3.30 -  exit 2
    3.31 -}
    3.32 -
    3.33 -
    3.34 -# command line args
    3.35 -
    3.36 -[ "$#" -eq 0 ] && usage
    3.37 -SOURCE="$1"; shift
    3.38 -
    3.39 -[ "$#" -eq 0 ] && usage
    3.40 -TARGET="$1"; shift
    3.41 -
    3.42 -USER_OPTIONS=("$@")
    3.43 -
    3.44 -
    3.45 -# main
    3.46 -
    3.47 -[ -d "$SOURCE" ] || fail "Bad source directory: \"$SOURCE\""
    3.48 -
    3.49 -case "$TARGET" in
    3.50 -  x86-linux)
    3.51 -    OPTIONS=()
    3.52 -    ;;
    3.53 -  x86_64-linux)
    3.54 -    OPTIONS=()
    3.55 -    ;;
    3.56 -  x86-darwin)
    3.57 -    OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3 -I../libffi/include'
    3.58 -      CXXFLAGS='-arch i686 -O3 -I../libffi/include' CCASFLAGS='-arch i686 -O3'
    3.59 -      LDFLAGS='-segprot POLY rwx rwx')
    3.60 -    ;;
    3.61 -  x86_64-darwin)
    3.62 -   OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3 -I../libffi/include'
    3.63 -     CXXFLAGS='-arch x86_64 -O3 -I../libffi/include' CCASFLAGS='-arch x86_64'
    3.64 -     LDFLAGS='-segprot POLY rwx rwx')
    3.65 -    ;;
    3.66 -  x86-cygwin)
    3.67 -    OPTIONS=()
    3.68 -    ;;
    3.69 -  x86-windows)
    3.70 -    OPTIONS=(--host=i686-w32-mingw32 CPPFLAGS='-I/mingw32/include' --disable-windows-gui)
    3.71 -    PATH="/mingw32/bin:$PATH"
    3.72 -    ;;
    3.73 -  x86_64-windows)
    3.74 -    OPTIONS=(--host=x86_64-w64-mingw32 CPPFLAGS='-I/mingw64/include' --disable-windows-gui)
    3.75 -    PATH="/mingw64/bin:$PATH"
    3.76 -    ;;
    3.77 -  *)
    3.78 -    fail "Bad platform identifier: \"$TARGET\""
    3.79 -    ;;
    3.80 -esac
    3.81 -
    3.82 -(
    3.83 -  cd "$SOURCE"
    3.84 -  make distclean
    3.85 -
    3.86 -  { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" --enable-intinf-as-int "${USER_OPTIONS[@]}" && \
    3.87 -    make compiler && \
    3.88 -    make compiler && \
    3.89 -    make install; } || fail "Build failed"
    3.90 -)
    3.91 -
    3.92 -mkdir -p "$TARGET"
    3.93 -for X in "$TARGET"/*
    3.94 -do
    3.95 -  [ -d "$X" ] && rm -rf "$X"
    3.96 -done
    3.97 -rm -rf "$TARGET/polyml"
    3.98 -cp -a "$THIS/polyi" "$TARGET/"
    3.99 -mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
   3.100 -mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
   3.101 -rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
   3.102 -rm -rf "$SOURCE/$TARGET/share"
   3.103 -
   3.104 -case "$TARGET" in
   3.105 -  x86-cygwin)
   3.106 -    peflags -x8192000 -z500 "$TARGET/poly.exe"
   3.107 -    ;;
   3.108 -  x86-windows)
   3.109 -    for X in libgcc_s_dw2-1.dll libgmp-10.dll libstdc++-6.dll
   3.110 -    do
   3.111 -      cp "/mingw32/bin/$X" "$TARGET/."
   3.112 -    done
   3.113 -    ;;
   3.114 -  x86_64-windows)
   3.115 -    for X in libgcc_s_seh-1.dll libgmp-10.dll libstdc++-6.dll
   3.116 -    do
   3.117 -      cp "/mingw64/bin/$X" "$TARGET/."
   3.118 -    done
   3.119 -    ;;
   3.120 -esac
     4.1 --- a/Admin/polyml/settings	Thu Dec 08 17:22:51 2016 +0100
     4.2 +++ b/Admin/polyml/settings	Sat Dec 10 15:45:16 2016 +0100
     4.3 @@ -36,12 +36,12 @@
     4.4  do
     4.5    if [ -z "$ML_HOME" ]
     4.6    then
     4.7 -    if "$POLYML_HOME/$PLATFORM/polyml" -v </dev/null >/dev/null 2>/dev/null
     4.8 +    if "$POLYML_HOME/$PLATFORM/polyi" -v </dev/null >/dev/null 2>/dev/null
     4.9      then
    4.10  
    4.11        # ML settings
    4.12  
    4.13 -      ML_SYSTEM=polyml-5.6
    4.14 +      ML_SYSTEM=polyml-5.7
    4.15        ML_PLATFORM="$PLATFORM"
    4.16        ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    4.17        ML_SOURCES="$POLYML_HOME/src"
     5.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Dec 08 17:22:51 2016 +0100
     5.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Dec 10 15:45:16 2016 +0100
     5.3 @@ -97,7 +97,7 @@
     5.4    private val remote_builds =
     5.5      List(
     5.6        List(Remote_Build("lxbroy8",
     5.7 -        options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-test-7a7b742897e9'",
     5.8 +        options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-test-8529546198aa'",
     5.9          args = "-N -g timing")),
    5.10        List(Remote_Build("lxbroy9", options = "-m32 -B -M1x2,2", args = "-N -g timing")),
    5.11        List(Remote_Build("lxbroy10", options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),