merged
authorwenzelm
Sun, 22 Jan 2017 19:37:06 +0100
changeset 64938 1b584fab241a
parent 64928 18a6b96f8b00 (current diff)
parent 64937 9c94853f03b3 (diff)
child 64939 c8626f7fae06
merged
Admin/java/build
Admin/java/settings
--- a/Admin/components/components.sha1	Sat Jan 21 20:59:47 2017 +0100
+++ b/Admin/components/components.sha1	Sun Jan 22 19:37:06 2017 +0100
@@ -69,6 +69,7 @@
 7d5b152ac70f720bb9e783fa45ecadcf95069584  jdk-7u9.tar.gz
 baf275a68d3f799a841932e4e9a95a1a604058ae  jdk-8u102.tar.gz
 741de6a4a805a0f9fb917d1845409e99346c2747  jdk-8u112.tar.gz
+ae7df8bd0c18eb40237cf54cc28933f4893b9c92  jdk-8u121.tar.gz
 5442f1015a0657259be0590b04572cd933431df7  jdk-8u11.tar.gz
 cfecb1383faaf027ffbabfcd77a0b6a6521e0969  jdk-8u20.tar.gz
 44ffeeae219782d40ce6822b580e608e72fd4c76  jdk-8u31.tar.gz
--- a/Admin/components/main	Sat Jan 21 20:59:47 2017 +0100
+++ b/Admin/components/main	Sun Jan 22 19:37:06 2017 +0100
@@ -4,7 +4,7 @@
 cvc4-1.5pre-4
 e-1.8
 isabelle_fonts-20160830
-jdk-8u112
+jdk-8u121
 jedit_build-20161024
 jfreechart-1.0.14-1
 jortho-1.0-2
