more robust access to GMP library that is provided here;
authorwenzelm
Thu, 10 Apr 2025 20:39:06 +0200
changeset 82480 489f4a79d215
parent 82479 983c18a45115
child 82481 041d65893a85
more robust access to GMP library that is provided here;
src/Pure/Admin/component_polyml.scala
src/Pure/System/executable.scala
--- 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)
     }