# HG changeset patch # User wenzelm # Date 1744568517 -7200 # Node ID 9e5f645d60007fdc25ff79b031b0434f418a287a # Parent d35d355f733042bbe4383417a657e134bc4c4ffe# Parent d46bc8a03141216c7adb9d3e82c2b73297775ef8 merged diff -r d35d355f7330 -r 9e5f645d6000 src/Pure/Admin/component_csdp.scala --- a/src/Pure/Admin/component_csdp.scala Sat Apr 12 22:42:32 2025 +0100 +++ b/src/Pure/Admin/component_csdp.scala Sun Apr 13 20:21:57 2025 +0200 @@ -118,7 +118,7 @@ Isabelle_System.copy_file(source_dir + Path.explode("solver/csdp").platform_exe, platform_dir) if (Platform.is_windows) { - Executable.libraries_closure(platform_dir + Path.explode("csdp.exe"), mingw = mingw, + Executable.library_closure(platform_dir + Path.explode("csdp.exe"), mingw = mingw, filter = Set("libblas", "liblapack", "libgfortran", "libgcc_s_seh", "libquadmath", "libwinpthread")) diff -r d35d355f7330 -r 9e5f645d6000 src/Pure/Admin/component_polyml.scala --- a/src/Pure/Admin/component_polyml.scala Sat Apr 12 22:42:32 2025 +0100 +++ b/src/Pure/Admin/component_polyml.scala Sun Apr 13 20:21:57 2025 +0200 @@ -17,29 +17,34 @@ setup: String = "", libs: Set[String] = Set.empty) - private val platform_info = Map( - "linux" -> - Platform_Info( - options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"), - libs = Set("libgmp")), - "darwin" -> - Platform_Info( - options = List("CFLAGS=-O3", "CXXFLAGS=-O3", "LDFLAGS=-segprot POLY rwx rwx"), - setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin", - libs = Set("libpolyml", "libgmp")), - "windows" -> - Platform_Info( - options = - List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"), - setup = MinGW.env_prefix, - libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread"))) - 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 info: Platform_Info = + if (platform.is_linux) { + Platform_Info( + options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"), + libs = Set("libgmp")) + } + else if (platform.is_macos) { + Platform_Info( + options = List("CFLAGS=-O3", "CXXFLAGS=-O3", "LDFLAGS=-segprot POLY rwx rwx"), + setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin", + libs = Set("libpolyml", "libgmp")) + } + else if (platform.is_windows) { + Platform_Info( + options = + List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"), + setup = MinGW.env_prefix, + libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread")) + } + else error("Bad platform: " + quote(platform.toString)) + + def standard_path(path: Path): String = + mingw.standard_path(File.standard_path(path)) def polyml(arch_64: Boolean): String = (if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name @@ -84,12 +89,18 @@ "[ -f Makefile ] && make distclean", "./configure --disable-static --enable-shared --enable-cxx" + " --build=" + platform_arch + "-" + platform_os + - " --prefix=" + Bash.string(platform_context.standard_path(target_dir)) + - if_proper(options, " " + Bash.strings(options)), + """ --prefix="$PWD/target" """ + Bash.strings(options), + "rm -rf target", "make", "make check", "make install") + if (platform.is_windows) { + val bin_dir = target_dir + Path.explode("bin") + val lib_dir = target_dir + Path.explode("lib") + Isabelle_System.copy_dir(bin_dir, lib_dir, direct = true) + } + target_dir } @@ -107,19 +118,14 @@ val platform = platform_context.platform - val info = - platform_info.getOrElse(platform.os_name, - error("Bad OS platform: " + quote(platform.os_name))) - - if (platform.is_linux) Isabelle_System.require_command("patchelf") + val info = platform_context.info /* configure and make */ val configure_options = { val options1 = - if (gmp_root.nonEmpty || platform.is_windows) List("--with-gmp") - else List("--without-gmp") + if (gmp_root.nonEmpty) List("--with-gmp") else List("--without-gmp") def detect_CFLAGS(s: String): Boolean = s.startsWith("CFLAGS=") @@ -190,7 +196,7 @@ for (file <- sha1_files) Isabelle_System.copy_file(file, platform_dir) - Executable.libraries_closure( + Executable.library_closure( platform_dir + Path.basic("poly").platform_exe, env_prefix = gmp_setup + "\n", mingw = platform_context.mingw, @@ -218,7 +224,7 @@ /** skeleton for component **/ - val standard_gmp_url = "https://gmplib.org/download/gmp/gmp-6.3.0.tar.bz2" + val default_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" @@ -250,6 +256,7 @@ options: List[String] = Nil, component_name: String = "", gmp_url: String = "", + gmp_root: Option[Path] = None, polyml_url: String = default_polyml_url, polyml_version: String = default_polyml_version, polyml_name: String = default_polyml_name, @@ -273,9 +280,8 @@ Isabelle_System.with_tmp_dir("build") { build_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") + val gmp_root1: Option[Path] = + if (gmp_url.isEmpty) gmp_root else { val gmp_dir = Isabelle_System.make_directory(build_dir + Path.basic("gmp")) @@ -309,11 +315,11 @@ init_src_root(component_dir.src, "RootX86.ML", "ROOT.ML") for (arch_64 <- List(false, true)) { - progress.echo("Building " + platform_context.polyml(arch_64)) + progress.echo("Building Poly/ML " + platform_context.polyml(arch_64)) make_polyml( platform_context, root = polyml_download, - gmp_root = gmp_root, + gmp_root = gmp_root1, sha1_root = Some(sha1_download), target_dir = component_dir.path, arch_64 = arch_64, @@ -382,11 +388,11 @@ * Linux and macOS - $ isabelle component_polyml -G: + $ isabelle component_polyml * Windows (Cygwin shell) - $ isabelle component_polyml -G: -M /cygdrive/c/msys64 + $ isabelle component_polyml -M /cygdrive/c/msys64 Makarius @@ -423,8 +429,12 @@ } val progress = new Console_Progress(verbose = verbose) - make_polyml_gmp(Platform_Context(mingw = mingw, progress = progress), - root, options = options) + + val target_dir = + make_polyml_gmp(Platform_Context(mingw = mingw, progress = progress), + root, options = options) + + progress.echo("GMP installation directory: " + target_dir) }) val isabelle_tool2 = @@ -477,7 +487,7 @@ Scala_Project.here, { args => var target_dir = Path.current - var gmp_url = "" + var gmp_url = default_gmp_url var mingw = MinGW.none var component_name = "" var sha1_url = default_sha1_url @@ -485,6 +495,7 @@ var polyml_url = default_polyml_url var polyml_version = default_polyml_version var polyml_name = default_polyml_name + var gmp_root: Option[Path] = None var verbose = false val getopts = Getopts(""" @@ -492,8 +503,8 @@ Options are: -D DIR target directory (default ".") - -G URL build GMP library from source: explicit URL or ":" for - """ + standard_gmp_url + """ + -G URL build GMP library from source (overrides option -g) + (default """ + quote(default_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 @@ -503,13 +514,14 @@ (default: """ + quote(default_polyml_url) + """) -V VERSION Poly/ML version (default: """ + quote(default_polyml_version) + """) -W NAME Poly/ML name (default: """ + quote(default_polyml_name) + """) + -g DIR use existing GMP library (overrides option -G) -v verbose Download and build Poly/ML component from source repositories, with additional CONFIGURE_OPTIONS. """, "D:" -> (arg => target_dir = Path.explode(arg)), - "G:" -> (arg => gmp_url = if (arg == ":") standard_gmp_url else arg), + "G:" -> (arg => { gmp_url = arg; gmp_root = None }), "M:" -> (arg => mingw = MinGW(Path.explode(arg))), "N:" -> (arg => component_name = arg), "S:" -> (arg => sha1_url = arg), @@ -517,6 +529,7 @@ "U:" -> (arg => polyml_url = arg), "V:" -> (arg => polyml_version = arg), "W:" -> (arg => polyml_name = arg), + "g:" -> (arg => { gmp_root = Some(Path.explode(arg)); gmp_url = "" }), "v" -> (_ => verbose = true)) val options = getopts(args) @@ -525,8 +538,8 @@ val platform_context = Platform_Context(mingw = mingw, 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) + gmp_url = gmp_url, gmp_root = gmp_root, 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 d35d355f7330 -r 9e5f645d6000 src/Pure/Admin/component_verit.scala --- a/src/Pure/Admin/component_verit.scala Sat Apr 12 22:42:32 2025 +0100 +++ b/src/Pure/Admin/component_verit.scala Sun Apr 13 20:21:57 2025 +0200 @@ -79,7 +79,7 @@ val exe_path = Path.basic("veriT").platform_exe Isabelle_System.copy_file(source_dir + exe_path, platform_dir) - Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw) + Executable.library_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw) /* settings */ diff -r d35d355f7330 -r 9e5f645d6000 src/Pure/Admin/component_zipperposition.scala --- a/src/Pure/Admin/component_zipperposition.scala Sat Apr 12 22:42:32 2025 +0100 +++ b/src/Pure/Admin/component_zipperposition.scala Sun Apr 13 20:21:57 2025 +0200 @@ -57,7 +57,7 @@ Isabelle_System.copy_file(build_dir + Path.basic("bin") + prg_path, platform_dir + exe_path) if (!Platform.is_windows) { - Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp")) + Executable.library_closure(platform_dir + exe_path, filter = Set("libgmp")) } diff -r d35d355f7330 -r 9e5f645d6000 src/Pure/System/executable.scala --- a/src/Pure/System/executable.scala Sat Apr 12 22:42:32 2025 +0100 +++ b/src/Pure/System/executable.scala Sun Apr 13 20:21:57 2025 +0200 @@ -14,7 +14,7 @@ else if (platform.is_windows) "PATH" else error("Bad platform " + platform) - def libraries_closure(path: Path, + def library_closure(path: Path, env_prefix: String = "", mingw: MinGW = MinGW.none, filter: String => Boolean = _ => true @@ -23,7 +23,7 @@ val exe_dir = exe_path.dir val exe = exe_path.base - val ldd_lines = { + val lines = { val ldd = if (Platform.is_macos) "otool -L" else "ldd" val script = mingw.bash_script(env_prefix + ldd + " " + File.bash_path(exe)) split_lines(Isabelle_System.bash(script, cwd = exe_dir).check.out) @@ -37,19 +37,14 @@ if (Platform.is_macos) { val Pattern = """^\s*(/.+)\s+\(.*\)$""".r for { - case Pattern(lib) <- ldd_lines + case Pattern(lib) <- lines if !lib.startsWith("@executable_path/") && filter(lib_name(lib)) } yield lib } else { val Pattern = """^.*=>\s*(/.+)\s+\(.*\)$""".r - val prefix = - mingw.root match { - case None => "" - case Some(path) => path.absolute.implode - } - for { case Pattern(lib) <- ldd_lines if filter(lib_name(lib)) } - yield prefix + lib + for { case Pattern(lib) <- lines if filter(lib_name(lib)) } + yield File.standard_path(mingw.platform_path(lib)) } if (libs.nonEmpty) { diff -r d35d355f7330 -r 9e5f645d6000 src/Pure/System/mingw.scala --- a/src/Pure/System/mingw.scala Sat Apr 12 22:42:32 2025 +0100 +++ b/src/Pure/System/mingw.scala Sun Apr 13 20:21:57 2025 +0200 @@ -22,18 +22,24 @@ case Some(msys_root) => "MinGW(" + msys_root.toString + ")" } - def standard_path(path: Path): String = + private def convert_path(str: String, opt: String): Option[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)) + File.platform_path(msys_root) + "\\usr\\bin\\cygpath", opt, str) val res = isabelle.setup.Environment.exec_process(command_line, null, null, false) - if (res.ok) Library.trim_line(res.out) + if (res.ok) Some(Library.trim_line(res.out)) else error("Error: " + quote(Library.trim_line(res.err))) - case _ => File.standard_path(path) + case _ => None } + def standard_path(platform_path: String): String = + convert_path(platform_path, "-u") getOrElse File.standard_path(platform_path) + + def platform_path(standard_path: String): String = + convert_path(standard_path, "-w") getOrElse File.platform_path(standard_path) + def bash_script(script: String, env_prefix: String = MinGW.env_prefix): String = root match { case None => script