# HG changeset patch # User wenzelm # Date 1744231504 -7200 # Node ID 1fa80133027d0bd04e9f1490e57524a872d93215 # Parent 7bd2e917f4253f0adea84372401923a119ca7aee# Parent 40a609d67b3386ac73a89e9584531a5696ce549d merged diff -r 7bd2e917f425 -r 1fa80133027d src/Pure/Admin/component_csdp.scala --- a/src/Pure/Admin/component_csdp.scala Tue Apr 08 21:32:44 2025 +0100 +++ b/src/Pure/Admin/component_csdp.scala Wed Apr 09 22:45:04 2025 +0200 @@ -53,7 +53,7 @@ target_dir: Path = Path.current, mingw: MinGW = MinGW.none ): Unit = { - mingw.check + mingw.check() Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ diff -r 7bd2e917f425 -r 1fa80133027d src/Pure/Admin/component_polyml.scala --- a/src/Pure/Admin/component_polyml.scala Tue Apr 08 21:32:44 2025 +0100 +++ b/src/Pure/Admin/component_polyml.scala Wed Apr 09 22:45:04 2025 +0200 @@ -31,29 +31,44 @@ Platform_Info( options = List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"), - setup = MinGW.environment_export, + setup = MinGW.env_prefix, libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread"))) - 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 + sealed case class Platform_Context( + platform: Isabelle_Platform = Isabelle_Platform.self, + mingw: MinGW = MinGW.none, + progress: Progress = new Progress + ) { + def standard_path(path: Path): String = mingw.standard_path(path) + + def polyml(arch_64: Boolean): String = + (if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name + + def sha1: String = platform.arch_64 + "-" + platform.os_name + + def bash(cwd: Path, script: String, redirect: Boolean = false): 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 make_polyml( + platform_context: Platform_Context, root: Path, + gmp_root: Option[Path] = None, sha1_root: Option[Path] = None, target_dir: Path = Path.current, arch_64: Boolean = false, - options: List[String] = Nil, - mingw: MinGW = MinGW.none, - progress: Progress = new Progress, + options: List[String] = Nil ): Unit = { if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir)) error("Bad Poly/ML root directory: " + root) - val platform = Isabelle_Platform.self - - val sha1_platform = platform.arch_64 + "-" + platform.os_name + val platform = platform_context.platform val info = platform_info.getOrElse(platform.os_name, @@ -62,29 +77,31 @@ if (platform.is_linux) Isabelle_System.require_command("patchelf") - /* bash */ + /* configure and make */ + + val configure_options = { + val options1 = + if (gmp_root.nonEmpty || platform.is_windows) 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 = platform_context.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, + platform_context.bash(root, 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).check /* sha1 library */ @@ -101,9 +118,9 @@ val sha1_files = if (sha1_root.isDefined) { val dir1 = sha1_root.get - bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check + platform_context.bash(dir1, "./build " + platform_context.sha1, redirect = true).check - val dir2 = dir1 + Path.explode(sha1_platform) + val dir2 = dir1 + Path.explode(platform_context.sha1) File.read_dir(dir2).map(entry => dir2 + Path.basic(entry)) } else Nil @@ -111,7 +128,7 @@ /* install */ - val platform_path = Path.explode(polyml_platform(arch_64)) + val platform_path = Path.explode(platform_context.polyml(arch_64)) val platform_dir = target_dir + platform_path Isabelle_System.rm_tree(platform_dir) @@ -128,7 +145,8 @@ for (file <- sha1_files) Isabelle_System.copy_file(file, platform_dir) Executable.libraries_closure( - platform_dir + Path.basic("poly").platform_exe, mingw = mingw, filter = info.libs) + platform_dir + Path.basic("poly").platform_exe, mingw = platform_context.mingw, + filter = info.libs) /* polyc: directory prefix */ @@ -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" @@ -178,17 +198,21 @@ def build_polyml( + platform_context: Platform_Context, 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, sha1_url: String = default_sha1_url, sha1_version: String = default_sha1_version, - target_dir: Path = Path.current, - progress: Progress = new Progress + target_dir: Path = Path.current ): Unit = { + val platform = platform_context.platform + val progress = platform_context.progress + + /* component */ val component_name1 = if (component_name.isEmpty) "polyml-" + polyml_version else component_name @@ -199,6 +223,44 @@ /* download and build */ Isabelle_System.with_tmp_dir("download") { download_dir => + /* GMP library */ + + val gmp_root: Option[Path] = + if (gmp_url.isEmpty) None + else if (platform.is_windows) error("Bad GMP source for Windows: use MinGW version instead") + 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 ...") + platform_context.bash(gmp_dir, + 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) <- @@ -217,15 +279,15 @@ init_src_root(component_dir.src, "RootX86.ML", "ROOT.ML") for (arch_64 <- List(false, true)) { - progress.echo("Building " + polyml_platform(arch_64)) + progress.echo("Building " + platform_context.polyml(arch_64)) make_polyml( + platform_context, root = polyml_download, + gmp_root = gmp_root, sha1_root = Some(sha1_download), target_dir = component_dir.path, arch_64 = arch_64, - options = options, - mingw = mingw, - progress = if (progress.verbose) progress else new Progress) + options = options) } } @@ -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(Platform_Context(mingw = mingw, progress = new Console_Progress), + root, gmp_root = gmp_root, sha1_root = sha1_root, arch_64 = arch_64, options = options) }) 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), @@ -417,10 +458,11 @@ val options = getopts(args) val progress = new Console_Progress(verbose = verbose) + val platform_context = Platform_Context(mingw = mingw, progress = progress) - 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) + build_polyml(platform_context, options = options, component_name = component_name, + 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) }) } diff -r 7bd2e917f425 -r 1fa80133027d src/Pure/Admin/component_verit.scala --- a/src/Pure/Admin/component_verit.scala Tue Apr 08 21:32:44 2025 +0100 +++ b/src/Pure/Admin/component_verit.scala Wed Apr 09 22:45:04 2025 +0200 @@ -19,7 +19,7 @@ target_dir: Path = Path.current, mingw: MinGW = MinGW.none ): Unit = { - mingw.check + mingw.check() Isabelle_System.with_tmp_dir("build") { tmp_dir => /* component */ diff -r 7bd2e917f425 -r 1fa80133027d src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Tue Apr 08 21:32:44 2025 +0100 +++ b/src/Pure/Build/build_manager.scala Wed Apr 09 22:45:04 2025 +0200 @@ -664,7 +664,7 @@ val log_opts = "--graph --color always" val rev1 = "children(" + rev0 + ")" val cmd = repository.command_line("log", Mercurial.opt_rev(rev1 + ":" + rev), log_opts) - val log = Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out + val log = Isabelle_System.bash(Bash.exports("HGPLAINEXCEPT=color") + cmd).check.out if (log.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(log_ext).gz, log) } @@ -677,7 +677,7 @@ if (rev0.nonEmpty && rev.nonEmpty) { val diff_opts = "--noprefix --nodates --ignore-all-space --color always" val cmd = repository.command_line("diff", Mercurial.opt_rev(rev0 + ":" + rev), diff_opts) - val diff = Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out + val diff = Isabelle_System.bash(Bash.exports("HGPLAINEXCEPT=color") + cmd).check.out if (diff.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(diff_ext).gz, diff) } diff -r 7bd2e917f425 -r 1fa80133027d src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Tue Apr 08 21:32:44 2025 +0100 +++ b/src/Pure/General/mercurial.scala Wed Apr 09 22:45:04 2025 +0200 @@ -223,7 +223,8 @@ options: String = "", repository: Boolean = true ): String = { - "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + + Bash.exports("LANG=C", "HGPLAIN=") + + "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") + (if (repository) " --repository " + ssh.bash_path(root) else "") + " --noninteractive " + name + " " + options + " " + args } diff -r 7bd2e917f425 -r 1fa80133027d src/Pure/ML/ml_statistics.scala --- a/src/Pure/ML/ml_statistics.scala Tue Apr 08 21:32:44 2025 +0100 +++ b/src/Pure/ML/ml_statistics.scala Wed Apr 09 22:45:04 2025 +0200 @@ -57,8 +57,7 @@ if (props.nonEmpty) consume(props) } - val env_prefix = - if_proper(stats_dir, "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n") + val env_prefix = if_proper(stats_dir, Bash.exports("POLYSTATSDIR=" + stats_dir)) Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " + Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " + diff -r 7bd2e917f425 -r 1fa80133027d src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Tue Apr 08 21:32:44 2025 +0100 +++ b/src/Pure/System/bash.scala Wed Apr 09 22:45:04 2025 +0200 @@ -42,6 +42,9 @@ def strings(ss: Iterable[String]): String = ss.iterator.map(Bash.string).mkString(" ") + def exports(environment: String*): String = + environment.iterator.map(a => "export " + string(a)).mkString("", "\n", "\n") + /* process and result */ @@ -50,10 +53,8 @@ isabelle_identifier: String = "", cwd: Path = Path.current ): String = { - if_proper(user_home, - "export USER_HOME=" + Bash.string(user_home) + "\n") + - if_proper(isabelle_identifier, - "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n") + + if_proper(user_home, exports("USER_HOME=" + user_home)) + + if_proper(isabelle_identifier, exports("ISABELLE_IDENTIFIER=" + isabelle_identifier)) + (if (cwd == null || cwd.is_current) "" else "cd " + quote(cwd.implode) + "\n") + script } diff -r 7bd2e917f425 -r 1fa80133027d src/Pure/System/mingw.scala --- a/src/Pure/System/mingw.scala Tue Apr 08 21:32:44 2025 +0100 +++ b/src/Pure/System/mingw.scala Wed Apr 09 22:45:04 2025 +0200 @@ -8,11 +8,8 @@ object MinGW { - def environment: List[String] = - List("PATH=/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE=/mingw64/etc/config.site") - - def environment_export: String = - environment.map(a => "export " + Bash.string(a)).mkString("", "\n", "\n") + def env_prefix: String = + Bash.exports("PATH=/usr/bin:/bin:/mingw64/bin", "CONFIG_SITE=/mingw64/etc/config.site") val none: MinGW = new MinGW(None) def apply(path: Path) = new MinGW(Some(path)) @@ -25,12 +22,24 @@ case Some(msys_root) => "MinGW(" + msys_root.toString + ")" } - def bash_script(script: String): String = + 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, env_prefix: String = MinGW.env_prefix): String = root match { case None => script case Some(msys_root) => File.bash_path(msys_root + Path.explode("usr/bin/bash")) + - " -c " + Bash.string(MinGW.environment_export + script) + " -c " + Bash.string(env_prefix + script) } def get_root: Path = @@ -38,7 +47,7 @@ else if (root.isEmpty) error("Windows platform requires msys/mingw root specification") else root.get - def check: Unit = { + def check(): Unit = { if (Platform.is_windows) { get_root try { require(Isabelle_System.bash(bash_script("uname -s")).check.out.startsWith("MSYS")) }