--- a/Admin/java/build	Sat Jan 21 20:59:47 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-#!/usr/bin/env bash
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-
-
-## diagnostics
-
-function fail()
-{
-  echo "$1" >&2
-  exit 2
-}
-
-
-## parameters
-
-VERSION="8u112"
-FULL_VERSION="1.8.0_112"
-
-ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
-ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
-ARCHIVE_WINDOWS32="jdk${FULL_VERSION}-w32.tar.gz"
-ARCHIVE_WINDOWS64="jdk${FULL_VERSION}-w64.tar.gz"
-ARCHIVE_DARWIN="jdk${FULL_VERSION}.jdk.tar.gz"
-
-
-## main
-
-DIR="jdk-${VERSION}"
-mkdir "$DIR" || fail "Cannot create fresh directory: \"$DIR\""
-
-
-# README
-
-cat >> "$DIR/README" << EOF
-This is JDK/JRE $FULL_VERSION as required for Isabelle.
-
-See http://www.oracle.com/technetwork/java/javase/downloads/index.html
-for the original downloads, which are covered by the Oracle Binary
-Code License Agreement for Java SE.
-
-Linux, Windows, Mac OS X all work uniformly, depending on certain
-platform-specific subdirectories.
-EOF
-
-
-# settings
-
-mkdir "$DIR/etc"
-cp "$THIS/settings" "$DIR/etc/settings"
-
-
-# content
-
-#GNU tar (notably on Mac OS X)
-type -p gnutar >/dev/null && function tar() { gnutar "$@"; }
-
-mkdir "$DIR/x86-linux" "$DIR/x86_64-linux" "$DIR/x86-windows" "$DIR/x86_64-windows" "$DIR/x86_64-darwin"
-
-tar -C "$DIR/x86-linux" -xf "$ARCHIVE_LINUX32"
-tar -C "$DIR/x86_64-linux" -xf "$ARCHIVE_LINUX64"
-tar -C "$DIR/x86-windows" -xf "$ARCHIVE_WINDOWS32"
-tar -C "$DIR/x86_64-windows" -xf "$ARCHIVE_WINDOWS64"
-tar -C "$DIR/x86_64-darwin" -xf "$ARCHIVE_DARWIN"
-
-(
-  cd "$DIR"
-  for PLATFORM in x86-linux x86_64-linux x86-windows x86_64-windows
-  do
-    mv "$PLATFORM/jdk${FULL_VERSION}"/* "$PLATFORM"/.
-    rmdir "$PLATFORM/jdk${FULL_VERSION}"
-  done
-  PLATFORM=x86_64-darwin
-  mv "$PLATFORM/jdk${FULL_VERSION}.jdk"/* "$PLATFORM"/.
-  rmdir "$PLATFORM/jdk${FULL_VERSION}.jdk"
-)
-
-chgrp -R isabelle "$DIR"
-chmod -R a+r "$DIR"
-chmod -R a+X "$DIR"
-
-find "$DIR/x86_64-darwin" -name "._*" -exec rm -f {} ";"
-
-echo "Sharing ..."
-(
-  cd "$DIR/x86-linux"
-  for FILE in $(find . -type f)
-  do
-    for OTHER in \
-      "../x86_64-linux/$FILE" \
-      "../x86-windows/$FILE" \
-      "../x86_64-windows/$FILE" \
-      "../x86_64-darwin/Contents/Home/$FILE"
-    do
-      if cmp -s "$FILE" "$OTHER"
-      then
-        echo -n "*"
-        ln -f "$FILE" "$OTHER"
-      fi
-    done
-  done
-)
-echo
-
-
-# create archive
-
-echo "Archiving ..."
-tar -c -z -f "${DIR}.tar.gz" "$DIR" && echo "${DIR}.tar.gz"
--- a/Admin/java/settings	Sat Jan 21 20:59:47 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-case "$ISABELLE_PLATFORM_FAMILY" in
-  linux)
-    ISABELLE_JAVA_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
-    ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
-    ;;
-  windows)
-    if [ ! -e "$COMPONENT/x86_64-windows" ]; then
-      ISABELLE_JAVA_PLATFORM="x86-windows"
-    elif "$COMPONENT/x86_64-windows/jre/bin/java" -version > /dev/null 2> /dev/null; then
-      ISABELLE_JAVA_PLATFORM="x86_64-windows"
-    else
-      ISABELLE_JAVA_PLATFORM="x86-windows"
-    fi
-    ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
-    ;;
-  macos)
-    if [ -z "$ISABELLE_PLATFORM64" ]; then
-      echo "### Java unavailable on 32bit Mac OS X" >&2
-    else
-      ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
-      ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM/Contents/Home"
-    fi
-    ;;
-esac
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_jdk.scala	Sun Jan 22 19:37:06 2017 +0100
@@ -0,0 +1,240 @@
+/*  Title:      Pure/Admin/build_jdk.scala
+    Author:     Makarius
+
+Build Isabelle jdk component from original platform installations.
+*/
+
+package isabelle
+
+
+import java.nio.file.Files
+import java.nio.file.attribute.PosixFilePermission
+
+import scala.util.matching.Regex
+
+
+object Build_JDK
+{
+  /* version */
+
+  sealed case class Version(short: String, full: String)
+
+  def detect_version(s: String): Version =
+  {
+    val Version_Dir_Entry = """^jdk1\.(\d+)\.0_(\d+)(?:\.jdk)?$""".r
+    s match {
+      case Version_Dir_Entry(a, b) => Version(a + "u" + b, "1." + a + ".0_" + b)
+      case _ => error("Cannot detect JDK version from " + quote(s))
+    }
+  }
+
+
+  /* platform */
+
+  sealed case class JDK_Platform(name: String, exe: String, regex: Regex)
+  {
+    override def toString: String = name
+
+    def detect(jdk_dir: Path): Boolean =
+    {
+      val path = jdk_dir + Path.explode(exe)
+      if (path.is_file) {
+        val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out
+        regex.pattern.matcher(file_descr).matches
+      }
+      else false
+    }
+  }
+  val jdk_platforms =
+    List(JDK_Platform("x86-linux", "bin/java", """.*ELF 32-bit.*80386.*""".r),
+      JDK_Platform("x86_64-linux", "bin/java", """.*ELF 64-bit.*x86[-_]64.*""".r),
+      JDK_Platform("x86-windows", "bin/java.exe", """.*PE32 executable.*80386.*""".r),
+      JDK_Platform("x86_64-windows", "bin/java.exe", """.*PE32\+ executable.*x86[-_]64.*""".r),
+      JDK_Platform("x86_64-darwin", "Contents/Home/bin/java", """.*Mach-O 64-bit.*x86[-_]64.*""".r))
+
+
+  /* README */
+
+  def readme(version: Version): String =
+"""This is JDK/JRE """ + version.full + """ as required for Isabelle.
+
+See http://www.oracle.com/technetwork/java/javase/downloads/index.html
+for the original downloads, which are covered by the Oracle Binary
+Code License Agreement for Java SE.
+
+Linux, Windows, Mac OS X all work uniformly, depending on certain
+platform-specific subdirectories.
+"""
+
+
+  /* settings */
+
+  val settings =
+"""# -*- shell-script -*- :mode=shellscript:
+
+case "$ISABELLE_PLATFORM_FAMILY" in
+  linux)
+    ISABELLE_JAVA_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM32}"
+    ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
+    ;;
+  windows)
+    if [ ! -e "$COMPONENT/x86_64-windows" ]; then
+      ISABELLE_JAVA_PLATFORM="x86-windows"
+    elif "$COMPONENT/x86_64-windows/jre/bin/java" -version > /dev/null 2> /dev/null; then
+      ISABELLE_JAVA_PLATFORM="x86_64-windows"
+    else
+      ISABELLE_JAVA_PLATFORM="x86-windows"
+    fi
+    ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
+    ;;
+  macos)
+    if [ -z "$ISABELLE_PLATFORM64" ]; then
+      echo "### Java unavailable on 32bit Mac OS X" >&2
+    else
+      ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
+      ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM/Contents/Home"
+    fi
+    ;;
+esac
+"""
+
+
+  /* extract archive */
+
+  def extract_archive(dir: Path, archive: Path): (Version, JDK_Platform) =
+  {
+    try {
+      val tmp_dir = dir + Path.explode("tmp")
+      Isabelle_System.mkdirs(tmp_dir)
+      Isabelle_System.gnutar(
+        "-C " + File.bash_path(tmp_dir) + " -xzf " + File.bash_path(archive)).check
+      val dir_entry =
+        File.read_dir(tmp_dir) match {
+          case List(s) => s
+          case _ => error("Archive contains multiple directories")
+        }
+      val version = detect_version(dir_entry)
+
+      val jdk_dir = tmp_dir + Path.explode(dir_entry)
+      val platform =
+        jdk_platforms.find(_.detect(jdk_dir)) getOrElse error("Failed to detect JDK platform")
+
+      val platform_dir = dir + Path.explode(platform.name)
+      if (platform_dir.is_dir) error("Directory already exists: " + platform_dir)
+      File.move(jdk_dir, platform_dir)
+
+      (version, platform)
+    }
+    catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for " + archive) }
+  }
+
+
+  /* build jdk */
+
+  def build_jdk(
+    archives: List[Path],
+    progress: Progress = No_Progress,
+    target_dir: Path = Path.current)
+  {
+    if (Platform.is_windows) error("Cannot build jdk on Windows")
+
+    Isabelle_System.with_tmp_dir("jdk")(dir =>
+      {
+        progress.echo("Extracting ...")
+        val extracted = archives.map(extract_archive(dir, _))
+
+        val version =
+          extracted.map(_._1).toSet.toList match {
+            case List(version) => version
+            case Nil => error("No archives")
+            case versions =>
+              error("Archives contain multiple JDK versions: " +
+                commas_quote(versions.map(_.short)))
+          }
+
+        val missing_platforms =
+          jdk_platforms.filterNot(p1 => extracted.exists({ case (_, p2) => p1.name == p2.name }))
+        if (missing_platforms.nonEmpty)
+          error("Missing platforms: " + commas_quote(missing_platforms.map(_.name)))
+
+        val jdk_name = "jdk-" + version.short
+        val jdk_path = Path.explode(jdk_name)
+        val component_dir = dir + jdk_path
+
+        Isabelle_System.mkdirs(component_dir + Path.explode("etc"))
+        File.write(component_dir + Path.explode("etc/settings"), settings)
+        File.write(component_dir + Path.explode("README"), readme(version))
+
+        for ((_, platform) <- extracted)
+          File.move(dir + Path.explode(platform.name), component_dir)
+
+        for (file <- File.find_files(component_dir.file, include_dirs = true)) {
+          val path = file.toPath
+          val perms = Files.getPosixFilePermissions(path)
+          perms.add(PosixFilePermission.OWNER_READ)
+          perms.add(PosixFilePermission.GROUP_READ)
+          perms.add(PosixFilePermission.OTHERS_READ)
+          perms.add(PosixFilePermission.OWNER_WRITE)
+          if (file.isDirectory) {
+            perms.add(PosixFilePermission.OWNER_WRITE)
+            perms.add(PosixFilePermission.OWNER_EXECUTE)
+            perms.add(PosixFilePermission.GROUP_EXECUTE)
+            perms.add(PosixFilePermission.OTHERS_EXECUTE)
+          }
+          Files.setPosixFilePermissions(path, perms)
+        }
+
+        File.find_files((component_dir + Path.explode("x86_64-darwin")).file,
+          file => file.getName.startsWith("._")).foreach(_.delete)
+
+        progress.echo("Sharing ...")
+        val main_dir :: other_dirs =
+          jdk_platforms.map(platform => (component_dir + Path.explode(platform.name)).file.toPath)
+        for {
+          file1 <- File.find_files(main_dir.toFile).iterator
+          path1 = file1.toPath
+          dir2 <- other_dirs.iterator
+        } {
+          val path2 = dir2.resolve(main_dir.relativize(path1))
+          val file2 = path2.toFile
+          if (file2.isFile && File.eq_content(file1, file2)) {
+            file2.delete
+            Files.createLink(path2, path1)
+          }
+        }
+
+        progress.echo("Archiving ...")
+        Isabelle_System.gnutar("--owner=root --group=root -C " + File.bash_path(dir) +
+          " -czf " + File.bash_path(target_dir + jdk_path.ext("tar.gz")) + " " + jdk_name).check
+      })
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("build_jdk", "build Isabelle jdk component from original platform installations",
+    args =>
+    {
+      var target_dir = Path.current
+
+      val getopts = Getopts("""
+Usage: Admin/build_jdk [OPTIONS] ARCHIVES...
+
+  Options are:
+    -D DIR       target directory (default ".")
+
+  Build jdk component from tar.gz archives, with original jdk installations
+  for Linux (x86, x86_64), Windows (x86, x86_64), Mac OS X (x86_64).
+""",
+        "D:" -> (arg => target_dir = Path.explode(arg)))
+
+      val more_args = getopts(args)
+      if (more_args.isEmpty) getopts.usage()
+
+      val archives = more_args.map(Path.explode(_))
+      val progress = new Console_Progress()
+
+      build_jdk(archives = archives, progress = progress, target_dir = target_dir)
+    }, admin = true)
+}
--- a/src/Pure/Admin/build_release.scala	Sat Jan 21 20:59:47 2017 +0100
+++ b/src/Pure/Admin/build_release.scala	Sun Jan 22 19:37:06 2017 +0100
@@ -155,11 +155,13 @@
           {
             def execute(script: String): Unit =
               Isabelle_System.bash(script, cwd = tmp_dir.file).check
+            def execute_tar(args: String): Unit =
+              Isabelle_System.gnutar(args, cwd = tmp_dir.file).check
 
             val name = release_info.name
             val platform = Isabelle_System.getenv_strict("ISABELLE_PLATFORM_FAMILY")
             val bundle = release_info.dist_dir + Path.explode(name + "_" + platform + ".tar.gz")
-            execute("tar xzf " + File.bash_path(bundle))
+            execute_tar("xzf " + File.bash_path(bundle))
 
             val other_isabelle =
               new Other_Isabelle(progress, tmp_dir + Path.explode(name), name + "-build")
@@ -171,7 +173,8 @@
 
             execute("chmod -R a+r " + Bash.string(name))
             execute("chmod -R g=o " + Bash.string(name))
-            execute("tar czf " + File.bash_path(release_info.dist_library_archive) +
+            execute_tar("--owner=root --group=root -czf " +
+              File.bash_path(release_info.dist_library_archive) +
               " " + Bash.string(name + "/browser_info"))
           })
       }
--- a/src/Pure/General/file.scala	Sat Jan 21 20:59:47 2017 +0100
+++ b/src/Pure/General/file.scala	Sun Jan 22 19:37:06 2017 +0100
@@ -122,18 +122,26 @@
     else files.toList.map(_.getName)
   }
 
