diff --git a/src/Pure/Admin/build_jdk.scala b/src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala
+++ b/src/Pure/Admin/build_jdk.scala
@@ -1,241 +1,240 @@
/* Title: Pure/Admin/build_jdk.scala
Author: Makarius
Build Isabelle jdk component from original platform installations.
*/
package isabelle
import java.io.{File => JFile}
import java.nio.file.Files
import java.nio.file.attribute.PosixFilePermission
import scala.util.matching.Regex
object Build_JDK
{
/* platform and version information */
sealed case class JDK_Platform(
platform_name: String,
platform_regex: Regex,
exe: String = "java",
macos_home: Boolean = false,
jdk_version: String = "")
{
override def toString: String = platform_name
def platform_path: Path = Path.explode(platform_name)
def detect(jdk_dir: Path): Option[JDK_Platform] =
{
val major_version =
{
val Major_Version = """.*jdk(\d+).*$""".r
val jdk_name = jdk_dir.file.getName
jdk_name match {
case Major_Version(s) => s
case _ => error("Cannot determine major version from " + quote(jdk_name))
}
}
val path = jdk_dir + Path.explode("bin") + Path.explode(exe)
if (path.is_file) {
val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out
if (platform_regex.pattern.matcher(file_descr).matches) {
val Version = ("^(" + major_version + """\.[0-9.]+\+\d+)(?:-LTS)?$""").r
val version_lines =
Isabelle_System.bash("strings " + File.bash_path(path)).check
.out_lines.flatMap({ case Version(s) => Some(s) case _ => None })
version_lines match {
case List(jdk_version) => Some(copy(jdk_version = jdk_version))
case _ => error("Expected unique version within executable " + path)
}
}
else None
}
else None
}
}
val templates: List[JDK_Platform] =
List(
JDK_Platform("arm64-darwin", """.*Mach-O 64-bit.*arm64.*""".r, macos_home = true),
JDK_Platform("arm64-linux", """.*ELF 64-bit.*ARM aarch64.*""".r),
JDK_Platform("x86_64-darwin", """.*Mach-O 64-bit.*x86[-_]64.*""".r, macos_home = true),
JDK_Platform("x86_64-linux", """.*ELF 64-bit.*x86[-_]64.*""".r),
JDK_Platform("x86_64-windows", """.*PE32\+ executable.*x86[-_]64.*""".r, exe = "java.exe"))
/* README */
def readme(jdk_version: String): String =
"""This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also
https://www.azul.com/downloads/zulu-community/?package=jdk
The main license is GPL2, but some modules are covered by other (more liberal)
licenses, see legal/* for details.
Linux, Windows, macOS all work uniformly, depending on platform-specific
subdirectories.
"""
/* settings */
val settings: String =
"""# -*- shell-script -*- :mode=shellscript:
case "$ISABELLE_PLATFORM_FAMILY" in
linux)
ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
;;
windows)
ISABELLE_JAVA_PLATFORM="$ISABELLE_WINDOWS_PLATFORM64"
ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
;;
macos)
if [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$COMPONENT/$ISABELLE_APPLE_PLATFORM64" ]
then
ISABELLE_JAVA_PLATFORM="$ISABELLE_APPLE_PLATFORM64"
else
ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
fi
ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
;;
esac
"""
/* extract archive */
def extract_archive(dir: Path, archive: Path): JDK_Platform =
{
try {
val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp"))
if (archive.get_ext == "zip") {
Isabelle_System.bash(
"unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check
}
else {
Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
}
val dir_entry =
File.read_dir(tmp_dir) match {
case List(s) => s
case _ => error("Archive contains multiple directories")
}
val jdk_dir = tmp_dir + Path.explode(dir_entry)
val platform =
templates.view.flatMap(_.detect(jdk_dir))
.headOption.getOrElse(error("Failed to detect JDK platform"))
val platform_dir = dir + platform.platform_path
if (platform_dir.is_dir) error("Directory already exists: " + platform_dir)
Isabelle_System.move_file(jdk_dir, platform_dir)
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 = new Progress,
target_dir: Path = Path.current): Unit =
{
if (Platform.is_windows) error("Cannot build jdk on Windows")
Isabelle_System.with_tmp_dir("jdk")(dir =>
{
progress.echo("Extracting ...")
val platforms = archives.map(extract_archive(dir, _))
val jdk_version =
platforms.map(_.jdk_version).distinct match {
case List(version) => version
case Nil => error("No archives")
case versions =>
error("Archives contain multiple JDK versions: " + commas_quote(versions))
}
templates.filterNot(p1 => platforms.exists(p2 => p1.platform_name == p2.platform_name))
match {
case Nil =>
case missing => error("Missing platforms: " + commas_quote(missing.map(_.platform_name)))
}
val jdk_name = "jdk-" + jdk_version
val jdk_path = Path.explode(jdk_name)
val component_dir = dir + jdk_path
Isabelle_System.make_directory(component_dir + Path.explode("etc"))
File.write(Components.settings(component_dir), settings)
File.write(component_dir + Path.explode("README"), readme(jdk_version))
for (platform <- platforms) {
Isabelle_System.move_file(dir + platform.platform_path, 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)
}
progress.echo("Archiving ...")
Isabelle_System.gnutar(
- "-czf " + File.bash_path(target_dir + jdk_path.ext("tar.gz")) + " " + jdk_name,
- dir = dir).check
+ "-czf " + File.bash_path(target_dir + jdk_path.tar.gz) + " " + jdk_name, dir = dir).check
})
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives",
Scala_Project.here, args =>
{
var target_dir = Path.current
val getopts = Getopts("""
Usage: isabelle build_jdk [OPTIONS] ARCHIVES...
Options are:
-D DIR target directory (default ".")
Build jdk component from tar.gz archives, with original jdk archives
for Linux, Windows, and macOS.
""",
"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)
})
}
diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala
+++ b/src/Pure/Admin/build_release.scala
@@ -1,895 +1,930 @@
/* Title: Pure/Admin/build_release.scala
Author: Makarius
Build full Isabelle distribution from repository.
*/
package isabelle
object Build_Release
{
- /** release info **/
+ /** release context **/
+
+ private def execute(dir: Path, script: String): Unit =
+ Isabelle_System.bash(script, cwd = dir.file).check
+
+ private def execute_tar(dir: Path, args: String, strip: Int = 0): Unit =
+ Isabelle_System.gnutar(args, dir = dir, strip = strip).check
+
+ object Release_Context
+ {
+ def apply(
+ target_dir: Path,
+ release_name: String = "",
+ components_base: Path = Components.default_components_base,
+ progress: Progress = new Progress): Release_Context =
+ {
+ val date = Date.now()
+ val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
+ val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
+ new Release_Context(release_name, dist_name, dist_dir, components_base, progress)
+ }
+ }
+
+ class Release_Context private[Build_Release](
+ val release_name: String,
+ val dist_name: String,
+ val dist_dir: Path,
+ val components_base: Path,
+ val progress: Progress)
+ {
+ override def toString: String = dist_name
+
+ val isabelle: Path = Path.explode(dist_name)
+ val isabelle_dir: Path = dist_dir + isabelle
+ val isabelle_archive: Path = dist_dir + isabelle.tar.gz
+ val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
+
+ def other_isabelle(dir: Path): Other_Isabelle =
+ Other_Isabelle(dir + isabelle,
+ isabelle_identifier = dist_name + "-build",
+ progress = progress)
+
+ def make_announce(id: String): Unit =
+ {
+ if (release_name.isEmpty) {
+ File.write(isabelle_dir + Path.explode("ANNOUNCE"),
+ """
+IMPORTANT NOTE
+==============
+
+This is a snapshot of Isabelle/""" + id + """ from the repository.
+""")
+ }
+ }
+
+ def make_contrib(): Unit =
+ {
+ Isabelle_System.make_directory(Components.contrib(isabelle_dir))
+ File.write(Components.contrib(isabelle_dir, name = "README"),
+ """This directory contains add-on components that contribute to the main
+Isabelle distribution. Separate licensing conditions apply, see each
+directory individually.
+""")
+ }
+
+ def bundle_info(platform: Platform.Family.Value): Bundle_Info =
+ platform match {
+ case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
+ case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
+ case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
+ }
+ }
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
name: String)
{
def path: Path = Path.explode(name)
}
- class Release private[Build_Release](
- progress: Progress,
- val date: Date,
- val dist_name: String,
- val dist_dir: Path,
- val dist_version: String,
- val ident: String,
- val tags: String)
+
+
+ /** release archive **/
+
+ val ISABELLE: Path = Path.basic("Isabelle")
+ val ISABELLE_ID: Path = Path.explode("etc/ISABELLE_ID")
+ val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS")
+ val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER")
+
+ object Release_Archive
{
- val isabelle: Path = Path.explode(dist_name)
- val isabelle_dir: Path = dist_dir + isabelle
- val isabelle_id: Path = isabelle_dir + Path.explode("etc/ISABELLE_ID")
- val isabelle_tags: Path = isabelle_dir + Path.explode("etc/ISABELLE_TAGS")
- val isabelle_identifier: Path = isabelle_dir + Path.explode("etc/ISABELLE_IDENTIFIER")
- val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz")
- val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz")
+ def make(bytes: Bytes, rename: String = ""): Release_Archive =
+ {
+ Isabelle_System.with_tmp_dir("tmp")(dir =>
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
+ {
+ val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
- def other_isabelle(dir: Path): Other_Isabelle =
- Other_Isabelle(dir + isabelle,
- isabelle_identifier = dist_name + "-build",
- progress = progress)
+ Bytes.write(archive_path, bytes)
+ execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1)
- def bundle_info(platform: Platform.Family.Value): Bundle_Info =
- platform match {
- case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz")
- case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz")
- case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe")
- }
+ val id = File.read(isabelle_dir + ISABELLE_ID)
+ val tags = File.read(isabelle_dir + ISABELLE_TAGS)
+ val identifier = File.read(isabelle_dir + ISABELLE_IDENTIFIER)
+
+ val (bytes1, identifier1) =
+ if (rename.isEmpty || rename == identifier) (bytes, identifier)
+ else {
+ File.write(isabelle_dir + ISABELLE_IDENTIFIER, rename)
+ Isabelle_System.move_file(isabelle_dir, dir + Path.basic(rename))
+ execute_tar(dir, "-czf " + File.bash_path(archive_path) + " " + Bash.string(rename))
+ (Bytes.read(archive_path), rename)
+ }
+ new Release_Archive(bytes1, id, tags, identifier1)
+ })
+ )
+ }
+
+ def read(path: Path, rename: String = ""): Release_Archive =
+ make(Bytes.read(path), rename = rename)
+
+ def get(url: String, rename: String = "", progress: Progress = new Progress): Release_Archive =
+ {
+ val bytes =
+ if (Path.is_wellformed(url)) Bytes.read(Path.explode(url))
+ else Isabelle_System.download(url, progress = progress).bytes
+ make(bytes, rename = rename)
+ }
+ }
+
+ case class Release_Archive private[Build_Release](
+ bytes: Bytes, id: String, tags: String, identifier: String)
+ {
+ override def toString: String = identifier
}
/** generated content **/
- /* ANNOUNCE */
-
- def make_announce(release: Release): Unit =
- {
- File.write(release.isabelle_dir + Path.explode("ANNOUNCE"),
-"""
-IMPORTANT NOTE
-==============
-
-This is a snapshot of Isabelle/""" + release.ident + """ from the repository.
-
-""")
- }
-
-
- /* NEWS */
-
- def make_news(other_isabelle: Other_Isabelle, dist_version: String): Unit =
- {
- val target = other_isabelle.isabelle_home + Path.explode("doc")
- val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts"))
- other_isabelle.copy_fonts(target_fonts)
-
- HTML.write_document(target, "NEWS.html",
- List(HTML.title("NEWS (" + dist_version + ")")),
- List(
- HTML.chapter("NEWS"),
- HTML.source(
- Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS"))))))
- }
-
-
/* bundled components */
class Bundled(platform: Option[Platform.Family.Value] = None)
{
def detect(s: String): Boolean =
s.startsWith("#bundled") && !s.startsWith("#bundled ")
def apply(name: String): String =
"#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name
private val Pattern1 = ("""^#bundled:(.*)$""").r
private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r
def unapply(s: String): Option[String] =
s match {
case Pattern1(name) => Some(name)
case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name)
case _ => None
}
}
def record_bundled_components(dir: Path): Unit =
{
val catalogs =
List("main", "bundled").map((_, new Bundled())) :::
default_platform_families.flatMap(platform =>
List(platform.toString, "bundled-" + platform.toString).
map((_, new Bundled(platform = Some(platform)))))
File.append(Components.components(dir),
terminate_lines("#bundled components" ::
(for {
(catalog, bundled) <- catalogs.iterator
path = Components.admin(dir) + Path.basic(catalog)
if path.is_file
line <- split_lines(File.read(path))
if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build")
} yield bundled(line)).toList))
}
def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
{
val Bundled = new Bundled(platform = Some(platform))
val components =
for {
Bundled(name) <- Components.read_components(dir)
if !name.startsWith("jedit_build")
} yield name
val jdk_component =
components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
(components, jdk_component)
}
def activate_components(
dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit =
{
def contrib_name(name: String): String =
Components.contrib(name = name).implode
val Bundled = new Bundled(platform = Some(platform))
Components.write_components(dir,
Components.read_components(dir).flatMap(line =>
line match {
case Bundled(name) =>
if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
else None
case _ => if (Bundled.detect(line)) None else Some(line)
}) ::: more_names.map(contrib_name))
}
- def make_contrib(dir: Path): Unit =
- {
- Isabelle_System.make_directory(Components.contrib(dir))
- File.write(Components.contrib(dir, "README"),
-"""This directory contains add-on components that contribute to the main
-Isabelle distribution. Separate licensing conditions apply, see each
-directory individually.
-""")
- }
-
-
/** build release **/
- private def execute(dir: Path, script: String): Unit =
- Isabelle_System.bash(script, cwd = dir.file).check
-
- private def execute_tar(dir: Path, args: String): Unit =
- Isabelle_System.gnutar(args, dir = dir).check
-
-
/* build heaps on remote server */
private def remote_build_heaps(
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
local_dir: Path): Unit =
{
val server_option = "build_host_" + platform.toString
options.string(server_option) match {
case SSH.Target(user, host) =>
using(SSH.open_session(options, host = host, user = user))(ssh =>
- {
- Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar =>
+ Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
{
execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
ssh.with_tmp_dir(remote_dir =>
{
val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
ssh.write_file(remote_tmp_tar, local_tmp_tar)
val remote_commands =
List(
"cd " + File.bash_path(remote_dir),
"tar -xf tmp.tar",
- "./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
+ "bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions),
"tar -cf tmp.tar heaps")
ssh.execute(remote_commands.mkString(" && ")).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
})
execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
})
- })
+ )
case s => error("Bad " + server_option + ": " + quote(s))
}
}
/* Isabelle application */
def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit =
{
val title = "# Java runtime options"
File.write(path, (title :: options).map(_ + line_ending).mkString)
}
def make_isabelle_app(
platform: Platform.Family.Value,
isabelle_target: Path,
isabelle_name: String,
jdk_component: String,
classpath: List[Path],
dock_icon: Boolean = false): Unit =
{
val script = """#!/usr/bin/env bash
#
# Author: Makarius
#
# Main Isabelle application script.
# minimal Isabelle environment
ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/../.."; pwd)"
source "$ISABELLE_HOME/lib/scripts/isabelle-platform"
#paranoia settings -- avoid intrusion of alien options
unset "_JAVA_OPTIONS"
unset "JAVA_TOOL_OPTIONS"
#paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc.
unset XMODIFIERS
COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """"
source "$COMPONENT/etc/settings"
# main
declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options"))
"$ISABELLE_HOME/bin/isabelle" env "$ISABELLE_HOME/lib/scripts/java-gui-setup"
exec "$ISABELLE_JDK_HOME/bin/java" \
"-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \
-classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \
"-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \
""" + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \
""" else "") + """isabelle.Main "$@"
"""
val script_path = isabelle_target + Path.explode("lib/scripts/Isabelle_app")
File.write(script_path, script)
File.set_executable(script_path, true)
val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app")
Isabelle_System.move_file(
component_dir + Path.explode(Platform.standard_platform(platform)) + Path.explode("Isabelle"),
isabelle_target + Path.explode(isabelle_name))
Isabelle_System.rm_tree(component_dir)
}
def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit =
{
File.write(path, """
CFBundleDevelopmentRegion
English
CFBundleIconFile
isabelle.icns
CFBundleIdentifier
de.tum.in.isabelle
CFBundleDisplayName
""" + isabelle_name + """
CFBundleInfoDictionaryVersion
6.0
CFBundleName
""" + isabelle_name + """
CFBundlePackageType
APPL
CFBundleShortVersionString
""" + isabelle_name + """
CFBundleSignature
????
CFBundleVersion
""" + isabelle_rev + """
NSHumanReadableCopyright
LSMinimumSystemVersion
10.11
LSApplicationCategoryType
public.app-category.developer-tools
NSHighResolutionCapable
true
NSSupportsAutomaticGraphicsSwitching
true
CFBundleDocumentTypes
CFBundleTypeExtensions
thy
CFBundleTypeIconFile
theory.icns
CFBundleTypeName
Isabelle theory file
CFBundleTypeRole
Editor
LSTypeIsPackage
""")
}
/* main */
private val default_platform_families: List[Platform.Family.Value] =
List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos)
- def build_release(options: Options,
- target_dir: Path = Path.current,
- components_base: Path = Components.default_components_base,
- progress: Progress = new Progress,
- rev: String = "",
- afp_rev: String = "",
- proper_release_name: Option[String] = None,
- platform_families: List[Platform.Family.Value] = default_platform_families,
- more_components: List[Path] = Nil,
- website: Option[Path] = None,
- build_sessions: List[String] = Nil,
- build_library: Boolean = false,
- parallel_jobs: Int = 1): Release =
+ def use_release_archive(
+ context: Release_Context,
+ archive: Release_Archive,
+ id: String = ""): Unit =
{
- val hg = Mercurial.repository(Path.ISABELLE_HOME)
-
- val release =
- {
- val date = Date.now()
- val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date))
- val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
-
- val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
- val ident =
- try { hg.id(version) }
- catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
- val tags = hg.tags(rev = ident)
-
- val dist_version =
- proper_release_name match {
- case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date)
- case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date)
- }
-
- new Release(progress, date, dist_name, dist_dir, dist_version, ident, tags)
+ if (id.nonEmpty && id != archive.id) {
+ error("Mismatch of release identification " + id + " vs. archive " + archive.id)
}
-
- /* make distribution */
-
- if (release.isabelle_archive.is_file) {
- progress.echo_warning("Release archive already exists: " + release.isabelle_archive)
+ if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) {
+ Bytes.write(context.isabelle_archive, archive.bytes)
+ }
+ }
- val archive_ident =
- Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
- {
- val isabelle_id = release.isabelle + Path.explode("etc/ISABELLE_ID")
- execute_tar(tmp_dir, "-xzf " +
- File.bash_path(release.isabelle_archive) + " " + File.bash_path(isabelle_id))
- Isabelle_System.isabelle_id(root = tmp_dir + release.isabelle)
- })
+ def build_release_archive(
+ context: Release_Context,
+ version: String,
+ parallel_jobs: Int = 1): Unit =
+ {
+ val progress = context.progress
- if (release.ident != archive_ident) {
- error("Mismatch of release identification " + release.ident +
- " vs. archive " + archive_ident)
- }
+ val hg = Mercurial.repository(Path.ISABELLE_HOME)
+ val id =
+ try { hg.id(version) }
+ catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
+
+ if (context.isabelle_archive.is_file) {
+ progress.echo_warning("Found existing release archive: " + context.isabelle_archive)
+ use_release_archive(context, Release_Archive.read(context.isabelle_archive), id = id)
}
else {
- progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...")
-
- Isabelle_System.make_directory(release.dist_dir)
+ progress.echo_warning("Preparing release " + context.dist_name + " ...")
- if (release.isabelle_dir.is_dir)
- error("Directory " + release.isabelle_dir + " already exists")
+ Isabelle_System.new_directory(context.dist_dir)
-
- progress.echo_warning("Retrieving Mercurial repository version " + release.ident)
-
- hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files")
+ hg.archive(context.isabelle_dir.expand.implode, rev = id, options = "--type files")
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
- (release.isabelle_dir + Path.explode(name)).file.delete
+ (context.isabelle_dir + Path.explode(name)).file.delete
}
-
- progress.echo_warning("Preparing distribution " + quote(release.dist_name))
-
- File.write(release.isabelle_id, release.ident)
- File.write(release.isabelle_tags, release.tags)
- File.write(release.isabelle_identifier, release.dist_name)
+ File.write(context.isabelle_dir + ISABELLE_ID, id)
+ File.write(context.isabelle_dir + ISABELLE_TAGS, hg.tags(rev = id))
+ File.write(context.isabelle_dir + ISABELLE_IDENTIFIER, context.dist_name)
- if (proper_release_name.isEmpty) make_announce(release)
+ context.make_announce(id)
- make_contrib(release.isabelle_dir)
+ context.make_contrib()
- execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
+ execute(context.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
- record_bundled_components(release.isabelle_dir)
+ record_bundled_components(context.isabelle_dir)
/* build tools and documentation */
- val other_isabelle = release.other_isabelle(release.dist_dir)
+ val other_isabelle = context.other_isabelle(context.dist_dir)
other_isabelle.init_settings(
- other_isabelle.init_components(components_base = components_base, catalogs = List("main")))
+ other_isabelle.init_components(
+ components_base = context.components_base, catalogs = List("main")))
other_isabelle.resolve_components(echo = true)
try {
val export_classpath =
"export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n"
- other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
- other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
+ other_isabelle.bash(export_classpath + "Admin/build all", echo = true).check
+ other_isabelle.bash(export_classpath + "bin/isabelle jedit -b", echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
try {
other_isabelle.bash(
- "./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
+ "bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
}
catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
- make_news(other_isabelle, release.dist_version)
+ other_isabelle.make_news()
for (name <- List("Admin", "browser_info", "heaps")) {
Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name))
}
other_isabelle.cleanup()
- progress.echo_warning("Creating distribution archive " + release.isabelle_archive)
-
- def execute_dist_name(script: String): Unit =
- Isabelle_System.bash(script, cwd = release.dist_dir.file,
- env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check
-
- execute_dist_name("""
-set -e
-
-chmod -R a+r "$DIST_NAME"
-chmod -R u+w "$DIST_NAME"
-chmod -R g=o "$DIST_NAME"
-find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w
-""")
-
- execute_tar(release.dist_dir, "-czf " +
- File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name))
+ progress.echo_warning("Creating release archive " + context.isabelle_archive + " ...")
- execute_dist_name("""
-set -e
-
-mv "$DIST_NAME" "${DIST_NAME}-old"
-mkdir "$DIST_NAME"
+ execute(context.dist_dir, """chmod -R a+r . && chmod -R u+w . && chmod -R g=o .""")
+ execute(context.dist_dir,
+ """find . -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w""")
+ execute_tar(context.dist_dir, "-czf " +
+ File.bash_path(context.isabelle_archive) + " " + Bash.string(context.dist_name))
+ }
+ }
-mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \
- "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME"
-mkdir "$DIST_NAME/doc"
-mv "${DIST_NAME}-old/doc/"*.pdf \
- "${DIST_NAME}-old/doc/"*.html \
- "${DIST_NAME}-old/doc/"*.css \
- "${DIST_NAME}-old/doc/fonts" \
- "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc"
+ def build_release(
+ options: Options,
+ context: Release_Context,
+ afp_rev: String = "",
+ platform_families: List[Platform.Family.Value] = default_platform_families,
+ more_components: List[Path] = Nil,
+ website: Option[Path] = None,
+ build_sessions: List[String] = Nil,
+ build_library: Boolean = false,
+ parallel_jobs: Int = 1): Unit =
+ {
+ val progress = context.progress
-rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle
-rm -rf "${DIST_NAME}-old"
-""")
+ /* release directory */
+
+ val archive = Release_Archive.read(context.isabelle_archive)
+
+ for (path <- List(context.isabelle, ISABELLE)) {
+ Isabelle_System.rm_tree(context.dist_dir + path)
}
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
+ {
+ Bytes.write(archive_path, archive.bytes)
+ val extract =
+ List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
+ map(name => context.dist_name + "/" + name)
+ execute_tar(context.dist_dir,
+ "-xzf " + File.bash_path(archive_path) + " " + Bash.strings(extract))
+ })
+
+ Isabelle_System.symlink(Path.explode(context.dist_name), context.dist_dir + ISABELLE)
+
/* make application bundles */
- val bundle_infos = platform_families.map(release.bundle_info)
+ val bundle_infos = platform_families.map(context.bundle_info)
for (bundle_info <- bundle_infos) {
- val isabelle_name = release.dist_name
+ val isabelle_name = context.dist_name
val platform = bundle_info.platform
progress.echo("\nApplication bundle for " + platform)
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
// release archive
- execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
- val other_isabelle = release.other_isabelle(tmp_dir)
+ execute_tar(tmp_dir, "-xzf " + File.bash_path(context.isabelle_archive))
+ val other_isabelle = context.other_isabelle(tmp_dir)
val isabelle_target = other_isabelle.isabelle_home
// bundled components
progress.echo("Bundled components:")
val contrib_dir = Components.contrib(isabelle_target)
val (bundled_components, jdk_component) =
get_bundled_components(isabelle_target, platform)
- Components.resolve(components_base, bundled_components,
+ Components.resolve(context.components_base, bundled_components,
target_dir = Some(contrib_dir),
- copy_dir = Some(release.dist_dir + Path.explode("contrib")),
+ copy_dir = Some(context.dist_dir + Path.explode("contrib")),
progress = progress)
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
Components.purge(contrib_dir, platform)
activate_components(isabelle_target, platform, more_components_names)
// Java parameters
val java_options: List[String] =
(for {
variable <-
List(
"ISABELLE_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_SYSTEM_OPTIONS",
"JEDIT_JAVA_OPTIONS")
opt <- Word.explode(other_isabelle.getenv(variable))
}
yield {
val s = "-Dapple.awt.application.name="
if (opt.startsWith(s)) s + isabelle_name else opt
}) ::: List("-Disabelle.jedit_server=" + isabelle_name)
val classpath: List[Path] =
{
val base = isabelle_target.absolute
Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
{
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
}
}) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
// build heaps
if (build_sessions.nonEmpty) {
progress.echo("Building heaps ...")
remote_build_heaps(options, platform, build_sessions, isabelle_target)
}
// application bundling
platform match {
case Platform.Family.linux =>
File.change(isabelle_target + jedit_options,
_.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24"))
File.change(isabelle_target + jedit_props,
_.replaceAll("console.fontsize=.*", "console.fontsize=18")
.replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18")
.replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18")
.replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18")
.replaceAll("view.fontsize=.*", "view.fontsize=24")
.replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16"))
make_isabelle_options(
isabelle_target + Path.explode("Isabelle.options"), java_options)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component, classpath)
val archive_name = isabelle_name + "_linux.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
execute_tar(tmp_dir,
- "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+ "-czf " + File.bash_path(context.dist_dir + Path.explode(archive_name)) + " " +
Bash.string(isabelle_name))
case Platform.Family.macos =>
File.change(isabelle_target + jedit_props,
_.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
.replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d"))
// macOS application bundle
val app_contents = isabelle_target + Path.explode("Contents")
for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) {
Isabelle_System.copy_file(isabelle_target + Path.explode(icon),
Isabelle_System.make_directory(app_contents + Path.explode("Resources")))
}
make_isabelle_plist(
- app_contents + Path.explode("Info.plist"), isabelle_name, release.ident)
+ app_contents + Path.explode("Info.plist"), isabelle_name, archive.id)
make_isabelle_app(platform, isabelle_target, isabelle_name, jdk_component,
classpath, dock_icon = true)
val isabelle_options = Path.explode("Isabelle.options")
make_isabelle_options(
isabelle_target + isabelle_options,
java_options ::: List("-Disabelle.app=true"))
// application archive
val archive_name = isabelle_name + "_macos.tar.gz"
progress.echo("Packaging " + archive_name + " ...")
val isabelle_app = Path.explode(isabelle_name + ".app")
Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name),
tmp_dir + isabelle_app)
execute_tar(tmp_dir,
- "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+ "-czf " + File.bash_path(context.dist_dir + Path.explode(archive_name)) + " " +
File.bash_path(isabelle_app))
case Platform.Family.windows =>
File.change(isabelle_target + jedit_props,
_.replaceAll("foldPainter=.*", "foldPainter=Square"))
// application launcher
Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
val app_template = Path.explode("~~/Admin/Windows/launch4j")
make_isabelle_options(
isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
java_options, line_ending = "\r\n")
val isabelle_xml = Path.explode("isabelle.xml")
val isabelle_exe = Path.explode(isabelle_name + ".exe")
File.write(tmp_dir + isabelle_xml,
File.read(app_template + isabelle_xml)
.replace("{ISABELLE_NAME}", isabelle_name)
.replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe))
.replace("{ICON}",
File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
.replace("{SPLASH}",
File.platform_path(app_template + Path.explode("isabelle.bmp")))
.replace("{CLASSPATH}",
cat_lines(classpath.map(cp =>
" %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "")))
.replace("\\jdk\\", "\\" + jdk_component + "\\"))
execute(tmp_dir,
"\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"),
isabelle_target + isabelle_exe.ext("manifest"))
// Cygwin setup
val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"),
isabelle_target)
val cygwin_mirror =
File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
val cygwin_bat = Path.explode("Cygwin-Setup.bat")
File.write(isabelle_target + cygwin_bat,
File.read(cygwin_template + cygwin_bat).replace("{MIRROR}", cygwin_mirror))
File.set_executable(isabelle_target + cygwin_bat, true)
for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
val path = Path.explode(name)
Isabelle_System.copy_file(cygwin_template + path,
isabelle_target + Path.explode("contrib/cygwin") + path)
}
execute(isabelle_target,
"""find . -type f -not -name "*.exe" -not -name "*.dll" """ +
(if (Platform.is_macos) "-perm +100" else "-executable") +
" -print0 > contrib/cygwin/isabelle/executables")
execute(isabelle_target,
"""find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
"""> contrib/cygwin/isabelle/symlinks""")
execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
// executable archive (self-extracting 7z)
val archive_name = isabelle_name + ".7z"
val exe_archive = tmp_dir + Path.explode(archive_name)
exe_archive.file.delete
progress.echo("Packaging " + archive_name + " ...")
execute(tmp_dir,
"7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
val sfx_txt =
File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt"))
.replace("{ISABELLE_NAME}", isabelle_name)
- Bytes.write(release.dist_dir + isabelle_exe,
+ Bytes.write(context.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
- File.set_executable(release.dist_dir + isabelle_exe, true)
+ File.set_executable(context.dist_dir + isabelle_exe, true)
}
})
progress.echo("DONE")
}
/* minimal website */
for (dir <- website) {
val website_platform_bundles =
for {
bundle_info <- bundle_infos
- if (release.dist_dir + bundle_info.path).is_file
+ if (context.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val isabelle_link =
- HTML.link(Isabelle_System.isabelle_repository.changeset(release.ident),
- HTML.text("Isabelle/" + release.ident))
+ HTML.link(Isabelle_System.isabelle_repository.changeset(archive.id),
+ HTML.text("Isabelle/" + archive.id))
val afp_link =
HTML.link(Isabelle_System.afp_repository.changeset(afp_rev),
HTML.text("AFP/" + afp_rev))
HTML.write_document(dir, "index.html",
- List(HTML.title(release.dist_name)),
+ List(HTML.title(context.dist_name)),
List(
- HTML.section(release.dist_name),
- HTML.subsection("Platforms"),
+ HTML.section(context.dist_name),
+ HTML.subsection("Downloads"),
HTML.itemize(
+ List(HTML.link(context.dist_name + ".tar.gz", HTML.text("Source archive"))) ::
website_platform_bundles.map({ case (bundle, bundle_info) =>
- List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })),
+ List(HTML.link(bundle, HTML.text(bundle_info.platform_description + " bundle"))) })),
HTML.subsection("Repositories"),
HTML.itemize(
List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
- for ((bundle, _) <- website_platform_bundles)
- Isabelle_System.copy_file(release.dist_dir + Path.explode(bundle), dir)
+ Isabelle_System.copy_file(context.isabelle_archive, dir)
+
+ for ((bundle, _) <- website_platform_bundles) {
+ Isabelle_System.copy_file(context.dist_dir + Path.explode(bundle), dir)
+ }
}
/* HTML library */
if (build_library) {
- if (release.isabelle_library_archive.is_file) {
- progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive)
+ if (context.isabelle_library_archive.is_file) {
+ progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
}
else {
Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
{
val bundle =
- release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz")
+ context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
- val other_isabelle = release.other_isabelle(tmp_dir)
+ val other_isabelle = context.other_isabelle(tmp_dir)
Isabelle_System.make_directory(other_isabelle.etc)
File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n")
other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
" -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
" -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check
other_isabelle.isabelle_home_user.file.delete
- execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name))
- execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name))
- execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) +
- " " + Bash.string(release.dist_name + "/browser_info"))
+ execute(tmp_dir, "chmod -R a+r " + Bash.string(context.dist_name))
+ execute(tmp_dir, "chmod -R g=o " + Bash.string(context.dist_name))
+ execute_tar(tmp_dir, "-czf " + File.bash_path(context.isabelle_library_archive) +
+ " " + Bash.string(context.dist_name + "/browser_info"))
})
}
}
-
- release
}
/** command line entry point **/
def main(args: Array[String]): Unit =
{
Command_Line.tool {
var afp_rev = ""
var components_base: Path = Components.default_components_base
var target_dir = Path.current
- var proper_release_name: Option[String] = None
+ var release_name = ""
+ var source_archive = ""
var website: Option[Path] = None
var build_sessions: List[String] = Nil
var more_components: List[Path] = Nil
var parallel_jobs = 1
var build_library = false
var options = Options.init()
var platform_families = default_platform_families
var rev = ""
val getopts = Getopts("""
Usage: Admin/build_release [OPTIONS] BASE_DIR
Options are:
-A REV corresponding AFP changeset id
-C DIR base directory for Isabelle components (default: """ +
Components.default_components_base + """)
-D DIR target directory (default ".")
- -R RELEASE proper release with name
+ -R RELEASE explicit release name
+ -S ARCHIVE use existing source archive (file or URL)
-W WEBSITE produce minimal website in given directory
-b SESSIONS build platform-specific session images (separated by commas)
-c ARCHIVE clean bundling with additional component .tar.gz archive
-j INT maximum number of parallel jobs (default 1)
-l build library
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-p NAMES platform families (default: """ + default_platform_families.mkString(",") + """)
- -r REV Mercurial changeset id (default: RELEASE or tip)
+ -r REV Mercurial changeset id (default: ARCHIVE or RELEASE or tip)
Build Isabelle release in base directory, using the local repository clone.
""",
"A:" -> (arg => afp_rev = arg),
"C:" -> (arg => components_base = Path.explode(arg)),
"D:" -> (arg => target_dir = Path.explode(arg)),
- "R:" -> (arg => proper_release_name = Some(arg)),
+ "R:" -> (arg => release_name = arg),
+ "S:" -> (arg => source_archive = arg),
"W:" -> (arg => website = Some(Path.explode(arg))),
"b:" -> (arg => build_sessions = space_explode(',', arg)),
"c:" -> (arg =>
{
val path = Path.explode(arg)
Components.Archive.get_name(path.file_name)
more_components = more_components ::: List(path)
}),
"j:" -> (arg => parallel_jobs = Value.Int.parse(arg)),
"l" -> (_ => build_library = true),
"o:" -> (arg => options = options + arg),
"p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)),
"r:" -> (arg => rev = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val progress = new Console_Progress()
-
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
- build_release(options, target_dir = target_dir, components_base = components_base,
- progress = progress, rev = rev, afp_rev = afp_rev,
- proper_release_name = proper_release_name, website = website,
- platform_families =
- if (platform_families.isEmpty) default_platform_families
- else platform_families,
+ def make_context(name: String): Release_Context =
+ Release_Context(target_dir,
+ release_name = name,
+ components_base = components_base,
+ progress = new Console_Progress())
+
+ val context =
+ if (source_archive.isEmpty) {
+ val context = make_context(release_name)
+ val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip"
+ build_release_archive(context, version, parallel_jobs = parallel_jobs)
+ context
+ }
+ else {
+ val archive = Release_Archive.get(source_archive, rename = release_name)
+ val context = make_context(archive.identifier)
+ Isabelle_System.new_directory(context.dist_dir)
+ use_release_archive(context, archive, id = rev)
+ context
+ }
+
+ build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
more_components = more_components, build_sessions = build_sessions,
- build_library = build_library, parallel_jobs = parallel_jobs)
+ build_library = build_library, parallel_jobs = parallel_jobs, website = website)
}
}
}
diff --git a/src/Pure/Admin/isabelle_cronjob.scala b/src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala
+++ b/src/Pure/Admin/isabelle_cronjob.scala
@@ -1,634 +1,634 @@
/* Title: Pure/Admin/isabelle_cronjob.scala
Author: Makarius
Main entry point for administrative cronjob at TUM.
*/
package isabelle
import java.nio.file.Files
import scala.annotation.tailrec
object Isabelle_Cronjob
{
/* global resources: owned by main cronjob */
val backup = "lxbroy10:cronjob"
val main_dir: Path = Path.explode("~/cronjob")
val main_state_file: Path = main_dir + Path.explode("run/main.state")
val current_log: Path = main_dir + Path.explode("run/main.log") // owned by log service
val cumulative_log: Path = main_dir + Path.explode("log/main.log") // owned by log service
val isabelle_repos: Path = main_dir + Path.explode("isabelle")
val afp_repos: Path = main_dir + Path.explode("AFP")
val mailman_archives_dir = Path.explode("~/cronjob/Mailman")
val build_log_dirs =
List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
/** logger tasks **/
sealed case class Logger_Task(name: String = "", body: Logger => Unit)
/* init and exit */
def get_rev(): String = Mercurial.repository(isabelle_repos).id()
def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
val init: Logger_Task =
Logger_Task("init", logger =>
{
Isabelle_Devel.make_index()
Mercurial.setup_repository(Isabelle_System.isabelle_repository.root, isabelle_repos)
Mercurial.setup_repository(Isabelle_System.afp_repository.root, afp_repos)
File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev())))
Isabelle_System.bash(
"""rsync -a --include="*/" --include="plain_identify*" --exclude="*" """ +
Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
if (!Isabelle_Devel.cronjob_log.is_file)
Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath)
})
val exit: Logger_Task =
Logger_Task("exit", logger =>
{
Isabelle_System.bash(
"rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.")
.check
})
/* Mailman archives */
val mailman_archives: Logger_Task =
Logger_Task("mailman_archives", logger =>
{
Mailman.isabelle_users.download(mailman_archives_dir)
Mailman.isabelle_dev.download(mailman_archives_dir)
})
/* build release */
val build_release: Logger_Task =
Logger_Task("build_release", logger =>
{
- Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev())
+ Isabelle_Devel.release_snapshot(logger.options, get_rev(), get_afp_rev())
})
/* remote build_history */
sealed case class Item(
known: Boolean,
isabelle_version: String,
afp_version: Option[String],
pull_date: Date)
{
def unknown: Boolean = !known
def versions: (String, Option[String]) = (isabelle_version, afp_version)
def known_versions(rev: String, afp_rev: Option[String]): Boolean =
known && rev != "" && isabelle_version == rev &&
(afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev)
}
def recent_items(db: SQL.Database,
days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] =
{
val afp = afp_rev.isDefined
val select =
Build_Log.Data.select_recent_versions(
days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(res =>
{
val known = res.bool(Build_Log.Data.known)
val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
val pull_date = res.date(Build_Log.Data.pull_date(afp))
Item(known, isabelle_version, afp_version, pull_date)
}).toList)
}
def unknown_runs(items: List[Item]): List[List[Item]] =
{
val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
if (run.nonEmpty) run :: unknown_runs(rest) else Nil
}
sealed case class Remote_Build(
description: String,
host: String,
actual_host: String = "",
user: String = "",
port: Int = 0,
proxy_host: String = "",
proxy_user: String = "",
proxy_port: Int = 0,
self_update: Boolean = false,
historic: Boolean = false,
history: Int = 0,
history_base: String = "build_history_base",
java_heap: String = "",
options: String = "",
args: String = "",
afp: Boolean = false,
bulky: Boolean = false,
more_hosts: List[String] = Nil,
detect: SQL.Source = "",
active: Boolean = true)
{
def ssh_session(context: SSH.Context): SSH.Session =
context.open_session(host = host, user = user, port = port, actual_host = actual_host,
proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
permissive = proxy_host.nonEmpty)
def sql: SQL.Source =
Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_History.engine) + " AND " +
SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
(if (detect == "") "" else " AND " + SQL.enclose(detect))
def profile: Build_Status.Profile =
Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
def pick(
options: Options,
rev: String = "",
filter: Item => Boolean = _ => true): Option[(String, Option[String])] =
{
val afp_rev = if (afp) Some(get_afp_rev()) else None
val store = Build_Log.store(options)
using(store.open_database())(db =>
{
def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =
{
val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
def runs = unknown_runs(items).filter(run => run.length >= gap)
if (historic || items.exists(_.known_versions(rev, afp_rev))) {
val longest_run =
runs.foldLeft(List.empty[Item]) {
case (item1, item2) => if (item1.length >= item2.length) item1 else item2
}
if (longest_run.isEmpty) None
else Some(longest_run(longest_run.length / 2).versions)
}
else if (rev != "") Some((rev, afp_rev))
else runs.flatten.headOption.map(_.versions)
}
pick_days(options.int("build_log_history") max history, 2) orElse
pick_days(200, 5) orElse
pick_days(2000, 1)
})
}
def build_history_options: String =
" -h " + Bash.string(host) + " " +
(java_heap match {
case "" => ""
case h =>
"-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + h + "\"' "
}) + options
}
val remote_builds_old: List[Remote_Build] =
List(
Remote_Build("Linux A", "lxbroy9",
java_heap = "2g", options = "-m32 -B -M1x2,2", args = "-N -g timing"),
Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90,
java_heap = "2g",
options = "-m32 -B -M1x2,2 -t Benchmarks" +
" -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
" -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_SMLNJ=sml" +
" -e ISABELLE_SWIPL=swipl",
args = "-N -a -d '~~/src/Benchmarks'",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("Benchmarks")),
Remote_Build("macOS 10.14 Mojave (Old)", "lapnipkow3",
options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
self_update = true, args = "-a -d '~~/src/Benchmarks'"),
Remote_Build("AFP old bulky", "lrzcloud1", self_update = true,
proxy_host = "lxbroy10", proxy_user = "i21isatest",
options = "-m64 -M6 -U30000 -s10 -t AFP",
args = "-g large -g slow",
afp = true,
bulky = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
Remote_Build("AFP old", "lxbroy7",
args = "-N -X large -X slow",
afp = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
history_base = "37074e22e8be",
options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
args = "-N -g timing",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7") + " AND " +
Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")),
Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8",
history_base = "a9d5b59c3e12",
options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
args = "-N -g timing",
detect =
Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
Remote_Build("Poly/ML 5.7 macOS", "macbroy2",
history_base = "37074e22e8be",
options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
args = "-a",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7")),
Remote_Build("Poly/ML 5.7.1 macOS", "macbroy2",
history_base = "a9d5b59c3e12",
options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
args = "-a",
detect =
Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
Remote_Build("macOS", "macbroy2",
options = "-m32 -M8" +
" -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
" -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_OPAM_ROOT=\"$ISABELLE_HOME/opam\"" +
" -e ISABELLE_SMLNJ=/home/isabelle/smlnj/110.85/bin/sml" +
" -p pide_session=false",
args = "-a",
detect = Build_Log.Prop.build_tags.undefined,
history_base = "2c0f24e927dd"),
Remote_Build("macOS, quick_and_dirty", "macbroy2",
options = "-m32 -M8 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty"),
history_base = "2c0f24e927dd"),
Remote_Build("macOS, skip_proofs", "macbroy2",
options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"),
history_base = "2c0f24e927dd"),
Remote_Build("Poly/ML test", "lxbroy8",
options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
args = "-N -g timing",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("polyml-test")),
Remote_Build("macOS 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a",
detect = Build_Log.Prop.build_start.toString + " > date '2017-03-03'"),
Remote_Build("macOS 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a"),
Remote_Build("macOS 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
detect = Build_Log.Prop.build_start.toString + " < date '2017-03-03'")) :::
{
for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
yield {
Remote_Build("AFP old", host = hosts.head, more_hosts = hosts.tail,
options = "-m32 -M1x2 -t AFP -P" + n +
" -e ISABELLE_GHC=ghc" +
" -e ISABELLE_MLTON=mlton" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
" -e ISABELLE_SMLNJ=sml",
args = "-N -X large -X slow",
afp = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"))
}
}
val remote_builds1: List[List[Remote_Build]] =
{
List(
List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
List(Remote_Build("macOS 10.13 High Sierra", "lapbroy68",
options = "-m32 -B -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
self_update = true, args = "-a -d '~~/src/Benchmarks'")),
List(
Remote_Build("macOS 11.1 Big Sur", "mini1",
options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_MLTON=/usr/local/bin/mlton" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
" -e ISABELLE_SWIPL=/usr/local/bin/swipl",
self_update = true, args = "-a -d '~~/src/Benchmarks'")),
List(
Remote_Build("macOS 10.14 Mojave", "mini2",
options = "-m32 -B -M1x2,2,4 -p pide_session=false" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_MLTON=/usr/local/bin/mlton" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
" -e ISABELLE_SWIPL=/usr/local/bin/swipl",
self_update = true, args = "-a -d '~~/src/Benchmarks'"),
Remote_Build("macOS, quick_and_dirty", "mini2",
options = "-m32 -M4 -t quick_and_dirty -p pide_session=false",
self_update = true, args = "-a -o quick_and_dirty",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("quick_and_dirty")),
Remote_Build("macOS, skip_proofs", "mini2",
options = "-m32 -M4 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("skip_proofs"))),
List(Remote_Build("macOS 10.15 Catalina", "laramac01", user = "makarius",
proxy_host = "laraserver", proxy_user = "makarius",
self_update = true,
options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
args = "-a -d '~~/src/Benchmarks'")),
List(
Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
options = "-m32 -M4" +
" -C /cygdrive/d/isatest/contrib" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
args = "-a",
detect =
Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86-windows") + " OR " +
Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64_32-windows")),
Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
options = "-m64 -M4" +
" -C /cygdrive/d/isatest/contrib" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
args = "-a",
detect = Build_Log.Settings.ML_PLATFORM.toString + " = " + SQL.string("x86_64-windows"))))
}
val remote_builds2: List[List[Remote_Build]] =
List(
List(
Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true,
proxy_host = "lxbroy10", proxy_user = "i21isatest",
java_heap = "8g",
options = "-m32 -M1x6 -t AFP" +
" -e ISABELLE_GHC=ghc" +
" -e ISABELLE_MLTON=mlton" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
" -e ISABELLE_SMLNJ=sml",
args = "-a -X large -X slow",
afp = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP")),
Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true,
proxy_host = "lxbroy10", proxy_user = "i21isatest",
java_heap = "8g",
options = "-m64 -M8 -U30000 -s10 -t AFP",
args = "-g large -g slow",
afp = true,
bulky = true,
detect = Build_Log.Prop.build_tags.toString + " = " + SQL.string("AFP"))))
def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build)
: Logger_Task =
{
val task_name = "build_history-" + r.host
Logger_Task(task_name, logger =>
{
using(r.ssh_session(logger.ssh_context))(ssh =>
{
val results =
Build_History.remote_build_history(ssh,
isabelle_repos,
isabelle_repos.ext(r.host),
isabelle_identifier = "cronjob_build_history",
self_update = r.self_update,
rev = rev,
afp_rev = afp_rev,
options =
" -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
" -R " + Bash.string(Components.default_component_repository) +
" -C '$USER_HOME/.isabelle/contrib' -f " +
r.build_history_options,
args = "-o timeout=10800 " + r.args)
for ((log_name, bytes) <- results) {
logger.log(Date.now(), log_name)
Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
}
})
})
}
val build_status_profiles: List[Build_Status.Profile] =
(remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile)
/** task logging **/
object Log_Service
{
def apply(options: Options, progress: Progress = new Progress): Log_Service =
new Log_Service(SSH.init_context(options), progress)
}
class Log_Service private(val ssh_context: SSH.Context, progress: Progress)
{
current_log.file.delete
private val thread: Consumer_Thread[String] =
Consumer_Thread.fork("cronjob: logger", daemon = true)(
consume = (text: String) =>
{ // critical
File.append(current_log, text + "\n")
File.append(cumulative_log, text + "\n")
progress.echo(text)
true
})
def shutdown(): Unit = { thread.shutdown() }
val hostname: String = Isabelle_System.hostname()
def log(date: Date, task_name: String, msg: String): Unit =
if (task_name != "")
thread.send(
"[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
def start_logger(start_date: Date, task_name: String): Logger =
new Logger(this, start_date, task_name)
def run_task(start_date: Date, task: Logger_Task): Unit =
{
val logger = start_logger(start_date, task.name)
val res = Exn.capture { task.body(logger) }
val end_date = Date.now()
val err =
res match {
case Exn.Res(_) => None
case Exn.Exn(exn) =>
Output.writeln("Exception trace for " + quote(task.name) + ":")
exn.printStackTrace()
val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
Some(first_line)
}
logger.log_end(end_date, err)
}
def fork_task(start_date: Date, task: Logger_Task): Task =
new Task(task.name, run_task(start_date, task))
}
class Logger private[Isabelle_Cronjob](
val log_service: Log_Service, val start_date: Date, val task_name: String)
{
def ssh_context: SSH.Context = log_service.ssh_context
def options: Options = ssh_context.options
def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
def log_end(end_date: Date, err: Option[String]): Unit =
{
val elapsed_time = end_date.time - start_date.time
val msg =
(if (err.isEmpty) "finished" else "ERROR " + err.get) +
(if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)")
log(end_date, msg)
}
val log_dir = Isabelle_System.make_directory(main_dir + Build_Log.log_subdir(start_date))
log(start_date, "started")
}
class Task private[Isabelle_Cronjob](name: String, body: => Unit)
{
private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
def is_finished: Boolean = future.is_finished
}
/** cronjob **/
def cronjob(progress: Progress, exclude_task: Set[String]): Unit =
{
/* soft lock */
val still_running =
try { Some(File.read(main_state_file)) }
catch { case ERROR(_) => None }
still_running match {
case None | Some("") =>
case Some(running) =>
error("Isabelle cronjob appears to be still running: " + running)
}
/* log service */
val log_service = Log_Service(Options.init(), progress = progress)
def run(start_date: Date, task: Logger_Task): Unit = log_service.run_task(start_date, task)
def run_now(task: Logger_Task): Unit = run(Date.now(), task)
/* structured tasks */
def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
run_now(task))
def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
{
@tailrec def join(running: List[Task]): Unit =
{
running.partition(_.is_finished) match {
case (Nil, Nil) =>
case (Nil, _ :: _) => Time.seconds(0.5).sleep; join(running)
case (_ :: _, remaining) => join(remaining)
}
}
val start_date = Date.now()
val running =
for (task <- tasks if !exclude_task(task.name))
yield log_service.fork_task(start_date, task)
join(running)
})
/* repository structure */
val hg = Mercurial.repository(isabelle_repos)
val hg_graph = hg.graph()
def history_base_filter(r: Remote_Build): Item => Boolean =
{
val base_rev = hg.id(r.history_base)
val nodes = hg_graph.all_succs(List(base_rev)).toSet
(item: Item) => nodes(item.isabelle_version)
}
/* main */
val main_start_date = Date.now()
File.write(main_state_file, main_start_date.toString + " " + log_service.hostname)
run(main_start_date,
Logger_Task("isabelle_cronjob", logger =>
run_now(
SEQ(List(
init,
PAR(List(mailman_archives, build_release)),
PAR(
List(remote_builds1, remote_builds2).map(remote_builds =>
SEQ(List(
PAR(remote_builds.map(_.filter(_.active)).map(seq =>
SEQ(
for {
(r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
(rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
} yield remote_build_history(rev, afp_rev, i, r)))),
Logger_Task("jenkins_logs", _ =>
Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)),
Logger_Task("build_log_database",
logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)),
Logger_Task("build_status",
logger => Isabelle_Devel.build_status(logger.options)))))),
exit)))))
log_service.shutdown()
main_state_file.file.delete
}
/** command line entry point **/
def main(args: Array[String]): Unit =
{
Command_Line.tool {
var force = false
var verbose = false
var exclude_task = Set.empty[String]
val getopts = Getopts("""
Usage: Admin/cronjob/main [OPTIONS]
Options are:
-f apply force to do anything
-v verbose
-x NAME exclude tasks with this name
""",
"f" -> (_ => force = true),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_task += arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = if (verbose) new Console_Progress() else new Progress
if (force) cronjob(progress, exclude_task)
else error("Need to apply force to do anything")
}
}
}
diff --git a/src/Pure/Admin/isabelle_devel.scala b/src/Pure/Admin/isabelle_devel.scala
--- a/src/Pure/Admin/isabelle_devel.scala
+++ b/src/Pure/Admin/isabelle_devel.scala
@@ -1,78 +1,75 @@
/* Title: Pure/Admin/isabelle_devel.scala
Author: Makarius
Website for Isabelle development resources.
*/
package isabelle
object Isabelle_Devel
{
val RELEASE_SNAPSHOT = "release_snapshot"
val BUILD_LOG_DB = "build_log.db"
val BUILD_STATUS = "build_status"
val CRONJOB_LOG = "cronjob-main.log"
val root: Path = Path.explode("~/html-data/devel")
val cronjob_log: Path = root + Path.basic(CRONJOB_LOG)
/* index */
def make_index(): Unit =
{
val redirect = "https://isabelle-dev.sketis.net/home/menu/view/20"
HTML.write_document(root, "index.html",
List(
XML.Elem(Markup("meta",
List("http-equiv" -> "Refresh", "content" -> ("0; url=" + redirect))), Nil)),
List(HTML.link(redirect, HTML.text("Isabelle Development Resources"))))
}
/* release snapshot */
- def release_snapshot(
- options: Options,
- rev: String = "",
- afp_rev: String = "",
- parallel_jobs: Int = 1): Unit =
+ def release_snapshot(options: Options, rev: String, afp_rev: String): Unit =
{
Isabelle_System.with_tmp_dir("isadist")(target_dir =>
{
Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
website_dir =>
- Build_Release.build_release(options, target_dir = target_dir,
- rev = rev,
- afp_rev = afp_rev,
- parallel_jobs = parallel_jobs,
- build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
- website = Some(website_dir)))
+ {
+ val context = Build_Release.Release_Context(target_dir)
+ Build_Release.build_release_archive(context, rev)
+ Build_Release.build_release(options, context, afp_rev = afp_rev,
+ build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
+ website = Some(website_dir))
+ })
})
}
/* maintain build_log database */
def build_log_database(options: Options, log_dirs: List[Path]): Unit =
{
val store = Build_Log.store(options)
using(store.open_database())(db =>
{
store.update_database(db, log_dirs)
store.update_database(db, log_dirs, ml_statistics = true)
store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB))
})
}
/* present build status */
def build_status(options: Options): Unit =
{
Isabelle_System.update_directory(root + Path.explode(BUILD_STATUS),
dir => Build_Status.build_status(options, target_dir = dir, ml_statistics = true))
}
}
diff --git a/src/Pure/Admin/other_isabelle.scala b/src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala
+++ b/src/Pure/Admin/other_isabelle.scala
@@ -1,120 +1,134 @@
/* Title: Pure/Admin/other_isabelle.scala
Author: Makarius
Manage other Isabelle distributions.
*/
package isabelle
object Other_Isabelle
{
def apply(isabelle_home: Path,
isabelle_identifier: String = "",
user_home: Path = Path.USER_HOME,
progress: Progress = new Progress): Other_Isabelle =
new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
}
class Other_Isabelle(
val isabelle_home: Path,
val isabelle_identifier: String,
user_home: Path,
progress: Progress)
{
other_isabelle =>
override def toString: String = isabelle_home.toString
if (proper_string(System.getenv("ISABELLE_SETTINGS_PRESENT")).isDefined)
error("Cannot initialize with enclosing ISABELLE_SETTINGS_PRESENT")
/* static system */
def bash(
script: String,
redirect: Boolean = false,
echo: Boolean = false,
strict: Boolean = true): Process_Result =
progress.bash(
"export USER_HOME=" + File.bash_path(user_home) + "\n" +
Isabelle_System.export_isabelle_identifier(isabelle_identifier) + script,
env = null, cwd = isabelle_home.file, redirect = redirect, echo = echo, strict = strict)
def apply(
cmdline: String,
redirect: Boolean = false,
echo: Boolean = false,
strict: Boolean = true): Process_Result =
bash("bin/isabelle " + cmdline, redirect = redirect, echo = echo, strict = strict)
def resolve_components(echo: Boolean): Unit =
other_isabelle(
"env ISABELLE_TOOLS=" + Bash.string(Isabelle_System.getenv("ISABELLE_TOOLS")) +
" isabelle components -a", redirect = true, echo = echo).check
def getenv(name: String): String =
other_isabelle("getenv -b " + Bash.string(name)).check.out
val isabelle_home_user: Path = Path.explode(getenv("ISABELLE_HOME_USER"))
val etc: Path = isabelle_home_user + Path.explode("etc")
val etc_settings: Path = etc + Path.explode("settings")
val etc_preferences: Path = etc + Path.explode("preferences")
- def copy_fonts(target_dir: Path): Unit =
+
+ /* NEWS */
+
+ def make_news(): Unit =
+ {
+ val doc_dir = isabelle_home + Path.explode("doc")
+ val fonts_dir = Isabelle_System.make_directory(doc_dir + Path.explode("fonts"))
+
Isabelle_Fonts.make_entries(getenv = getenv, hidden = true).
- foreach(entry => Isabelle_System.copy_file(entry.path, target_dir))
+ foreach(entry => Isabelle_System.copy_file(entry.path, fonts_dir))
+
+ HTML.write_document(doc_dir, "NEWS.html",
+ List(HTML.title("NEWS")),
+ List(
+ HTML.chapter("NEWS"),
+ HTML.source(Symbol.decode(File.read(isabelle_home + Path.explode("NEWS"))))))
+ }
/* components */
def init_components(
component_repository: String = Components.default_component_repository,
components_base: Path = Components.default_components_base,
catalogs: List[String] = Nil,
components: List[String] = Nil): List[String] =
{
val dir = Components.admin(isabelle_home)
("ISABELLE_COMPONENT_REPOSITORY=" + Bash.string(component_repository)) ::
catalogs.map(name =>
"init_components " + File.bash_path(components_base) + " " +
File.bash_path(dir + Path.basic(name))) :::
components.map(name =>
"init_component " + File.bash_path(components_base + Path.basic(name)))
}
/* settings */
def clean_settings(): Boolean =
if (!etc_settings.is_file) true
else if (File.read(etc_settings).startsWith("# generated by Isabelle")) {
etc_settings.file.delete; true
}
else false
def init_settings(settings: List[String]): Unit =
{
if (!clean_settings())
error("Cannot proceed with existing user settings file: " + etc_settings)
Isabelle_System.make_directory(etc_settings.dir)
File.write(etc_settings,
"# generated by Isabelle " + Date.now() + "\n" +
"#-*- shell-script -*- :mode=shellscript:\n" +
settings.mkString("\n", "\n", "\n"))
}
/* cleanup */
def cleanup(): Unit =
{
clean_settings()
etc.file.delete
isabelle_home_user.file.delete
}
}
diff --git a/src/Pure/General/file.scala b/src/Pure/General/file.scala
--- a/src/Pure/General/file.scala
+++ b/src/Pure/General/file.scala
@@ -1,328 +1,334 @@
/* Title: Pure/General/file.scala
Author: Makarius
File-system operations.
*/
package isabelle
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
InputStreamReader, File => JFile, IOException}
import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
FileVisitOption, FileVisitResult}
import java.nio.file.attribute.BasicFileAttributes
import java.net.{URL, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
import java.util.regex.Pattern
import java.util.EnumSet
import org.tukaani.xz.{XZInputStream, XZOutputStream}
import scala.collection.mutable
import scala.util.matching.Regex
object File
{
/* standard path (Cygwin or Posix) */
def standard_path(path: Path): String = path.expand.implode
def standard_path(platform_path: String): String =
if (Platform.is_windows) {
val Platform_Root = new Regex("(?i)" +
Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
platform_path.replace('/', '\\') match {
case Platform_Root(rest) => "/" + rest.replace('\\', '/')
case Drive(letter, rest) =>
"/cygdrive/" + Word.lowercase(letter) +
(if (rest == "") "" else "/" + rest.replace('\\', '/'))
case path => path.replace('\\', '/')
}
}
else platform_path
def standard_path(file: JFile): String = standard_path(file.getPath)
def standard_url(name: String): String =
try {
val url = new URL(name)
if (url.getProtocol == "file" && Url.is_wellformed_file(name))
standard_path(Url.parse_file(name))
else name
}
catch { case _: MalformedURLException => standard_path(name) }
/* platform path (Windows or Posix) */
private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
private val Named_Root = new Regex("//+([^/]*)(.*)")
def platform_path(standard_path: String): String =
if (Platform.is_windows) {
val result_path = new StringBuilder
val rest =
standard_path match {
case Cygdrive(drive, rest) =>
result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
rest
case Named_Root(root, rest) =>
result_path ++= JFile.separator
result_path ++= JFile.separator
result_path ++= root
rest
case path if path.startsWith("/") =>
result_path ++= Isabelle_System.cygwin_root()
path
case path => path
}
for (p <- space_explode('/', rest) if p != "") {
val len = result_path.length
if (len > 0 && result_path(len - 1) != JFile.separatorChar)
result_path += JFile.separatorChar
result_path ++= p
}
result_path.toString
}
else standard_path
def platform_path(path: Path): String = platform_path(standard_path(path))
def platform_file(path: Path): JFile = new JFile(platform_path(path))
/* platform files */
def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile
def absolute_name(file: JFile): String = absolute(file).getPath
def canonical(file: JFile): JFile = file.getCanonicalFile
def canonical_name(file: JFile): String = canonical(file).getPath
def path(file: JFile): Path = Path.explode(standard_path(file))
def pwd(): Path = path(Path.current.absolute_file)
/* relative paths */
def relative_path(base: Path, other: Path): Option[Path] =
{
val base_path = base.file.toPath
val other_path = other.file.toPath
if (other_path.startsWith(base_path))
Some(path(base_path.relativize(other_path).toFile))
else None
}
/* bash path */
def bash_path(path: Path): String = Bash.string(standard_path(path))
def bash_path(file: JFile): String = Bash.string(standard_path(file))
def bash_platform_path(path: Path): String = Bash.string(platform_path(path))
/* directory entries */
def check_dir(path: Path): Path =
if (path.is_dir) path else error("No such directory: " + path)
def check_file(path: Path): Path =
if (path.is_file) path else error("No such file: " + path)
/* directory content */
def read_dir(dir: Path): List[String] =
{
if (!dir.is_dir) error("No such directory: " + dir.toString)
val files = dir.file.listFiles
if (files == null) Nil
else files.toList.map(_.getName).sorted
}
def get_dir(dir: Path): String =
read_dir(dir).filter(name => (dir + Path.basic(name)).is_dir) match {
case List(entry) => entry
case dirs =>
error("Exactly one directory entry expected: " + commas_quote(dirs.sorted))
}
def find_files(
start: JFile,
pred: JFile => Boolean = _ => true,
include_dirs: Boolean = false,
follow_links: Boolean = false): List[JFile] =
{
val result = new mutable.ListBuffer[JFile]
def check(file: JFile): Unit = if (pred(file)) result += file
if (start.isFile) check(start)
else if (start.isDirectory) {
val options =
if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS)
else EnumSet.noneOf(classOf[FileVisitOption])
Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE,
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 (include_dirs || !file.isDirectory) check(file)
FileVisitResult.CONTINUE
}
}
)
}
result.toList
}
/* read */
def read(file: JFile): String = Bytes.read(file).text
def read(path: Path): String = read(path.file)
def read_stream(reader: BufferedReader): String =
{
val output = new StringBuilder(100)
var c = -1
while ({ c = reader.read; c != -1 }) output += c.toChar
reader.close()
output.toString
}
def read_stream(stream: InputStream): String =
read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
def read_gzip(file: JFile): String =
read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
def read_gzip(path: Path): String = read_gzip(path.file)
def read_xz(file: JFile): String =
read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
def read_xz(path: Path): String = read_xz(path.file)
/* read lines */
def read_line(reader: BufferedReader): Option[String] =
{
val line =
try { reader.readLine}
catch { case _: IOException => null }
Option(line).map(Library.trim_line)
}
def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
{
val result = new mutable.ListBuffer[String]
var line: Option[String] = None
while ({ line = read_line(reader); line.isDefined }) {
progress(line.get)
result += line.get
}
reader.close()
result.toList
}
/* write */
def writer(file: JFile): BufferedWriter =
new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset))
def write_file(
file: JFile, text: String, make_stream: OutputStream => OutputStream): Unit =
{
val stream = make_stream(new FileOutputStream(file))
using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text))
}
def write(file: JFile, text: String): Unit = write_file(file, text, s => s)
def write(path: Path, text: String): Unit = write(path.file, text)
def write_gzip(file: JFile, text: String): Unit =
write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
def write_gzip(path: Path, text: String): Unit = write_gzip(path.file, text)
def write_xz(file: JFile, text: String, options: XZ.Options): Unit =
File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options))
def write_xz(file: JFile, text: String): Unit = write_xz(file, text, XZ.options())
def write_xz(path: Path, text: String, options: XZ.Options): Unit =
write_xz(path.file, text, options)
def write_xz(path: Path, text: String): Unit = write_xz(path, text, XZ.options())
def write_backup(path: Path, text: String): Unit =
{
if (path.is_file) Isabelle_System.move_file(path, path.backup)
write(path, text)
}
def write_backup2(path: Path, text: String): Unit =
{
if (path.is_file) Isabelle_System.move_file(path, path.backup2)
write(path, text)
}
/* change */
- def change(file: JFile, f: String => String): Unit = write(file, f(read(file)))
- def change(path: Path, f: String => String): Unit = write(path, f(read(path)))
+ def change(file: JFile, f: String => String): Unit =
+ {
+ val x = read(file)
+ val y = f(x)
+ if (x != y) write(file, y)
+ }
+
+ def change(path: Path, f: String => String): Unit = change(path.file, f)
/* append */
def append(file: JFile, text: String): Unit =
- Files.write(file.toPath, UTF8.bytes(text.toString),
+ Files.write(file.toPath, UTF8.bytes(text),
StandardOpenOption.APPEND, StandardOpenOption.CREATE)
def append(path: Path, text: String): Unit = append(path.file, text)
/* eq */
def eq(file1: JFile, file2: JFile): Boolean =
try { Files.isSameFile(file1.toPath, file2.toPath) }
catch { case ERROR(_) => false }
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)
/* permissions */
def is_executable(path: Path): Boolean =
{
if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok
else path.file.canExecute
}
def set_executable(path: Path, flag: Boolean): Unit =
{
if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path)
else if (Platform.is_windows) Isabelle_System.chmod("a-x", path)
else path.file.setExecutable(flag, false)
}
}
diff --git a/src/Pure/General/mercurial.scala b/src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala
+++ b/src/Pure/General/mercurial.scala
@@ -1,438 +1,438 @@
/* Title: Pure/General/mercurial.scala
Author: Makarius
Support for Mercurial repositories, with local or remote repository clone
and working directory (via ssh connection).
*/
package isabelle
import scala.annotation.tailrec
import scala.collection.mutable
object Mercurial
{
type Graph = isabelle.Graph[String, Unit]
/* HTTP server */
object Server
{
def apply(root: String): Server = new Server(root)
def start(root: Path): Server =
{
val hg = repository(root)
val server_process = Future.promise[Bash.Process]
val server_root = Future.promise[String]
Isabelle_Thread.fork("hg") {
val process =
Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) }
server_process.fulfill_result(process)
Exn.release(process).result(progress_stdout =
line => if (!server_root.is_finished) {
server_root.fulfill(Library.try_unsuffix("/", line).getOrElse(line))
})
}
server_process.join
new Server(server_root.join) {
override def close(): Unit = server_process.join.terminate()
}
}
}
class Server private(val root: String) extends AutoCloseable
{
override def toString: String = root
def close(): Unit = ()
def changeset(rev: String = "tip", raw: Boolean = false): String =
root + (if (raw) "/raw-rev/" else "/rev/") + rev
def file(path: Path, rev: String = "tip", raw: Boolean = false): String =
root + (if (raw) "/raw-file/" else "/file/") + rev + "/" + path.expand.implode
def archive(rev: String = "tip"): String =
root + "/archive/" + rev + ".tar.gz"
def read_changeset(rev: String = "tip"): String =
Url.read(changeset(rev = rev, raw = true))
def read_file(path: Path, rev: String = "tip"): String =
Url.read(file(path, rev = rev, raw = true))
def download_archive(rev: String = "tip", progress: Progress = new Progress): HTTP.Content =
Isabelle_System.download(archive(rev = rev), progress = progress)
def download_dir(dir: Path, rev: String = "tip", progress: Progress = new Progress): Unit =
{
Isabelle_System.new_directory(dir)
Isabelle_System.with_tmp_file("rev", ext = ".tar.gz")(archive_path =>
{
val content = download_archive(rev = rev, progress = progress)
Bytes.write(archive_path, content.bytes)
progress.echo("Unpacking " + rev + ".tar.gz")
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path) + " --strip-components=1",
- dir = dir, original_owner = true).check
+ Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
+ dir = dir, original_owner = true, strip = 1).check
})
}
}
/* command-line syntax */
def optional(s: String, prefix: String = ""): String =
if (s == "") "" else " " + prefix + " " + Bash.string(s)
def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
def opt_rev(s: String): String = optional(s, "--rev")
def opt_template(s: String): String = optional(s, "--template")
/* repository archives */
private val Archive_Node = """^node: (\S{12}).*$""".r
private val Archive_Tag = """^tag: (\S+).*$""".r
sealed case class Archive_Info(lines: List[String])
{
def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a })
def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag
}
def archive_info(root: Path): Option[Archive_Info] =
{
val path = root + Path.explode(".hg_archival.txt")
if (path.is_file) Some(Archive_Info(Library.trim_split_lines(File.read(path)))) else None
}
def archive_id(root: Path): Option[String] =
archive_info(root).flatMap(_.id)
def archive_tags(root: Path): Option[String] =
archive_info(root).map(info => info.tags.mkString(" "))
/* repository access */
def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =
ssh.is_dir(root + Path.explode(".hg")) &&
new Repository(root, ssh).command("root").ok
def repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
{
val hg = new Repository(root, ssh)
hg.command("root").check
hg
}
def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
{
@tailrec def find(root: Path): Option[Repository] =
if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
else if (root.is_root) None
else find(root + Path.parent)
find(ssh.expand_path(start))
}
private def make_repository(root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local)
: Repository =
{
val hg = new Repository(root, ssh)
ssh.make_directory(hg.root.dir)
hg.command(cmd, args, repository = false).check
hg
}
def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
make_repository(root, "init", ssh.bash_path(root), ssh = ssh)
def clone_repository(source: String, root: Path,
rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
make_repository(root, "clone",
options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
{
if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
else clone_repository(source, root, options = "--noupdate", ssh = ssh)
}
class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local)
{
hg =>
val root: Path = ssh.expand_path(root_path)
def root_url: String = ssh.hg_url + root.implode
override def toString: String = ssh.hg_url + root.implode
def command_line(name: String, args: String = "", options: String = "",
repository: Boolean = true): String =
{
"export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
(if (repository) " --repository " + ssh.bash_path(root) else "") +
" --noninteractive " + name + " " + options + " " + args
}
def command(
name: String, args: String = "", options: String = "",
repository: Boolean = true): Process_Result =
{
ssh.execute(command_line(name, args = args, options = options, repository = repository))
}
def add(files: List[Path]): Unit =
hg.command("add", files.map(ssh.bash_path).mkString(" "))
def archive(target: String, rev: String = "", options: String = ""): Unit =
hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
hg.command("heads", opt_template(template), options).check.out_lines
def identify(rev: String = "tip", options: String = ""): String =
hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
def id(rev: String = "tip"): String = identify(rev, options = "-i")
def tags(rev: String = "tip"): String =
{
val result = identify(rev, options = "-t")
Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
}
def paths(args: String = "", options: String = ""): List[String] =
hg.command("paths", args = args, options = options).check.out_lines
def manifest(rev: String = "", options: String = ""): List[String] =
hg.command("manifest", opt_rev(rev), options).check.out_lines
def log(rev: String = "", template: String = "", options: String = ""): String =
hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
def parent(): String = log(rev = "p1()", template = "{node|short}")
def push(
remote: String = "", rev: String = "", force: Boolean = false, options: String = ""): Unit =
{
hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
check_rc(rc => rc == 0 | rc == 1)
}
def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
hg.command("pull", opt_rev(rev) + optional(remote), options).check
def update(
rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = ""): Unit =
{
hg.command("update",
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
}
def known_files(): List[String] =
hg.command("status", options = "--modified --added --clean --no-status").check.out_lines
def graph(): Graph =
{
val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
val log_result =
log(template = """node: {node|short} {p1node|short} {p2node|short}\n""")
split_lines(log_result).foldLeft(Graph.string[Unit]) {
case (graph, Node(x, y, z)) =>
val deps = List(y, z).filterNot(s => s.forall(_ == '0'))
val graph1 = (x :: deps).foldLeft(graph)(_.default_node(_, ()))
deps.foldLeft(graph1)({ case (g, dep) => g.add_edge(dep, x) })
case (graph, _) => graph
}
}
}
/* check files */
def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) =
{
val outside = new mutable.ListBuffer[Path]
val unknown = new mutable.ListBuffer[Path]
@tailrec def check(paths: List[Path]): Unit =
{
paths match {
case path :: rest =>
find_repository(path, ssh) match {
case None => outside += path; check(rest)
case Some(hg) =>
val known =
hg.known_files().iterator.map(name =>
(hg.root + Path.explode(name)).canonical_file).toSet
if (!known(path.canonical_file)) unknown += path
check(rest.filterNot(p => known(p.canonical_file)))
}
case Nil =>
}
}
check(files)
(outside.toList, unknown.toList)
}
/* setup remote vs. local repository */
private def edit_hgrc(local_hg: Repository, path_name: String, source: String): Unit =
{
val hgrc = local_hg.root + Path.explode(".hg/hgrc")
def header(line: String): Boolean = line.startsWith("[paths]")
val Entry = """^(\S+)\s*=\s*(.*)$""".r
val new_entry = path_name + " = " + source
def commit(lines: List[String]): Boolean =
{
File.write(hgrc, cat_lines(lines))
true
}
val edited =
hgrc.is_file && {
val lines = split_lines(File.read(hgrc))
lines.count(header) == 1 && {
if (local_hg.paths(options = "-q").contains(path_name)) {
val old_source = local_hg.paths(args = path_name).head
val old_entry = path_name + ".old = " + old_source
val lines1 =
lines.map {
case Entry(a, b) if a == path_name && b == old_source =>
new_entry + "\n" + old_entry
case line => line
}
lines != lines1 && commit(lines1)
}
else {
val prefix = lines.takeWhile(line => !header(line))
val n = prefix.length
commit(prefix ::: List(lines(n), new_entry) ::: lines.drop(n + 1))
}
}
}
if (!edited) File.append(hgrc, "\n[paths]\n" + new_entry + "\n")
}
val default_path_name = "default"
def hg_setup(
remote: String,
local_path: Path,
remote_name: String = "",
path_name: String = default_path_name,
remote_exists: Boolean = false,
progress: Progress = new Progress): Unit =
{
/* local repository */
Isabelle_System.make_directory(local_path)
val repos_name =
proper_string(remote_name) getOrElse local_path.absolute.base.implode
val local_hg =
if (is_repository(local_path)) repository(local_path)
else init_repository(local_path)
progress.echo("Local repository " + local_hg.root.absolute)
/* remote repository */
val remote_url =
remote match {
case _ if remote.startsWith("ssh://") =>
val ssh_url = remote + "/" + repos_name
if (!remote_exists) {
try { local_hg.command("init", ssh_url, repository = false).check }
catch { case ERROR(msg) => progress.echo_warning(msg) }
}
ssh_url
case SSH.Target(user, host) =>
val phabricator = Phabricator.API(user, host)
var repos =
phabricator.get_repositories().find(r => r.short_name == repos_name) getOrElse {
if (remote_exists) {
error("Remote repository " +
quote(phabricator.hg_url + "/source/" + repos_name) + " expected to exist")
}
else phabricator.create_repository(repos_name, short_name = repos_name)
}
while (repos.importing) {
progress.echo("Awaiting remote repository ...")
Time.seconds(0.5).sleep
repos = phabricator.the_repository(repos.phid)
}
repos.ssh_url
case _ => error("Malformed remote specification " + quote(remote))
}
progress.echo("Remote repository " + quote(remote_url))
/* synchronize local and remote state */
progress.echo("Synchronizing ...")
edit_hgrc(local_hg, path_name, remote_url)
local_hg.pull(options = "-u")
local_hg.push(remote = remote_url)
}
val isabelle_tool =
Isabelle_Tool("hg_setup", "setup remote vs. local Mercurial repository",
Scala_Project.here, args =>
{
var remote_name = ""
var path_name = default_path_name
var remote_exists = false
val getopts = Getopts("""
Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR
Options are:
-n NAME remote repository name (default: base name of LOCAL_DIR)
-p PATH Mercurial path name (default: """ + quote(default_path_name) + """)
-r assume that remote repository already exists
Setup a remote vs. local Mercurial repository: REMOTE either refers to a
Phabricator server "user@host" or SSH file server "ssh://user@host/path".
""",
"n:" -> (arg => remote_name = arg),
"p:" -> (arg => path_name = arg),
"r" -> (_ => remote_exists = true))
val more_args = getopts(args)
val (remote, local_path) =
more_args match {
case List(arg1, arg2) => (arg1, Path.explode(arg2))
case _ => getopts.usage()
}
val progress = new Console_Progress
hg_setup(remote, local_path, remote_name = remote_name, path_name = path_name,
remote_exists = remote_exists, progress = progress)
})
}
diff --git a/src/Pure/General/path.scala b/src/Pure/General/path.scala
--- a/src/Pure/General/path.scala
+++ b/src/Pure/General/path.scala
@@ -1,309 +1,311 @@
/* Title: Pure/General/path.scala
Author: Makarius
Algebra of file-system paths: basic POSIX notation, extended by named
roots (e.g. //foo) and variables (e.g. $BAR).
*/
package isabelle
import java.io.{File => JFile}
import scala.util.matching.Regex
object Path
{
/* path elements */
sealed abstract class Elem
private case class Root(name: String) extends Elem
private case class Basic(name: String) extends Elem
private case class Variable(name: String) extends Elem
private case object Parent extends Elem
private def err_elem(msg: String, s: String): Nothing =
error(msg + " path element " + quote(s))
private val illegal_elem = Set("", "~", "~~", ".", "..")
private val illegal_char = "/\\$:\"'<>|?*"
private def check_elem(s: String): String =
if (illegal_elem.contains(s)) err_elem("Illegal", s)
else {
for (c <- s) {
if (c.toInt < 32)
err_elem("Illegal control character " + c.toInt + " in", s)
if (illegal_char.contains(c))
err_elem("Illegal character " + quote(c.toString) + " in", s)
}
s
}
private def root_elem(s: String): Elem = Root(check_elem(s))
private def basic_elem(s: String): Elem = Basic(check_elem(s))
private def variable_elem(s: String): Elem = Variable(check_elem(s))
private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] =
(y, xs) match {
case (Root(_), _) => List(y)
case (Parent, Root(_) :: _) => xs
case (Parent, Basic(_) :: rest) => rest
case _ => y :: xs
}
private def norm_elems(elems: List[Elem]): List[Elem] =
elems.foldRight(List.empty[Elem])(apply_elem)
private def implode_elem(elem: Elem, short: Boolean): String =
elem match {
case Root("") => ""
case Root(s) => "//" + s
case Basic(s) => s
case Variable("USER_HOME") if short => "~"
case Variable("ISABELLE_HOME") if short => "~~"
case Variable(s) => "$" + s
case Parent => ".."
}
private def squash_elem(elem: Elem): String =
elem match {
case Root("") => "ROOT"
case Root(s) => "SERVER_" + s
case Basic(s) => s
case Variable(s) => s
case Parent => "PARENT"
}
/* path constructors */
val current: Path = new Path(Nil)
val root: Path = new Path(List(Root("")))
def named_root(s: String): Path = new Path(List(root_elem(s)))
def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem))
def basic(s: String): Path = new Path(List(basic_elem(s)))
def variable(s: String): Path = new Path(List(variable_elem(s)))
val parent: Path = new Path(List(Parent))
val USER_HOME: Path = variable("USER_HOME")
val ISABELLE_HOME: Path = variable("ISABELLE_HOME")
/* explode */
def explode(str: String): Path =
{
def explode_elem(s: String): Elem =
try {
if (s == "..") Parent
else if (s == "~") Variable("USER_HOME")
else if (s == "~~") Variable("ISABELLE_HOME")
else if (s.startsWith("$")) variable_elem(s.substring(1))
else basic_elem(s)
}
catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) }
val ss = space_explode('/', str)
val r = ss.takeWhile(_.isEmpty).length
val es = ss.dropWhile(_.isEmpty)
val (roots, raw_elems) =
if (r == 0) (Nil, es)
else if (r == 1) (List(Root("")), es)
else if (es.isEmpty) (List(Root("")), Nil)
else (List(root_elem(es.head)), es.tail)
val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
new Path(norm_elems(elems reverse_::: roots))
}
def is_wellformed(str: String): Boolean =
try { explode(str); true } catch { case ERROR(_) => false }
def is_valid(str: String): Boolean =
try { explode(str).expand; true } catch { case ERROR(_) => false }
def split(str: String): List[Path] =
space_explode(':', str).filterNot(_.isEmpty).map(explode)
/* encode */
val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
/* reserved names */
private val reserved_windows: Set[String] =
Set("CON", "PRN", "AUX", "NUL",
"COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9",
"LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9")
def is_reserved(name: String): Boolean =
Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a)))
/* case-insensitive names */
def check_case_insensitive(paths: List[Path]): Unit =
{
val table =
paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) =>
val name = path.expand.implode
tab.insert(Word.lowercase(name), name)
}
val collisions =
(for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten
if (collisions.nonEmpty) {
error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n "))
}
}
}
final class Path private(protected val elems: List[Path.Elem]) // reversed elements
{
override def hashCode: Int = elems.hashCode
override def equals(that: Any): Boolean =
that match {
case other: Path => elems == other.elems
case _ => false
}
def is_current: Boolean = elems.isEmpty
def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }
def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic]
def +(other: Path): Path = new Path(other.elems.foldRight(elems)(Path.apply_elem))
/* implode */
private def gen_implode(short: Boolean): String =
elems match {
case Nil => "."
case List(Path.Root("")) => "/"
case _ => elems.map(Path.implode_elem(_, short)).reverse.mkString("/")
}
def implode: String = gen_implode(false)
def implode_short: String = gen_implode(true)
override def toString: String = quote(implode)
/* base element */
private def split_path: (Path, String) =
elems match {
case Path.Basic(s) :: xs => (new Path(xs), s)
case _ => error("Cannot split path into dir/base: " + toString)
}
def dir: Path = split_path._1
def base: Path = new Path(List(Path.Basic(split_path._2)))
def ext(e: String): Path =
if (e == "") this
else {
val (prfx, s) = split_path
prfx + Path.basic(s + "." + e)
}
def xz: Path = ext("xz")
def html: Path = ext("html")
def tex: Path = ext("tex")
def pdf: Path = ext("pdf")
def thy: Path = ext("thy")
+ def tar: Path = ext("tar")
+ def gz: Path = ext("gz")
def backup: Path =
{
val (prfx, s) = split_path
prfx + Path.basic(s + "~")
}
def backup2: Path =
{
val (prfx, s) = split_path
prfx + Path.basic(s + "~~")
}
def platform_exe: Path =
if (Platform.is_windows) ext("exe") else this
private val Ext = new Regex("(.*)\\.([^.]*)")
def split_ext: (Path, String) =
{
val (prefix, base) = split_path
base match {
case Ext(b, e) => (prefix + Path.basic(b), e)
case _ => (prefix + Path.basic(base), "")
}
}
def drop_ext: Path = split_ext._1
def get_ext: String = split_ext._2
def squash: Path = new Path(elems.map(elem => Path.Basic(Path.squash_elem(elem))))
/* expand */
def expand_env(env: Map[String, String]): Path =
{
def eval(elem: Path.Elem): List[Path.Elem] =
elem match {
case Path.Variable(s) =>
val path = Path.explode(Isabelle_System.getenv_strict(s, env))
if (path.elems.exists(_.isInstanceOf[Path.Variable]))
error("Illegal path variable nesting: " + s + "=" + path.toString)
else path.elems
case x => List(x)
}
new Path(Path.norm_elems(elems.flatMap(eval)))
}
def expand: Path = expand_env(Isabelle_System.settings())
def file_name: String = expand.base.implode
/* implode wrt. given directories */
def implode_symbolic: String =
{
val directories =
Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
val full_name = expand.implode
directories.view.flatMap(a =>
try {
val b = Path.explode(a).expand.implode
if (full_name == b) Some(a)
else {
Library.try_unprefix(b + "/", full_name) match {
case Some(name) => Some(a + "/" + name)
case None => None
}
}
} catch { case ERROR(_) => None }).headOption.getOrElse(implode)
}
def position: Position.T = Position.File(implode_symbolic)
/* platform files */
def file: JFile = File.platform_file(this)
def is_file: Boolean = file.isFile
def is_dir: Boolean = file.isDirectory
def absolute_file: JFile = File.absolute(file)
def canonical_file: JFile = File.canonical(file)
def absolute: Path = File.path(absolute_file)
def canonical: Path = File.path(canonical_file)
}
diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala
+++ b/src/Pure/System/isabelle_system.scala
@@ -1,633 +1,635 @@
/* Title: Pure/System/isabelle_system.scala
Author: Makarius
Fundamental Isabelle system environment: quasi-static module with
optional init operation.
*/
package isabelle
import java.io.{File => JFile, IOException}
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
import scala.jdk.CollectionConverters._
object Isabelle_System
{
/** bootstrap information **/
def jdk_home(): String =
{
val java_home = System.getProperty("java.home", "")
val home = new JFile(java_home)
val parent = home.getParent
if (home.getName == "jre" && parent != null &&
(new JFile(new JFile(parent, "bin"), "javac")).exists) parent
else java_home
}
def bootstrap_directory(
preference: String, envar: String, property: String, description: String): String =
{
val value =
proper_string(preference) orElse // explicit argument
proper_string(System.getenv(envar)) orElse // e.g. inherited from running isabelle tool
proper_string(System.getProperty(property)) getOrElse // e.g. via JVM application boot process
error("Unknown " + description + " directory")
if ((new JFile(value)).isDirectory) value
else error("Bad " + description + " directory " + quote(value))
}
/** implicit settings environment **/
abstract class Service
@volatile private var _settings: Option[Map[String, String]] = None
@volatile private var _services: Option[List[Class[Service]]] = None
def settings(): Map[String, String] =
{
if (_settings.isEmpty) init() // unsynchronized check
_settings.get
}
def services(): List[Class[Service]] =
{
if (_services.isEmpty) init() // unsynchronized check
_services.get
}
def make_services[C](c: Class[C]): List[C] =
for { c1 <- services() if Library.is_subclass(c1, c) }
yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = synchronized
{
if (_settings.isEmpty || _services.isEmpty) {
val isabelle_root1 =
bootstrap_directory(isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root")
val cygwin_root1 =
if (Platform.is_windows)
bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
else ""
if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
def set_cygwin_root(): Unit =
{
if (Platform.is_windows)
_settings = Some(_settings.getOrElse(Map.empty) + ("CYGWIN_ROOT" -> cygwin_root1))
}
set_cygwin_root()
def default(env: Map[String, String], entry: (String, String)): Map[String, String] =
if (env.isDefinedAt(entry._1) || entry._2 == "") env
else env + entry
val env =
{
val temp_windows =
{
val temp = if (Platform.is_windows) System.getenv("TEMP") else null
if (temp != null && temp.contains('\\')) temp else ""
}
val user_home = System.getProperty("user.home", "")
val isabelle_app = System.getProperty("isabelle.app", "")
default(
default(
default(sys.env + ("ISABELLE_JDK_HOME" -> File.standard_path(jdk_home())),
"TEMP_WINDOWS" -> temp_windows),
"HOME" -> user_home),
"ISABELLE_APP" -> "true")
}
val settings =
{
val dump = JFile.createTempFile("settings", null)
dump.deleteOnExit
try {
val cmd1 =
if (Platform.is_windows)
List(cygwin_root1 + "\\bin\\bash", "-l",
File.standard_path(isabelle_root1 + "\\bin\\isabelle"))
else
List(isabelle_root1 + "/bin/isabelle")
val cmd = cmd1 ::: List("getenv", "-d", dump.toString)
val (output, rc) = process_output(process(cmd, env = env, redirect = true))
if (rc != 0) error(output)
val entries =
(for (entry <- space_explode('\u0000', File.read(dump)) if entry != "") yield {
val i = entry.indexOf('=')
if (i <= 0) entry -> ""
else entry.substring(0, i) -> entry.substring(i + 1)
}).toMap
entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
}
finally { dump.delete }
}
_settings = Some(settings)
set_cygwin_root()
val variable = "ISABELLE_SCALA_SERVICES"
val services =
for (name <- space_explode(':', settings.getOrElse(variable, getenv_error(variable))))
yield {
def err(msg: String): Nothing =
error("Bad entry " + quote(name) + " in " + variable + "\n" + msg)
try { Class.forName(name).asInstanceOf[Class[Service]] }
catch {
case _: ClassNotFoundException => err("Class not found")
case exn: Throwable => err(Exn.message(exn))
}
}
_services = Some(services)
}
}
/* getenv -- dynamic process environment */
private def getenv_error(name: String): Nothing =
error("Undefined Isabelle environment variable: " + quote(name))
def getenv(name: String, env: Map[String, String] = settings()): String =
env.getOrElse(name, "")
def getenv_strict(name: String, env: Map[String, String] = settings()): String =
proper_string(getenv(name, env)) getOrElse
error("Undefined Isabelle environment variable: " + quote(name))
def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
/* getetc -- static distribution parameters */
def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] =
{
val path = root + Path.basic("etc") + Path.basic(name)
if (path.is_file) {
Library.trim_split_lines(File.read(path)) match {
case Nil => None
case List(s) => Some(s)
case _ => error("Single line expected in " + path.absolute)
}
}
else None
}
/* Isabelle distribution identification */
def isabelle_id(root: Path = Path.ISABELLE_HOME): String =
getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) getOrElse {
if (Mercurial.is_repository(root)) Mercurial.repository(root).parent()
else error("Failed to identify Isabelle distribution " + root)
}
object Isabelle_Id extends Scala.Fun_String("isabelle_id")
{
val here = Scala_Project.here
def apply(arg: String): String = isabelle_id()
}
def isabelle_tags(root: Path = Path.ISABELLE_HOME): String =
getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse {
if (Mercurial.is_repository(root)) {
val hg = Mercurial.repository(root)
hg.tags(rev = hg.parent())
}
else ""
}
def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER"))
def isabelle_heading(): String =
isabelle_identifier() match {
case None => ""
case Some(version) => " (" + version + ")"
}
def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading()
/** file-system operations **/
/* scala functions */
private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] =
{ fun(args.map(Path.explode)); Nil }
private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
apply_paths(args, { case List(path) => fun(path) })
private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] =
apply_paths(args, { case List(path1, path2) => fun(path1, path2) })
private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
/* permissions */
def chmod(arg: String, path: Path): Unit =
bash("chmod " + arg + " " + File.bash_path(path)).check
def chown(arg: String, path: Path): Unit =
bash("chown " + arg + " " + File.bash_path(path)).check
/* directories */
def make_directory(path: Path): Path =
{
if (!path.is_dir) {
try { Files.createDirectories(path.file.toPath) }
catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
}
path
}
def new_directory(path: Path): Path =
if (path.is_dir) error("Directory already exists: " + path.absolute)
else make_directory(path)
def copy_dir(dir1: Path, dir2: Path): Unit =
{
val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2))
if (!res.ok) {
cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err)
}
}
object Make_Directory extends Scala.Fun_Strings("make_directory")
{
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths1(args, make_directory)
}
object Copy_Dir extends Scala.Fun_Strings("copy_dir")
{
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir)
}
/* copy files */
def copy_file(src: JFile, dst: JFile): Unit =
{
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
if (!File.eq(src, target)) {
try {
Files.copy(src.toPath, target.toPath,
StandardCopyOption.COPY_ATTRIBUTES,
StandardCopyOption.REPLACE_EXISTING)
}
catch {
case ERROR(msg) =>
cat_error("Failed top copy file " +
File.path(src).absolute + " to " + File.path(dst).absolute, msg)
}
}
}
def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file)
def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit =
{
val src1 = src.expand
val src1_dir = src1.dir
if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory")
copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir))
}
object Copy_File extends Scala.Fun_Strings("copy_file")
{
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths2(args, copy_file)
}
object Copy_File_Base extends Scala.Fun_Strings("copy_file_base")
{
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base)
}
/* move files */
def move_file(src: JFile, dst: JFile): Unit =
{
val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
if (!File.eq(src, target))
Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
}
def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file)
/* symbolic link */
def symlink(src: Path, dst: Path, force: Boolean = false): Unit =
{
val src_file = src.file
val dst_file = dst.file
val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
if (force) target.delete
try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
catch {
case _: UnsupportedOperationException if Platform.is_windows =>
Cygwin.link(File.standard_path(src), target)
case _: FileSystemException if Platform.is_windows =>
Cygwin.link(File.standard_path(src), target)
}
}
/* tmp files */
def isabelle_tmp_prefix(): JFile =
{
val path = Path.explode("$ISABELLE_TMP_PREFIX")
path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment
File.platform_file(path)
}
def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile =
{
val suffix = if (ext == "") "" else "." + ext
val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
file.deleteOnExit
file
}
def with_tmp_file[A](name: String, ext: String = "")(body: Path => A): A =
{
val file = tmp_file(name, ext)
try { body(File.path(file)) } finally { file.delete }
}
/* tmp dirs */
def rm_tree(root: JFile): Unit =
{
root.delete
if (root.isDirectory) {
Files.walkFileTree(root.toPath,
new SimpleFileVisitor[JPath] {
override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult =
{
try { Files.deleteIfExists(file) }
catch { case _: IOException => }
FileVisitResult.CONTINUE
}
override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult =
{
if (e == null) {
try { Files.deleteIfExists(dir) }
catch { case _: IOException => }
FileVisitResult.CONTINUE
}
else throw e
}
}
)
}
}
def rm_tree(root: Path): Unit = rm_tree(root.file)
object Rm_Tree extends Scala.Fun_Strings("rm_tree")
{
val here = Scala_Project.here
def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree)
}
def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
{
val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
dir.deleteOnExit
dir
}
def with_tmp_dir[A](name: String)(body: Path => A): A =
{
val dir = tmp_dir(name)
try { body(File.path(dir)) } finally { rm_tree(dir) }
}
/* quasi-atomic update of directory */
def update_directory(dir: Path, f: Path => Unit): Unit =
{
val new_dir = dir.ext("new")
val old_dir = dir.ext("old")
rm_tree(new_dir)
rm_tree(old_dir)
f(new_dir)
if (dir.is_dir) move_file(dir, old_dir)
move_file(new_dir, dir)
rm_tree(old_dir)
}
/** external processes **/
/* raw process */
def process(command_line: List[String],
cwd: JFile = null,
env: Map[String, String] = settings(),
redirect: Boolean = false): Process =
{
val proc = new ProcessBuilder
// fragile on Windows:
// see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
proc.command(command_line.asJava)
if (cwd != null) proc.directory(cwd)
if (env != null) {
proc.environment.clear()
for ((x, y) <- env) proc.environment.put(x, y)
}
proc.redirectErrorStream(redirect)
proc.start
}
def process_output(proc: Process): (String, Int) =
{
proc.getOutputStream.close()
val output = File.read_stream(proc.getInputStream)
val rc =
try { proc.waitFor }
finally {
proc.getInputStream.close()
proc.getErrorStream.close()
proc.destroy()
Exn.Interrupt.dispose()
}
(output, rc)
}
def process_signal(group_pid: String, signal: String = "0"): Boolean =
{
val bash =
if (Platform.is_windows) List(cygwin_root() + "\\bin\\bash.exe")
else List("/usr/bin/env", "bash")
val (_, rc) = process_output(process(bash ::: List("-c", "kill -" + signal + " -" + group_pid)))
rc == 0
}
/* GNU bash */
def bash(script: String,
cwd: JFile = null,
env: Map[String, String] = settings(),
redirect: Boolean = false,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
watchdog: Option[Bash.Watchdog] = None,
strict: Boolean = true,
cleanup: () => Unit = () => ()): Process_Result =
{
Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
result(progress_stdout = progress_stdout, progress_stderr = progress_stderr,
watchdog = watchdog, strict = 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,
dir: Path = Path.current,
original_owner: Boolean = false,
+ strip: Int = 0,
redirect: Boolean = false): Process_Result =
{
val options =
(if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
- (if (original_owner) "" else "--owner=root --group=staff ")
+ (if (original_owner) "" else "--owner=root --group=staff ") +
+ (if (strip <= 0) "" else "--strip-components=" + strip + " ")
if (gnutar_check) bash("tar " + options + args, redirect = redirect)
else error("Expected to find GNU tar executable")
}
def require_command(cmds: String*): Unit =
{
for (cmd <- cmds) {
if (!bash(Bash.string(cmd) + " --version").ok) error("Missing system command: " + quote(cmd))
}
}
def hostname(): String = bash("hostname -s").check.out
def open(arg: String): Unit =
bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &")
def pdf_viewer(arg: Path): Unit =
bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &")
def open_external_file(name: String): Boolean =
{
val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
val external =
ext.nonEmpty &&
Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
if (external) {
if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
else open(name)
}
external
}
def export_isabelle_identifier(isabelle_identifier: String): String =
if (isabelle_identifier == "") ""
else "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n"
/** Isabelle resources **/
/* repository clone with Admin */
def admin(): Boolean = Path.explode("~~/Admin").is_dir
/* components */
def components(): List[Path] =
Path.split(getenv_strict("ISABELLE_COMPONENTS"))
/* default logic */
def default_logic(args: String*): String =
{
args.find(_ != "") match {
case Some(logic) => logic
case None => getenv_strict("ISABELLE_LOGIC")
}
}
/* download file */
def download(url_name: String, progress: Progress = new Progress): HTTP.Content =
{
val url = Url(url_name)
progress.echo("Getting " + quote(url_name))
try { HTTP.Client.get(url) }
catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) }
}
def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit =
Bytes.write(file, download(url_name, progress = progress).bytes)
object Download extends Scala.Fun("download", thread = true)
{
val here = Scala_Project.here
override def invoke(args: List[Bytes]): List[Bytes] =
args match { case List(url) => List(download(url.text).bytes) }
}
/* repositories */
val isabelle_repository: Mercurial.Server =
Mercurial.Server("https://isabelle.sketis.net/repos/isabelle")
val afp_repository: Mercurial.Server =
Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel")
def official_releases(): List[String] =
Library.trim_split_lines(
isabelle_repository.read_file(Path.explode("Admin/Release/official")))
}