--- a/src/Pure/Admin/component_polyml.scala Thu Apr 10 20:02:38 2025 +0200
+++ b/src/Pure/Admin/component_polyml.scala Thu Apr 10 20:39:06 2025 +0200
@@ -119,8 +119,14 @@
if (gmp_root.nonEmpty || platform.is_windows) List("--with-gmp")
else List("--without-gmp")
+ def detect_CFLAGS(s: String): Boolean = s.startsWith("CFLAGS=")
+
+ val info_options =
+ if (info.options.exists(detect_CFLAGS)) info.options
+ else "CFLAGS=" :: info.options
+
val options2 =
- for (opt <- info.options) yield {
+ 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)
@@ -136,8 +142,18 @@
options1 ::: options2 ::: options ::: options3
}
+ val gmp_setup =
+ gmp_root match {
+ case Some(dir) =>
+ val v = Executable.library_path_variable(platform)
+ val p = Isabelle_System.getenv(v)
+ val s = platform_context.standard_path(dir)
+ Bash.exports(v + "=" + s + if_proper(p, ":" + p))
+ case None => ""
+ }
+
platform_context.execute(root,
- info.setup,
+ info.setup + gmp_setup,
"[ -f Makefile ] && make distclean",
"""./configure --prefix="$PWD/target" """ + Bash.strings(configure_options),
"rm -rf target",
@@ -173,7 +189,9 @@
for (file <- sha1_files) Isabelle_System.copy_file(file, platform_dir)
Executable.libraries_closure(
- platform_dir + Path.basic("poly").platform_exe, mingw = platform_context.mingw,
+ platform_dir + Path.basic("poly").platform_exe,
+ env_prefix = gmp_setup,
+ mingw = platform_context.mingw,
filter = info.libs)
--- a/src/Pure/System/executable.scala Thu Apr 10 20:02:38 2025 +0200
+++ b/src/Pure/System/executable.scala Thu Apr 10 20:39:06 2025 +0200
@@ -8,7 +8,14 @@
object Executable {
+ def library_path_variable(platform: Isabelle_Platform): String =
+ if (platform.is_linux) "LD_LIBRARY_PATH"
+ else if (platform.is_macos) "DYLD_LIBRARY_PATH"
+ else if (platform.is_windows) "PATH"
+ else error("Bad platform " + platform)
+
def libraries_closure(path: Path,
+ env_prefix: String = "",
mingw: MinGW = MinGW.none,
filter: String => Boolean = _ => true
): List[String] = {
@@ -18,7 +25,7 @@
val ldd_lines = {
val ldd = if (Platform.is_macos) "otool -L" else "ldd"
- val script = mingw.bash_script(ldd + " " + File.bash_path(exe))
+ val script = mingw.bash_script(env_prefix + ldd + " " + File.bash_path(exe))
split_lines(Isabelle_System.bash(script, cwd = exe_dir).check.out)
}