-  def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] =
+  def find_files(
+    start: JFile,
+    pred: JFile => Boolean = _ => true,
+    include_dirs: Boolean = false): List[JFile] =
   {
     val result = new mutable.ListBuffer[JFile]
+    def check(file: JFile) { if (pred(file)) result += file }
 
-    if (start.isFile && pred(start)) result += start
+    if (start.isFile) check(start)
     else if (start.isDirectory) {
       Files.walkFileTree(start.toPath,
         new SimpleFileVisitor[JPath] {
+          override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
+          {
+            if (include_dirs) check(path.toFile)
+            FileVisitResult.CONTINUE
+          }
           override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
           {
-            val file = path.toFile
-            if (pred(file)) result += file
+            check(path.toFile)
             FileVisitResult.CONTINUE
           }
         }
@@ -240,6 +248,16 @@
   def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file)
 
 
+  /* eq_content */
+
+  def eq_content(file1: JFile, file2: JFile): Boolean =
+    if (eq(file1, file2)) true
+    else if (file1.length != file2.length) false
+    else Bytes.read(file1) == Bytes.read(file2)
+
+  def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file)
+
+
   /* copy */
 
   def copy(src: JFile, dst: JFile)
--- a/src/Pure/System/isabelle_system.scala	Sat Jan 21 20:59:47 2017 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sun Jan 22 19:37:06 2017 +0100
@@ -302,6 +302,16 @@
       result(progress_stdout, progress_stderr, progress_limit, strict)
   }
 
