--- a/Admin/components/components.sha1 Thu Dec 08 17:22:51 2016 +0100
+++ b/Admin/components/components.sha1 Sat Dec 10 15:45:16 2016 +0100
@@ -138,6 +138,7 @@
5b70c12c95a90d858f90c1945011289944ea8e17 polyml-5.6-20160118.tar.gz
5b19dc93082803b82aa553a5cfb3e914606c0ffd polyml-5.6.tar.gz
853ab0e9ff2b73790cc80a2d36cbff8b03e50a8e polyml-test-7a7b742897e9.tar.gz
+c629cd499a724bbe37b962f727e4ff340c50299d polyml-test-8529546198aa.tar.gz
8ee375cfc38972f080dbc78f07b68dac03efe968 ProofGeneral-3.7.1.1.tar.gz
847b52c0676b5eb0fbf0476f64fc08c2d72afd0c ProofGeneral-4.1.tar.gz
8e0b2b432755ef11d964e20637d1bc567d1c0477 ProofGeneral-4.2-1.tar.gz
--- a/Admin/polyml/README Thu Dec 08 17:22:51 2016 +0100
+++ b/Admin/polyml/README Sat Dec 10 15:45:16 2016 +0100
@@ -1,32 +1,27 @@
Poly/ML for Isabelle
====================
-This compilation of Poly/ML 5.6 (http://www.polyml.org) is based on the source
-distribution from https://github.com/polyml/polyml/releases/tag/v5.6/.
+This compilation of Poly/ML (http://www.polyml.org) is based on the repository
+version https://github.com/polyml/polyml/commit/8529546198aa
-On Linux the sources have changed as follows, in order to evade a
-potential conflict of /bin/bash versus /bin/sh -> dash (notably on
-Ubuntu and Debian):
+The Isabelle repository provides the administrative tool "build_polyml", which
+can be used in the polyml component directory as follows.
-diff -r src-orig/libpolyml/process_env.cpp src/libpolyml/process_env.cpp
-228c228
-< execve("/bin/sh", argv, environ);
----
-> execvp("bash", argv);
+* Linux:
+ isabelle build_polyml -m32 -s sha1 src --with-gmp
+ isabelle build_polyml -m64 -s sha1 src --with-gmp
-The included build script is used like this:
+* Mac OS X:
- ./build src x86-linux --with-gmp
- ./build src x86_64-linux --with-gmp
- ./build src x86-darwin --without-gmp
- ./build src x86_64-darwin --without-gmp
- ./build src x86-windows --with-gmp
- ./build src x86_64-windows --with-gmp
+ isabelle build_polyml -m32 -s sha1 src --without-gmp
+ isabelle build_polyml -m64 -s sha1 src --without-gmp
-Also note that the separate "sha1" library module is required for
-efficient digestion of strings according to SHA-1.
+* Windows (Cygwin shell)
+
+ isabelle build_polyml -M /cygdrive/c/msys64 -m32 -s sha1 src --with-gmp
+ isabelle build_polyml -M /cygdrive/c/msys64 -m64 -s sha1 src --with-gmp
Makarius
- 11-Feb-2016
+ 10-Dec-2016
--- a/Admin/polyml/build Thu Dec 08 17:22:51 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-#!/usr/bin/env bash
-#
-# Multi-platform build script for Poly/ML
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-PRG="$(basename "$0")"
-
-
-# diagnostics
-
-function usage()
-{
- echo
- echo "Usage: $PRG SOURCE TARGET [OPTIONS]"
- echo
- echo " Build Poly/ML in SOURCE directory for given platform in TARGET,"
- echo " using the usual Isabelle platform identifiers."
- echo
- echo " Additional options for ./configure may be given, e.g. --with-gmp"
- echo
- exit 1
-}
-
-function fail()
-{
- echo "$1" >&2
- exit 2
-}
-
-
-# command line args
-
-[ "$#" -eq 0 ] && usage
-SOURCE="$1"; shift
-
-[ "$#" -eq 0 ] && usage
-TARGET="$1"; shift
-
-USER_OPTIONS=("$@")
-
-
-# main
-
-[ -d "$SOURCE" ] || fail "Bad source directory: \"$SOURCE\""
-
-case "$TARGET" in
- x86-linux)
- OPTIONS=()
- ;;
- x86_64-linux)
- OPTIONS=()
- ;;
- x86-darwin)
- OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3 -I../libffi/include'
- CXXFLAGS='-arch i686 -O3 -I../libffi/include' CCASFLAGS='-arch i686 -O3'
- LDFLAGS='-segprot POLY rwx rwx')
- ;;
- x86_64-darwin)
- OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3 -I../libffi/include'
- CXXFLAGS='-arch x86_64 -O3 -I../libffi/include' CCASFLAGS='-arch x86_64'
- LDFLAGS='-segprot POLY rwx rwx')
- ;;
- x86-cygwin)
- OPTIONS=()
- ;;
- x86-windows)
- OPTIONS=(--host=i686-w32-mingw32 CPPFLAGS='-I/mingw32/include' --disable-windows-gui)
- PATH="/mingw32/bin:$PATH"
- ;;
- x86_64-windows)
- OPTIONS=(--host=x86_64-w64-mingw32 CPPFLAGS='-I/mingw64/include' --disable-windows-gui)
- PATH="/mingw64/bin:$PATH"
- ;;
- *)
- fail "Bad platform identifier: \"$TARGET\""
- ;;
-esac
-
-(
- cd "$SOURCE"
- make distclean
-
- { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" --enable-intinf-as-int "${USER_OPTIONS[@]}" && \
- make compiler && \
- make compiler && \
- make install; } || fail "Build failed"
-)
-
-mkdir -p "$TARGET"
-for X in "$TARGET"/*
-do
- [ -d "$X" ] && rm -rf "$X"
-done
-rm -rf "$TARGET/polyml"
-cp -a "$THIS/polyi" "$TARGET/"
-mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
-mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
-rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
-rm -rf "$SOURCE/$TARGET/share"
-
-case "$TARGET" in
- x86-cygwin)
- peflags -x8192000 -z500 "$TARGET/poly.exe"
- ;;
- x86-windows)
- for X in libgcc_s_dw2-1.dll libgmp-10.dll libstdc++-6.dll
- do
- cp "/mingw32/bin/$X" "$TARGET/."
- done
- ;;
- x86_64-windows)
- for X in libgcc_s_seh-1.dll libgmp-10.dll libstdc++-6.dll
- do
- cp "/mingw64/bin/$X" "$TARGET/."
- done
- ;;
-esac
--- a/Admin/polyml/settings Thu Dec 08 17:22:51 2016 +0100
+++ b/Admin/polyml/settings Sat Dec 10 15:45:16 2016 +0100
@@ -36,12 +36,12 @@
do
if [ -z "$ML_HOME" ]
then
- if "$POLYML_HOME/$PLATFORM/polyml" -v </dev/null >/dev/null 2>/dev/null
+ if "$POLYML_HOME/$PLATFORM/polyi" -v </dev/null >/dev/null 2>/dev/null
then
# ML settings
- ML_SYSTEM=polyml-5.6
+ ML_SYSTEM=polyml-5.7
ML_PLATFORM="$PLATFORM"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_SOURCES="$POLYML_HOME/src"
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Dec 08 17:22:51 2016 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sat Dec 10 15:45:16 2016 +0100
@@ -97,7 +97,7 @@
private val remote_builds =
List(
List(Remote_Build("lxbroy8",
- options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-test-7a7b742897e9'",
+ options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-test-8529546198aa'",
args = "-N -g timing")),
List(Remote_Build("lxbroy9", options = "-m32 -B -M1x2,2", args = "-N -g timing")),
List(Remote_Build("lxbroy10", options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),