--- a/src/Pure/Admin/component_polyml.scala Wed Apr 09 15:31:27 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala Wed Apr 09 16:55:20 2025 +0200
@@ -34,43 +34,41 @@
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,
+ sealed case class Platform_Context(
+ platform: Isabelle_Platform = Isabelle_Platform.self,
+ mingw: MinGW = MinGW.none,
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 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 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
+ 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,
@@ -88,7 +86,7 @@
for (opt <- info.options) yield {
if (opt.startsWith("CFLAGS=") && gmp_root.nonEmpty) {
val root0 = gmp_root.get.absolute
- val root1 = mingw.standard_path(root0)
+ 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"
}
@@ -101,7 +99,7 @@
options1 ::: options2 ::: options ::: options3
}
- bash(root, platform, mingw,
+ platform_context.bash(root,
info.setup + "\n" +
"""
[ -f Makefile ] && make distclean
@@ -110,7 +108,7 @@
rm -rf target
make && make install
} || { echo "Build failed" >&2; exit 2; }
- """, redirect = true, progress = progress).check
+ """, redirect = true).check
/* sha1 library */
@@ -118,10 +116,9 @@
val sha1_files =
if (sha1_root.isDefined) {
val dir1 = sha1_root.get
- bash(dir1, platform, mingw, "./build " + sha1_platform, redirect = true,
- progress = progress).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
@@ -129,7 +126,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)
@@ -146,7 +143,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 */
@@ -198,8 +196,8 @@
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,
@@ -207,10 +205,10 @@
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 = Isabelle_Platform.self
+ val platform = platform_context.platform
+ val progress = platform_context.progress
/* component */
@@ -244,7 +242,7 @@
else error("Bad platform " + platform)
progress.echo("Building GMP library ...")
- bash(gmp_dir, platform, mingw, progress = progress,
+ platform_context.bash(gmp_dir,
script = Library.make_lines(
"set -e",
"./configure --enable-cxx --build=" + platform_arch + "-" + platform_os +
@@ -278,16 +276,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)
}
}
@@ -404,8 +401,8 @@
case root :: options => (Path.explode(root), options)
case Nil => getopts.usage()
}
- make_polyml(root, gmp_root = gmp_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 =
@@ -458,10 +455,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,
+ 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, progress = progress)
+ target_dir = target_dir)
})
}