# HG changeset patch # User wenzelm # Date 1485110226 -3600 # Node ID 1b584fab241a728fa3ea1dbe72c1bef08bb7d086 # Parent 18a6b96f8b009d78f6f487afb1559bdd12c47179# Parent 9c94853f03b37aeefb8a797c41404c7d8598ddef merged diff -r 18a6b96f8b00 -r 1b584fab241a Admin/components/components.sha1 --- 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 diff -r 18a6b96f8b00 -r 1b584fab241a Admin/components/main --- 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 diff -r 18a6b96f8b00 -r 1b584fab241a Admin/java/build --- 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" diff -r 18a6b96f8b00 -r 1b584fab241a Admin/java/settings --- 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 diff -r 18a6b96f8b00 -r 1b584fab241a src/Pure/Admin/build_jdk.scala --- /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) +} diff -r 18a6b96f8b00 -r 1b584fab241a src/Pure/Admin/build_release.scala --- 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")) }) } diff -r 18a6b96f8b00 -r 1b584fab241a src/Pure/General/file.scala --- 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) diff -r 18a6b96f8b00 -r 1b584fab241a src/Pure/System/isabelle_system.scala --- 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 = diff -r 18a6b96f8b00 -r 1b584fab241a src/Pure/System/isabelle_tool.scala --- 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, diff -r 18a6b96f8b00 -r 1b584fab241a src/Pure/build-jars --- 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