# HG changeset patch # User wenzelm # Date 1548102496 -3600 # Node ID c9ea1e9916fb7ddd924855f7cc81ceb4b75f9534 # Parent 7a92cbec7030fba1fb9bd4c6df193c5dde216a83# Parent 3fb94d9b87b0f8fbb2c8040fb49dd0541cfda042 merged diff -r 7a92cbec7030 -r c9ea1e9916fb Admin/polyml/README --- 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 diff -r 7a92cbec7030 -r c9ea1e9916fb Admin/polyml/settings --- 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 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" diff -r 7a92cbec7030 -r c9ea1e9916fb src/Pure/Admin/build_polyml.scala --- 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)) }, diff -r 7a92cbec7030 -r c9ea1e9916fb src/Pure/Admin/components.scala --- 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") diff -r 7a92cbec7030 -r c9ea1e9916fb src/Pure/ML/ml_process.scala --- 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 diff -r 7a92cbec7030 -r c9ea1e9916fb src/Pure/ML/ml_system.ML --- 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