# HG changeset patch # User wenzelm # Date 1548097400 -3600 # Node ID 3fb94d9b87b0f8fbb2c8040fb49dd0541cfda042 # Parent 1e30b4093924509b946e6f912ce32a4ebf940558 updated polyml platform: 32=x86_64_32; diff -r 1e30b4093924 -r 3fb94d9b87b0 Admin/polyml/README --- a/Admin/polyml/README Mon Jan 21 19:59:37 2019 +0100 +++ b/Admin/polyml/README Mon Jan 21 20:03:20 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 1e30b4093924 -r 3fb94d9b87b0 Admin/polyml/settings --- a/Admin/polyml/settings Mon Jan 21 19:59:37 2019 +0100 +++ b/Admin/polyml/settings Mon Jan 21 20:03:20 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 1e30b4093924 -r 3fb94d9b87b0 src/Pure/Admin/build_polyml.scala --- a/src/Pure/Admin/build_polyml.scala Mon Jan 21 19:59:37 2019 +0100 +++ b/src/Pure/Admin/build_polyml.scala Mon Jan 21 20:03:20 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)) },