+  private lazy val gnutar_check: Boolean =
+    try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") }
+    catch { case ERROR(_) => false }
+
+  def gnutar(args: String, cwd: JFile = null, redirect: Boolean = false): Process_Result =
+  {
+    if (gnutar_check) bash("tar " + args, cwd = cwd, redirect = redirect)
+    else error("Expected to find GNU tar executable")
+  }
+
   def hostname(): String = bash("hostname -s").check.out
 
   def open(arg: String): Unit =
--- a/src/Pure/System/isabelle_tool.scala	Sat Jan 21 20:59:47 2017 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Sun Jan 22 19:37:06 2017 +0100
@@ -102,6 +102,7 @@
       Build.isabelle_tool,
       Build_Doc.isabelle_tool,
       Build_Docker.isabelle_tool,
+      Build_JDK.isabelle_tool,
       Build_PolyML.isabelle_tool,
       Build_Stats.isabelle_tool,
       Check_Sources.isabelle_tool,
--- a/src/Pure/build-jars	Sat Jan 21 20:59:47 2017 +0100
+++ b/src/Pure/build-jars	Sun Jan 22 19:37:06 2017 +0100
@@ -12,6 +12,7 @@
   Admin/build_doc.scala
   Admin/build_docker.scala
   Admin/build_history.scala
+  Admin/build_jdk.scala
   Admin/build_log.scala
   Admin/build_polyml.scala
   Admin/build_release.scala