# HG changeset patch # User wenzelm # Date 1744205487 -7200 # Node ID 3125fd1ee69c03fbc277a721576514a98c7d1861 # Parent 5a0d1075911cdf330a0a47af37cac09c16c27df3 added option -G to build GMP library from sources; diff -r 5a0d1075911c -r 3125fd1ee69c src/Pure/Admin/component_polyml.scala --- a/src/Pure/Admin/component_polyml.scala Mon Apr 07 12:36:56 2025 +0200 +++ b/src/Pure/Admin/component_polyml.scala Wed Apr 09 15:31:27 2025 +0200 @@ -34,6 +34,22 @@ setup = MinGW.environment_export, libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread"))) + def bash( + cwd: Path, + platform: Isabelle_Platform, + mingw: MinGW, + script: String, + redirect: Boolean = false, + progress: Progress = new Progress + ): Process_Result = { + val script1 = + if (platform.is_arm && platform.is_macos) { + "arch -arch arm64 bash -c " + Bash.string(script) + } + else mingw.bash_script(script) + progress.bash(script1, cwd = cwd, redirect = redirect, echo = progress.verbose) + } + def polyml_platform(arch_64: Boolean): String = { val platform = Isabelle_Platform.self (if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name @@ -41,6 +57,7 @@ def make_polyml( root: Path, + gmp_root: Option[Path] = None, sha1_root: Option[Path] = None, target_dir: Path = Path.current, arch_64: Boolean = false, @@ -62,29 +79,29 @@ if (platform.is_linux) Isabelle_System.require_command("patchelf") - /* bash */ + /* configure and make */ + + val configure_options = { + val options1 = if (gmp_root.nonEmpty) List("--with-gmp") else List("--without-gmp") - def bash( - cwd: Path, script: String, - redirect: Boolean = false, - echo: Boolean = false - ): Process_Result = { - val script1 = - if (platform.is_arm && platform.is_macos) { - "arch -arch arm64 bash -c " + Bash.string(script) + val options2 = + for (opt <- info.options) yield { + if (opt.startsWith("CFLAGS=") && gmp_root.nonEmpty) { + val root0 = gmp_root.get.absolute + val root1 = mingw.standard_path(root0) + require(root0.implode == File.bash_path(root0), "Bad directory name " + root0) + opt + " " + "-I" + root1 + "/include -L" + root1 + "/lib" + } + else opt } - else mingw.bash_script(script) - progress.bash(script1, cwd = cwd, redirect = redirect, echo = echo) + + val options3 = if (arch_64) Nil else List("--enable-compact32bit") + + List("--disable-shared", "--enable-intinf-as-int") ::: + options1 ::: options2 ::: options ::: options3 } - - /* configure and make */ - - val configure_options = - List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") ::: - info.options ::: options ::: (if (arch_64) Nil else List("--enable-compact32bit")) - - bash(root, + bash(root, platform, mingw, info.setup + "\n" + """ [ -f Makefile ] && make distclean @@ -93,7 +110,7 @@ rm -rf target make && make install } || { echo "Build failed" >&2; exit 2; } - """, redirect = true, echo = true).check + """, redirect = true, progress = progress).check /* sha1 library */ @@ -101,7 +118,8 @@ val sha1_files = if (sha1_root.isDefined) { val dir1 = sha1_root.get - bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check + bash(dir1, platform, mingw, "./build " + sha1_platform, redirect = true, + progress = progress).check val dir2 = dir1 + Path.explode(sha1_platform) File.read_dir(dir2).map(entry => dir2 + Path.basic(entry)) @@ -152,6 +170,8 @@ /** skeleton for component **/ + val standard_gmp_url = "https://gmplib.org/download/gmp/gmp-6.3.0.tar.bz2" + val default_polyml_url = "https://github.com/polyml/polyml/archive" val default_polyml_version = "90c0dbb2514e" val default_polyml_name = "polyml-5.9.1" @@ -181,6 +201,7 @@ options: List[String] = Nil, mingw: MinGW = MinGW.none, component_name: String = "", + gmp_url: String = "", polyml_url: String = default_polyml_url, polyml_version: String = default_polyml_version, polyml_name: String = default_polyml_name, @@ -189,6 +210,9 @@ target_dir: Path = Path.current, progress: Progress = new Progress ): Unit = { + val platform = Isabelle_Platform.self + + /* component */ val component_name1 = if (component_name.isEmpty) "polyml-" + polyml_version else component_name @@ -199,6 +223,43 @@ /* download and build */ Isabelle_System.with_tmp_dir("download") { download_dir => + /* GMP library */ + + val gmp_root: Option[Path] = + if (gmp_url.isEmpty) None + else { + val gmp_dir = Isabelle_System.make_directory(download_dir + Path.basic("gmp")) + + val archive_name = + Url.get_base_name(gmp_url).getOrElse(error("No base name in " + quote(gmp_url))) + val archive = download_dir + Path.basic(archive_name) + Isabelle_System.download_file(gmp_url, archive, progress = progress) + Isabelle_System.extract(archive, gmp_dir, strip = true) + + val platform_arch = if (platform.is_arm) "aarch64" else "x86_64" + val platform_os = + if (platform.is_linux) "unknown-linux-gnu" + else if (platform.is_windows) "w64-mingw32" + else if (platform.is_macos) """apple-darwin"$(uname -r)"""" + else error("Bad platform " + platform) + + progress.echo("Building GMP library ...") + bash(gmp_dir, platform, mingw, progress = progress, + script = Library.make_lines( + "set -e", + "./configure --enable-cxx --build=" + platform_arch + "-" + platform_os + + """ --prefix="$PWD/target"""", + "make", + "make check", + "make install" + )).check + + Some(gmp_dir + Path.explode("target")) + } + + + /* Poly/ML */ + val List(polyml_download, sha1_download) = for { (url, version, target) <- @@ -220,6 +281,7 @@ progress.echo("Building " + polyml_platform(arch_64)) make_polyml( root = polyml_download, + gmp_root = gmp_root, sha1_root = Some(sha1_download), target_dir = component_dir.path, arch_64 = arch_64, @@ -290,39 +352,11 @@ * Linux and macOS - $ isabelle component_polyml + $ isabelle component_polyml -G: * Windows (Cygwin shell) - $ isabelle component_polyml -M /cygdrive/c/msys64 - - -Building libgmp on macOS -======================== - -The build_polyml invocations above implicitly use the GNU Multiple Precision -Arithmetic Library (libgmp), but that is not available on macOS by default. -Appending "--without-gmp" to the command-line omits this library. Building -libgmp properly from sources works as follows (library headers and binaries -will be placed in /usr/local). - -* Download: - - $ curl https://gmplib.org/download/gmp/gmp-6.3.0.tar.bz2 | tar xjf - - $ cd gmp-6.3.0 - -* build: - - $ make distclean - - #Intel - $ ./configure --enable-cxx --build=core2-apple-darwin"$(uname -r)" - - #ARM - $ ./configure --enable-cxx --build=aarch64-apple-darwin"$(uname -r)" - - $ make && make check - $ sudo make install + $ isabelle component_polyml -G: -M /cygdrive/c/msys64 Makarius @@ -336,6 +370,7 @@ val isabelle_tool1 = Isabelle_Tool("make_polyml", "make Poly/ML from existing sources", Scala_Project.here, { args => + var gmp_root: Option[Path] = None var mingw = MinGW.none var arch_64 = false var sha1_root: Option[Path] = None @@ -344,14 +379,16 @@ Usage: isabelle make_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS] Options are: + -G DIR GMP library root -M DIR msys/mingw root specification for Windows -m ARCH processor architecture (32 or 64, default: """ + (if (arch_64) "64" else "32") + """) -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 Make Poly/ML in the ROOT directory of its sources, with additional - CONFIGURE_OPTIONS (e.g. --without-gmp). + CONFIGURE_OPTIONS. """, + "G:" -> (arg => gmp_root = Some(Path.explode(arg))), "M:" -> (arg => mingw = MinGW(Path.explode(arg))), "m:" -> { @@ -367,8 +404,8 @@ case root :: options => (Path.explode(root), options) case Nil => getopts.usage() } - make_polyml(root, sha1_root = sha1_root, progress = new Console_Progress, - arch_64 = arch_64, options = options, mingw = mingw) + make_polyml(root, gmp_root = gmp_root, sha1_root = sha1_root, + progress = new Console_Progress, arch_64 = arch_64, options = options, mingw = mingw) }) val isabelle_tool2 = @@ -376,6 +413,7 @@ Scala_Project.here, { args => var target_dir = Path.current + var gmp_url = "" var mingw = MinGW.none var component_name = "" var sha1_url = default_sha1_url @@ -384,12 +422,14 @@ var polyml_version = default_polyml_version var polyml_name = default_polyml_name var verbose = false - + val getopts = Getopts(""" Usage: isabelle component_polyml [OPTIONS] [CONFIGURE_OPTIONS] Options are: -D DIR target directory (default ".") + -G URL build GMP library from source: explicit URL or ":" for + """ + standard_gmp_url + """ -M DIR msys/mingw root specification for Windows -N NAME component name (default: derived from Poly/ML version) -S URL SHA1 repository archive area @@ -402,9 +442,10 @@ -v verbose Download and build Poly/ML component from source repositories, with additional - CONFIGURE_OPTIONS (e.g. --without-gmp). + CONFIGURE_OPTIONS. """, "D:" -> (arg => target_dir = Path.explode(arg)), + "G:" -> (arg => gmp_url = if (arg == ":") standard_gmp_url else arg), "M:" -> (arg => mingw = MinGW(Path.explode(arg))), "N:" -> (arg => component_name = arg), "S:" -> (arg => sha1_url = arg), @@ -419,8 +460,8 @@ val progress = new Console_Progress(verbose = verbose) build_polyml(options = options, mingw = mingw, component_name = component_name, - polyml_url = polyml_url, polyml_version = polyml_version, polyml_name = polyml_name, - sha1_url = sha1_url, sha1_version = sha1_version, target_dir = target_dir, - progress = progress) + gmp_url = gmp_url, polyml_url = polyml_url, polyml_version = polyml_version, + polyml_name = polyml_name, sha1_url = sha1_url, sha1_version = sha1_version, + target_dir = target_dir, progress = progress) }) } diff -r 5a0d1075911c -r 3125fd1ee69c src/Pure/System/mingw.scala --- a/src/Pure/System/mingw.scala Mon Apr 07 12:36:56 2025 +0200 +++ b/src/Pure/System/mingw.scala Wed Apr 09 15:31:27 2025 +0200 @@ -25,6 +25,18 @@ case Some(msys_root) => "MinGW(" + msys_root.toString + ")" } + def standard_path(path: Path): String = + root match { + case Some(msys_root) if Platform.is_windows => + val command_line = + java.util.List.of( + File.platform_path(msys_root) + "\\usr\\bin\\cygpath", "-u", File.platform_path(path)) + val res = isabelle.setup.Environment.exec_process(command_line, null, null, false) + if (res.ok) Library.trim_line(res.out) + else error("Error: " + quote(Library.trim_line(res.err))) + case _ => File.standard_path(path) + } + def bash_script(script: String): String = root match { case None => script