--- a/Admin/polyml/INSTALL-MinGW Mon Aug 31 21:28:08 2015 +0200
+++ b/Admin/polyml/INSTALL-MinGW Mon Aug 31 22:28:23 2015 +0200
@@ -12,6 +12,7 @@
mingw-w64-install.exe
i686-4.9.3-win32-dwarf-rt_v4-rev0
+ x86_64-4.9.3-win32-seh-rt_v4-rev0
target c:\msys32 or c:\msys64
@@ -22,8 +23,9 @@
after restart of msys shell:
pacman -Su
- pacman -S make diffutils texinfo gmp-devel mingw-w64-i686-gmp
+ pacman -S make diffutils texinfo gmp-devel mingw-w64-i686-gmp mingw-w64-x86_64-gmp
- build (as regular user) e.g. on vmbroy9
isabelle/repos/Admin/polyml/build polyml-git x86-windows --build=i686-pc-msys --with-gmp
+ isabelle/repos/Admin/polyml/build polyml-git x86_64-windows --build=x86_64-pc-msys --with-gmp
--- a/Admin/polyml/README Mon Aug 31 21:28:08 2015 +0200
+++ b/Admin/polyml/README Mon Aug 31 22:28:23 2015 +0200
@@ -2,7 +2,7 @@
====================
This is a preview of Poly/ML 5.5.3, based on
-https://github.com/polyml/polyml/commit/3fbfb80c471f
+https://github.com/polyml/polyml/
The included build script is used like this:
@@ -11,10 +11,11 @@
./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
Also note that the separate "sha1" library module is required for
efficient digesting of strings according to SHA-1.
Makarius
- 20-Aug-2015
+ 31-Aug-2015
--- a/Admin/polyml/build Mon Aug 31 21:28:08 2015 +0200
+++ b/Admin/polyml/build Mon Aug 31 22:28:23 2015 +0200
@@ -64,11 +64,12 @@
OPTIONS=()
;;
x86-windows)
- OPTIONS=(--host=i686-w32-mingw32 CPPFLAGS='-I/mingw32/include') # --build=i686-pc-msys --with-gmp
+ OPTIONS=(--host=i686-w32-mingw32 CPPFLAGS='-I/mingw32/include')
PATH="/mingw32/bin:$PATH"
;;
x86_64-windows)
- OPTIONS=()
+ OPTIONS=(--host=x86_64-w64-mingw32 CPPFLAGS='-I/mingw64/include')
+ PATH="/mingw64/bin:$PATH"
;;
*)
fail "Bad platform identifier: \"$TARGET\""
@@ -101,4 +102,10 @@
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