| 
72448
 | 
     1  | 
/*  Title:      Pure/System/executable.scala
  | 
| 
 | 
     2  | 
    Author:     Makarius
  | 
| 
 | 
     3  | 
  | 
| 
 | 
     4  | 
Support for platform-specific executables.
  | 
| 
 | 
     5  | 
*/
  | 
| 
 | 
     6  | 
  | 
| 
 | 
     7  | 
package isabelle
  | 
| 
 | 
     8  | 
  | 
| 
 | 
     9  | 
  | 
| 
75393
 | 
    10  | 
object Executable {
 | 
| 
72460
 | 
    11  | 
  def libraries_closure(path: Path,
  | 
| 
72454
 | 
    12  | 
    mingw: MinGW = MinGW.none,
  | 
| 
72460
 | 
    13  | 
    filter: String => Boolean = _ => true,
  | 
| 
75393
 | 
    14  | 
    patchelf: Boolean = false
  | 
| 
 | 
    15  | 
  ): List[String] = {
 | 
| 
72460
 | 
    16  | 
    val exe_path = path.expand
  | 
| 
72454
 | 
    17  | 
    val exe_dir = exe_path.dir
  | 
| 
 | 
    18  | 
    val exe = exe_path.base
  | 
| 
72448
 | 
    19  | 
  | 
| 
75393
 | 
    20  | 
    val ldd_lines = {
 | 
| 
72454
 | 
    21  | 
      val ldd = if (Platform.is_macos) "otool -L" else "ldd"
  | 
| 
 | 
    22  | 
      val script = mingw.bash_script(ldd + " " + File.bash_path(exe))
  | 
| 
 | 
    23  | 
      Library.split_lines(Isabelle_System.bash(script, cwd = exe_dir.file).check.out)
  | 
| 
72448
 | 
    24  | 
    }
  | 
| 
 | 
    25  | 
  | 
| 
72454
 | 
    26  | 
    def lib_name(lib: String): String =
  | 
| 
72468
 | 
    27  | 
      Library.take_prefix[Char](c => c != '.' && c != '-',
  | 
| 
72454
 | 
    28  | 
        Library.take_suffix[Char](_ != '/', lib.toList)._2)._1.mkString
  | 
| 
 | 
    29  | 
  | 
| 
 | 
    30  | 
    val libs =
  | 
| 
 | 
    31  | 
      if (Platform.is_macos) {
 | 
| 
 | 
    32  | 
        val Pattern = """^\s*(/.+)\s+\(.*\)$""".r
  | 
| 
 | 
    33  | 
        for {
 | 
| 
 | 
    34  | 
          Pattern(lib) <- ldd_lines
  | 
| 
 | 
    35  | 
          if !lib.startsWith("@executable_path/") && filter(lib_name(lib))
 | 
| 
 | 
    36  | 
        } yield lib
  | 
| 
 | 
    37  | 
      }
  | 
| 
 | 
    38  | 
      else {
 | 
| 
 | 
    39  | 
        val Pattern = """^.*=>\s*(/.+)\s+\(.*\)$""".r
  | 
| 
 | 
    40  | 
        val prefix =
  | 
| 
 | 
    41  | 
          mingw.root match {
 | 
| 
 | 
    42  | 
            case None => ""
  | 
| 
 | 
    43  | 
            case Some(path) => path.absolute.implode
  | 
| 
 | 
    44  | 
          }
  | 
| 
 | 
    45  | 
        for { Pattern(lib) <- ldd_lines if filter(lib_name(lib)) }
 | 
| 
 | 
    46  | 
          yield prefix + lib
  | 
| 
 | 
    47  | 
      }
  | 
| 
 | 
    48  | 
  | 
| 
 | 
    49  | 
    if (libs.nonEmpty) {
 | 
| 
73317
 | 
    50  | 
      libs.foreach(lib => Isabelle_System.copy_file(Path.explode(lib), exe_dir))
  | 
| 
72454
 | 
    51  | 
  | 
| 
 | 
    52  | 
      if (Platform.is_linux) {
 | 
| 
72460
 | 
    53  | 
        if (patchelf) {
 | 
| 
 | 
    54  | 
          // requires e.g. Ubuntu 16.04 LTS
  | 
| 
 | 
    55  | 
          Isabelle_System.require_command("patchelf")
 | 
| 
 | 
    56  | 
          Isabelle_System.bash("patchelf --force-rpath --set-rpath '$ORIGIN' " + File.bash_path(exe_path)).check
 | 
| 
 | 
    57  | 
        }
  | 
| 
 | 
    58  | 
        else {
 | 
| 
 | 
    59  | 
          // requires e.g. LDFLAGS=-Wl,-rpath,_DUMMY_
  | 
| 
 | 
    60  | 
          Isabelle_System.require_command("chrpath")
 | 
| 
 | 
    61  | 
          Isabelle_System.bash("chrpath -r '$ORIGIN' " + File.bash_path(exe_path)).check
 | 
| 
 | 
    62  | 
        }
  | 
| 
72454
 | 
    63  | 
      }
  | 
| 
 | 
    64  | 
      else if (Platform.is_macos) {
 | 
| 
 | 
    65  | 
        val script =
  | 
| 
 | 
    66  | 
          ("install_name_tool" ::
 | 
| 
 | 
    67  | 
            libs.map(file => "-change " + Bash.string(file) + " " +
  | 
| 
 | 
    68  | 
              Bash.string("@executable_path/" + Path.explode(file).file_name) + " " +
 | 
| 
 | 
    69  | 
              File.bash_path(exe))).mkString(" ")
 | 
| 
 | 
    70  | 
        Isabelle_System.bash(script, cwd = exe_dir.file).check
  | 
| 
72448
 | 
    71  | 
      }
  | 
| 
 | 
    72  | 
    }
  | 
| 
72454
 | 
    73  | 
  | 
| 
 | 
    74  | 
    libs
  | 
| 
72448
 | 
    75  | 
  }
  | 
| 
 | 
    76  | 
}
  |