# HG changeset patch # User wenzelm # Date 1744310346 -7200 # Node ID 489f4a79d2158f542f7949949fd41afd01020227 # Parent 983c18a451150e1a695ab9dcaf5270a0362ced2b more robust access to GMP library that is provided here; diff -r 983c18a45115 -r 489f4a79d215 src/Pure/Admin/component_polyml.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) diff -r 983c18a45115 -r 489f4a79d215 src/Pure/System/executable.scala --- 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) }