--- a/Admin/polyml/README Mon Jan 21 14:44:23 2019 +0000
+++ b/Admin/polyml/README Mon Jan 21 21:28:16 2019 +0100
@@ -1,12 +1,13 @@
Poly/ML for Isabelle
====================
-This compilation of Poly/ML 5.7.1 (http://www.polyml.org) is based on the
-source distribution from https://github.com/polyml/polyml/commits/fixes-5.7.1
-up to commit b3d1ff33a4b4.
+This compilation of Poly/ML (https://www.polyml.org) is based on the
+repository version
+https://github.com/polyml/polyml/commit/0a6ebca445fc (master).
-The Isabelle repository provides the administrative tool "build_polyml",
-which can be used in the polyml component directory as follows.
+The Isabelle repository provides the administrative tool
+"build_polyml", which can be used in the polyml component directory as
+follows.
* Linux:
@@ -38,14 +39,7 @@
$ curl https://gmplib.org/download/gmp/gmp-6.1.2.tar.xz | xz -dc | tar xf -
$ cd gmp-6.1.2
-* build x86-darwin:
-
- $ make distclean
- $ env ABI=32 ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)" --libdir=/usr/local/lib32
- $ make && make check
- $ sudo make install
-
-* build x86_64-darwin:
+* build:
$ make distclean
$ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)"
@@ -54,4 +48,4 @@
Makarius
- 28-Jul-2018
+ 21-Jan-2019
--- a/Admin/polyml/settings Mon Jan 21 14:44:23 2019 +0000
+++ b/Admin/polyml/settings Mon Jan 21 21:28:16 2019 +0100
@@ -2,68 +2,16 @@
POLYML_HOME="$COMPONENT"
-
-# platform preference
+ML_PLATFORM="${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_PLATFORM64}}"
if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
then
- ML_SYSTEM_64="true"
+ ML_OPTIONS="--minheap 1000"
else
- ML_SYSTEM_64="false"
+ ML_PLATFORM="${ML_PLATFORM/x86_64/x86_64_32}"
+ ML_OPTIONS="--minheap 500"
fi
-case "${ISABELLE_PLATFORM_FAMILY}:${ML_SYSTEM_64}" in
- windows:true)
- PLATFORMS="x86_64-windows x86-windows"
- ;;
- windows:*)
- PLATFORMS="x86-windows x86_64-windows"
- ;;
- *:true)
- PLATFORMS="$ISABELLE_PLATFORM64 $ISABELLE_PLATFORM32"
- ;;
- *)
- PLATFORMS="$ISABELLE_PLATFORM32 $ISABELLE_PLATFORM64"
- ;;
-esac
-
-
-# check executable
-
-unset ML_HOME
-
-for PLATFORM in $PLATFORMS
-do
- if [ -z "$ML_HOME" ]
- then
- if "$POLYML_HOME/$PLATFORM/poly" -v </dev/null >/dev/null 2>/dev/null
- then
-
- # ML settings
-
- ML_SYSTEM=polyml-5.7.1
- ML_PLATFORM="$PLATFORM"
- ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_SOURCES="$POLYML_HOME/src"
-
- case "$ML_PLATFORM" in
- x86_64-windows)
- ML_OPTIONS="--minheap 1000 --codepage utf8"
- ;;
- x86-windows)
- ML_OPTIONS="--minheap 500 --codepage utf8"
- ;;
- x86_64-*)
- ML_OPTIONS="--minheap 1000"
- ;;
- *)
- ML_OPTIONS="--minheap 500"
- ;;
- esac
-
- fi
- fi
-done
-
-unset PLATFORM
-unset PLATFORMS
+ML_SYSTEM=polyml-5.7.1
+ML_HOME="$POLYML_HOME/$ML_PLATFORM"
+ML_SOURCES="$POLYML_HOME/src"
--- a/src/Pure/Admin/build_polyml.scala Mon Jan 21 14:44:23 2019 +0000
+++ b/src/Pure/Admin/build_polyml.scala Mon Jan 21 21:28:16 2019 +0100
@@ -7,58 +7,33 @@
package isabelle
+import scala.util.matching.Regex
+
+
object Build_PolyML
{
/** platform-specific build **/
sealed case class Platform_Info(
options: List[String] = Nil,
- options_multilib: List[String] = Nil,
setup: String = "",
- copy_files: List[String] = Nil)
- {
- def platform_options(arch_64: Boolean): List[String] =
- if (!arch_64 && Isabelle_System.getenv("ISABELLE_PLATFORM64") == "x86_64-linux")
- options_multilib
- else options
- }
+ copy_files: List[String] = Nil,
+ ldd_pattern: Option[(String, Regex)] = None)
private val platform_info = Map(
- "x86-linux" ->
- Platform_Info(
- options_multilib =
- List("--build=i386", "CFLAGS=-m32 -O3", "CXXFLAGS=-m32 -O3", "CCASFLAGS=-m32",
- "LDFLAGS=-Wl,-rpath,_DUMMY_", "--without-gmp"),
- options = List("LDFLAGS=-Wl,-rpath,_DUMMY_")),
- "x86_64-linux" ->
+ "linux" ->
Platform_Info(
- options = List("LDFLAGS=-Wl,-rpath,_DUMMY_")),
- "x86-darwin" ->
- Platform_Info(
- options =
- List("--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 -L/usr/local/lib32"),
- setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin"),
- "x86_64-darwin" ->
+ options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"),
+ ldd_pattern = Some(("ldd", """\s*libgmp.*=>\s*(\S+).*""".r))),
+ "darwin" ->
Platform_Info(
options =
List("--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"),
- setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin"),
- "x86-windows" ->
- Platform_Info(
- options =
- List("--host=i686-w32-mingw32", "CPPFLAGS=-I/mingw32/include", "--disable-windows-gui"),
- setup =
- """PATH=/usr/bin:/bin:/mingw32/bin
- export CONFIG_SITE=/etc/config.site""",
- copy_files =
- List("$MSYS/mingw32/bin/libgcc_s_dw2-1.dll",
- "$MSYS/mingw32/bin/libgmp-10.dll",
- "$MSYS/mingw32/bin/libstdc++-6.dll")),
- "x86_64-windows" ->
+ setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin",
+ ldd_pattern = Some(("otool -L", """\s*(\S+lib(?:polyml|gmp).*dylib).*""".r))),
+ "windows" ->
Platform_Info(
options =
List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"),
@@ -81,13 +56,16 @@
if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir))
error("Bad Poly/ML root directory: " + root)
- val platform =
- (if (arch_64) "x86_64" else "x86") +
- (if (Platform.is_windows) "-windows" else if (Platform.is_macos) "-darwin" else "-linux")
+ val platform_arch = if (arch_64) "x86_64" else "x86_64_32"
+ val platform_os =
+ if (Platform.is_windows) "windows" else if (Platform.is_macos) "darwin" else "linux"
+
+ val platform = platform_arch + "-" + platform_os
+ val platform_64 = "x86_64-" + platform_os
val info =
- platform_info.get(platform) getOrElse
- error("Bad platform identifier: " + quote(platform))
+ platform_info.get(platform_os) getOrElse
+ error("Bad OS platform: " + quote(platform_os))
val settings =
msys_root match {
@@ -117,7 +95,7 @@
val configure_options =
List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") :::
- info.platform_options(arch_64) ::: options
+ info.options ::: options ::: (if (arch_64) Nil else List("--enable-compact32bit"))
bash(root,
info.setup + "\n" +
@@ -132,11 +110,7 @@
val ldd_files =
{
- val ldd_pattern =
- if (Platform.is_linux) Some(("ldd", """\s*libgmp.*=>\s*(\S+).*""".r))
- else if (Platform.is_macos) Some(("otool -L", """\s*(\S+lib(?:polyml|gmp).*dylib).*""".r))
- else None
- ldd_pattern match {
+ info.ldd_pattern match {
case Some((ldd, pattern)) =>
val lines = bash(root, ldd + " target/bin/poly").check.out_lines
for { line <- lines; List(lib) <- pattern.unapplySeq(line) } yield lib
@@ -150,9 +124,9 @@
val sha1_files =
if (sha1_root.isDefined) {
val dir1 = sha1_root.get
- bash(dir1, "./build " + platform, redirect = true, echo = true).check
+ bash(dir1, "./build " + platform_64, redirect = true, echo = true).check
- val dir2 = dir1 + Path.explode(platform)
+ val dir2 = dir1 + Path.explode(platform_64)
File.read_dir(dir2).map(entry => dir2.implode + "/" + entry)
}
else Nil
@@ -248,7 +222,7 @@
Options are:
-M DIR msys root directory (for Windows)
- -m ARCH processor architecture (32=x86, 64=x86_64, default: x86)
+ -m ARCH processor architecture (32=x86_64_32, 64=x86_64, default: 32)
-s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1
Build Poly/ML in the ROOT directory of its sources, with additional
@@ -257,7 +231,7 @@
"M:" -> (arg => msys_root = Some(Path.explode(arg))),
"m:" ->
{
- case "32" | "x86" => arch_64 = false
+ case "32" | "x86_64_32" => arch_64 = false
case "64" | "x86_64" => arch_64 = true
case bad => error("Bad processor architecture: " + quote(bad))
},
--- a/src/Pure/Admin/components.scala Mon Jan 21 14:44:23 2019 +0000
+++ b/src/Pure/Admin/components.scala Mon Jan 21 21:28:16 2019 +0100
@@ -73,7 +73,8 @@
def purge(dir: Path, platform: Platform.Family.Value)
{
def purge_platforms(platforms: String*): Set[String] =
- platforms.flatMap(name => List("x86-" + name, "x86_64-" + name)).toSet + "ppc-darwin"
+ platforms.flatMap(name => List("x86-" + name, "x86_64_32-" + name, "x86_64-" + name)).toSet +
+ "ppc-darwin"
val purge_set =
platform match {
case Platform.Family.linux => purge_platforms("darwin", "cygwin", "windows")
--- a/src/Pure/ML/ml_process.scala Mon Jan 21 14:44:23 2019 +0000
+++ b/src/Pure/ML/ml_process.scala Mon Jan 21 21:28:16 2019 +0100
@@ -129,8 +129,13 @@
val ml_runtime_options =
{
val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS"))
- if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
- else ml_options ::: List("--gcthreads", options.int("threads").toString)
+ val ml_options1 =
+ if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options
+ else ml_options ::: List("--gcthreads", options.int("threads").toString)
+ val ml_options2 =
+ if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1
+ else ml_options1 ::: List("--codepage", "utf8")
+ ml_options2
}
// bash
--- a/src/Pure/ML/ml_system.ML Mon Jan 21 14:44:23 2019 +0000
+++ b/src/Pure/ML/ml_system.ML Mon Jan 21 21:28:16 2019 +0100
@@ -9,6 +9,7 @@
val name: string
val platform: string
val platform_is_windows: bool
+ val platform_is_64: bool
val platform_path: string -> string
val standard_path: string -> string
end;
@@ -19,6 +20,7 @@
val SOME name = OS.Process.getEnv "ML_SYSTEM";
val SOME platform = OS.Process.getEnv "ML_PLATFORM";
val platform_is_windows = String.isSuffix "windows" platform;
+val platform_is_64 = String.isPrefix "x86_64-" platform;
val platform_path =
if platform_is_windows then