src/Pure/Admin/build_jdk.scala
author wenzelm
Sun, 22 Jan 2017 16:15:08 +0100
changeset 64935 9437a117408b
parent 64934 795055a0be98
child 64936 a11f3ebb7bd8
permissions -rw-r--r--
insist in proper GNU tar, to avoid subtle semantic differences;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64929
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/build_jdk.scala
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
     3
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
     4
Build Isabelle jdk component from original platform installations.
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
     5
*/
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
     6
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
     7
package isabelle
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
     8
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
     9
64933
wenzelm
parents: 64931
diff changeset
    10
import java.nio.file.Files
64934
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
    11
import java.nio.file.attribute.PosixFilePermission
64933
wenzelm
parents: 64931
diff changeset
    12
64929
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    13
import scala.util.matching.Regex
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    14
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    15
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    16
object Build_JDK
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    17
{
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    18
  /* version */
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    19
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    20
  sealed case class Version(short: String, full: String)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    21
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    22
  def detect_version(s: String): Version =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    23
  {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    24
    val Version_Dir_Entry = """^jdk1\.(\d+)\.0_(\d+)(?:\.jdk)?$""".r
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    25
    s match {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    26
      case Version_Dir_Entry(a, b) => Version(a + "u" + b, "1." + a + ".0_" + b)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    27
      case _ => error("Cannot detect JDK version from " + quote(s))
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    28
    }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    29
  }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    30
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    31
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    32
  /* platform */
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    33
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    34
  sealed case class JDK_Platform(name: String, exe: String, regex: Regex)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    35
  {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    36
    override def toString: String = name
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    37
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    38
    def detect(jdk_dir: Path): Boolean =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    39
    {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    40
      val path = jdk_dir + Path.explode(exe)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    41
      if (path.is_file) {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    42
        val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    43
        regex.pattern.matcher(file_descr).matches
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    44
      }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    45
      else false
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    46
    }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    47
  }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    48
  val jdk_platforms =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    49
    List(JDK_Platform("x86-linux", "bin/java", """.*ELF 32-bit.*80386.*""".r),
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    50
      JDK_Platform("x86_64-linux", "bin/java", """.*ELF 64-bit.*x86[-_]64.*""".r),
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    51
      JDK_Platform("x86-windows", "bin/java.exe", """.*PE32 executable.*80386.*""".r),
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    52
      JDK_Platform("x86_64-windows", "bin/java.exe", """.*PE32\+ executable.*x86[-_]64.*""".r),
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    53
      JDK_Platform("x86_64-darwin", "Contents/Home/bin/java", """.*Mach-O 64-bit.*x86[-_]64.*""".r))
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    54
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    55
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    56
  /* README */
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    57
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    58
  def readme(version: Version): String =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    59
"""This is JDK/JRE """ + version.full + """ as required for Isabelle.
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    60
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    61
See http://www.oracle.com/technetwork/java/javase/downloads/index.html
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    62
for the original downloads, which are covered by the Oracle Binary
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    63
Code License Agreement for Java SE.
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    64
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    65
Linux, Windows, Mac OS X all work uniformly, depending on certain
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    66
platform-specific subdirectories.
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    67
"""
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    68
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    69
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    70
  /* settings */
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    71
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    72
  val settings =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    73
"""# -*- shell-script -*- :mode=shellscript:
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    74
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    75
case "$ISABELLE_PLATFORM_FAMILY" in
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    76
  linux)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    77
    ISABELLE_JAVA_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    78
    ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    79
    ;;
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    80
  windows)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    81
    if [ ! -e "$COMPONENT/x86_64-windows" ]; then
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    82
      ISABELLE_JAVA_PLATFORM="x86-windows"
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    83
    elif "$COMPONENT/x86_64-windows/jre/bin/java" -version > /dev/null 2> /dev/null; then
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    84
      ISABELLE_JAVA_PLATFORM="x86_64-windows"
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    85
    else
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    86
      ISABELLE_JAVA_PLATFORM="x86-windows"
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    87
    fi
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    88
    ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    89
    ;;
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    90
  macos)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    91
    if [ -z "$ISABELLE_PLATFORM64" ]; then
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    92
      echo "### Java unavailable on 32bit Mac OS X" >&2
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    93
    else
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    94
      ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    95
      ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM/Contents/Home"
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    96
    fi
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    97
    ;;
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    98
esac
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
    99
"""
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   100
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   101
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   102
  /* extract archive */
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   103
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   104
  def extract_archive(dir: Path, archive: Path): (Version, JDK_Platform) =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   105
  {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   106
    try {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   107
      val tmp_dir = dir + Path.explode("tmp")
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   108
      Isabelle_System.mkdirs(tmp_dir)
64935
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64934
diff changeset
   109
      Isabelle_System.gnutar(
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64934
diff changeset
   110
        "-C " + File.bash_path(tmp_dir) + " -xzf " + File.bash_path(archive)).check
64929
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   111
      val dir_entry =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   112
        File.read_dir(tmp_dir) match {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   113
          case List(s) => s
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   114
          case _ => error("Archive contains multiple directories")
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   115
        }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   116
      val version = detect_version(dir_entry)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   117
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   118
      val jdk_dir = tmp_dir + Path.explode(dir_entry)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   119
      val platform =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   120
        jdk_platforms.find(_.detect(jdk_dir)) getOrElse error("Failed to detect JDK platform")
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   121
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   122
      val platform_dir = dir + Path.explode(platform.name)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   123
      if (platform_dir.is_dir) error("Directory already exists: " + platform_dir)
64930
wenzelm
parents: 64929
diff changeset
   124
      File.move(jdk_dir, platform_dir)
64929
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   125
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   126
      (version, platform)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   127
    }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   128
    catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for " + archive) }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   129
  }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   130
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   131
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   132
  /* build jdk */
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   133
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   134
  def build_jdk(
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   135
    archives: List[Path],
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   136
    progress: Progress = No_Progress,
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   137
    target_dir: Path = Path.current)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   138
  {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   139
    if (Platform.is_windows) error("Cannot build jdk on Windows")
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   140
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   141
    Isabelle_System.with_tmp_dir("jdk")(dir =>
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   142
      {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   143
        progress.echo("Extracting ...")
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   144
        val extracted = archives.map(extract_archive(dir, _))
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   145
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   146
        val version =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   147
          extracted.map(_._1).toSet.toList match {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   148
            case List(version) => version
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   149
            case Nil => error("No archives")
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   150
            case versions =>
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   151
              error("Archives contain multiple JDK versions: " +
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   152
                commas_quote(versions.map(_.short)))
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   153
          }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   154
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   155
        val missing_platforms =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   156
          jdk_platforms.filterNot(p1 => extracted.exists({ case (_, p2) => p1.name == p2.name }))
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   157
        if (missing_platforms.nonEmpty)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   158
          error("Missing platforms: " + commas_quote(missing_platforms.map(_.name)))
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   159
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   160
        val jdk_name = "jdk-" + version.short
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   161
        val jdk_path = Path.explode(jdk_name)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   162
        val component_dir = dir + jdk_path
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   163
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   164
        Isabelle_System.mkdirs(component_dir + Path.explode("etc"))
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   165
        File.write(component_dir + Path.explode("etc/settings"), settings)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   166
        File.write(component_dir + Path.explode("README"), readme(version))
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   167
64930
wenzelm
parents: 64929
diff changeset
   168
        for ((_, platform) <- extracted)
wenzelm
parents: 64929
diff changeset
   169
          File.move(dir + Path.explode(platform.name), component_dir)
64929
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   170
64933
wenzelm
parents: 64931
diff changeset
   171
        for (file <- File.find_files(component_dir.file, include_dirs = true)) {
wenzelm
parents: 64931
diff changeset
   172
          val path = file.toPath
wenzelm
parents: 64931
diff changeset
   173
          val perms = Files.getPosixFilePermissions(path)
64934
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   174
          perms.add(PosixFilePermission.OWNER_READ)
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   175
          perms.add(PosixFilePermission.GROUP_READ)
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   176
          perms.add(PosixFilePermission.OTHERS_READ)
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   177
          perms.add(PosixFilePermission.OWNER_WRITE)
64933
wenzelm
parents: 64931
diff changeset
   178
          if (file.isDirectory) {
64934
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   179
            perms.add(PosixFilePermission.OWNER_WRITE)
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   180
            perms.add(PosixFilePermission.OWNER_EXECUTE)
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   181
            perms.add(PosixFilePermission.GROUP_EXECUTE)
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   182
            perms.add(PosixFilePermission.OTHERS_EXECUTE)
64933
wenzelm
parents: 64931
diff changeset
   183
          }
wenzelm
parents: 64931
diff changeset
   184
          Files.setPosixFilePermissions(path, perms)
wenzelm
parents: 64931
diff changeset
   185
        }
64931
wenzelm
parents: 64930
diff changeset
   186
wenzelm
parents: 64930
diff changeset
   187
        File.find_files((component_dir + Path.explode("x86_64-darwin")).file,
wenzelm
parents: 64930
diff changeset
   188
          file => file.getName.startsWith("._")).foreach(_.delete)
64929
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   189
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   190
        progress.echo("Sharing ...")
64934
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   191
        val main_dir :: other_dirs =
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   192
          jdk_platforms.map(platform => (component_dir + Path.explode(platform.name)).file.toPath)
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   193
        for {
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   194
          file1 <- File.find_files(main_dir.toFile).iterator
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   195
          path1 = file1.toPath
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   196
          dir2 <- other_dirs.iterator
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   197
        } {
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   198
          val path2 = dir2.resolve(main_dir.relativize(path1))
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   199
          val file2 = path2.toFile
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   200
          if (file2.isFile && File.eq_content(file1, file2)) {
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   201
            file2.delete
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   202
            Files.createLink(path2, path1)
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   203
          }
795055a0be98 hardlink within JVM;
wenzelm
parents: 64933
diff changeset
   204
        }
64929
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   205
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   206
        progress.echo("Archiving ...")
64935
9437a117408b insist in proper GNU tar, to avoid subtle semantic differences;
wenzelm
parents: 64934
diff changeset
   207
        Isabelle_System.gnutar("-C " + File.bash_path(dir) + " -czf " +
64929
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   208
          File.bash_path(target_dir + jdk_path.ext("tar.gz")) + " " + jdk_name).check
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   209
      })
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   210
  }
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   211
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   212
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   213
  /* Isabelle tool wrapper */
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   214
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   215
  val isabelle_tool =
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   216
    Isabelle_Tool("build_jdk", "build Isabelle jdk component from original platform installations",
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   217
    args =>
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   218
    {
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   219
      var target_dir = Path.current
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   220
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   221
      val getopts = Getopts("""
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   222
Usage: Admin/build_jdk [OPTIONS] ARCHIVES...
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   223
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   224
  Options are:
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   225
    -D DIR       target directory (default ".")
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   226
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   227
  Build jdk component from tar.gz archives, with original jdk installations
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   228
  for Linux (x86, x86_64), Windows (x86, x86_64), Mac OS X (x86_64).
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   229
""",
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   230
        "D:" -> (arg => target_dir = Path.explode(arg)))
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   231
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   232
      val more_args = getopts(args)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   233
      if (more_args.isEmpty) getopts.usage()
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   234
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   235
      val archives = more_args.map(Path.explode(_))
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   236
      val progress = new Console_Progress()
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   237
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   238
      build_jdk(archives = archives, progress = progress, target_dir = target_dir)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   239
    }, admin = true)
3b4e5fad4dc2 build_jdk in Scala;
wenzelm
parents:
diff changeset
   240
}