always use patchelf on Linux: base-line is Ubuntu 18.04 where that works properly (see also e79294c4230c);
--- a/src/Pure/Admin/component_polyml.scala Sat Jan 20 13:24:26 2024 +0100
+++ b/src/Pure/Admin/component_polyml.scala Sat Jan 20 13:31:07 2024 +0100
@@ -62,7 +62,7 @@
platform_info.getOrElse(platform.os_name,
error("Bad OS platform: " + quote(platform.os_name)))
- if (platform.is_linux) Isabelle_System.require_command("chrpath")
+ if (platform.is_linux) Isabelle_System.require_command("patchelf")
/* bash */
--- a/src/Pure/Admin/component_zipperposition.scala Sat Jan 20 13:24:26 2024 +0100
+++ b/src/Pure/Admin/component_zipperposition.scala Sat Jan 20 13:31:07 2024 +0100
@@ -60,8 +60,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"), patchelf = true)
+ Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"))
}
--- a/src/Pure/System/executable.scala Sat Jan 20 13:24:26 2024 +0100
+++ b/src/Pure/System/executable.scala Sat Jan 20 13:31:07 2024 +0100
@@ -10,8 +10,7 @@
object Executable {
def libraries_closure(path: Path,
mingw: MinGW = MinGW.none,
- filter: String => Boolean = _ => true,
- patchelf: Boolean = false
+ filter: String => Boolean = _ => true
): List[String] = {
val exe_path = path.expand
val exe_dir = exe_path.dir
@@ -50,16 +49,8 @@
libs.foreach(lib => Isabelle_System.copy_file(Path.explode(lib), exe_dir))
if (Platform.is_linux) {
- if (patchelf) {
- // requires e.g. Ubuntu 18.04 LTS
- Isabelle_System.require_command("patchelf")
- Isabelle_System.bash("patchelf --force-rpath --set-rpath '$ORIGIN' " + File.bash_path(exe_path)).check
- }
- else {
- // requires e.g. LDFLAGS=-Wl,-rpath,_DUMMY_
- Isabelle_System.require_command("chrpath")
- Isabelle_System.bash("chrpath -r '$ORIGIN' " + File.bash_path(exe_path)).check
- }
+ Isabelle_System.require_command("patchelf")
+ Isabelle_System.bash("patchelf --force-rpath --set-rpath '$ORIGIN' " + File.bash_path(exe_path)).check
}
else if (Platform.is_macos) {
val script =