diff --git a/Admin/Release/CHECKLIST b/Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST
+++ b/Admin/Release/CHECKLIST
@@ -1,98 +1,98 @@
Checklist for official releases
===============================
- check latest updates of polyml, jdk, scala, jedit;
- check Admin/components;
- test "isabelle dump -b Pure ZF";
- test "isabelle build -o export_theory -f ZF";
- test "isabelle server" according to "system" manual;
- test Isabelle/VSCode;
- test Isabelle/jEdit: print buffer
- test Isabelle/jEdit: deactivate main plugin;
- test "#!/usr/bin/env isabelle_scala_script";
- test Windows 10 subsystem for Linux:
https://docs.microsoft.com/en-us/windows/wsl/install-win10
- check (non-)executable files:
$ find . "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" -o -name ROOT ")" -executable
$ find -type f -executable
- check sources:
isabelle check_sources '~~' '$AFP_BASE'
- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
- check versions:
src/Tools/jEdit/jedit_base/plugin.props
src/Tools/jEdit/jedit_main/plugin.props
- check Isabelle version:
src/Tools/VSCode/extension/README.md
src/Tools/VSCode/extension/package.json
- check funny base directory, e.g. "Test 中国";
- diff NEWS wrt. last official release, which is read-only;
- update https://isabelle.sketis.net/repos/isabelle-website
- check doc/Contents, $JEDIT_HOME/doc/Contents;
- test old HD display: Linux, Windows, macOS;
- macOS: check recent MacTeX;
- Windows: check recent MiKTeX;
- Phabricator:
. src/Doc/System/Phabricator.thy: check/update underlying Ubuntu version
. etc/options: check/update phabricator_version entries;
Repository fork
===============
- isabelle: finalize NEWS / CONTRIBUTORS -- proper headers for named release;
- isabelle-release: hg tag;
- isabelle: back to post-release mode -- after fork point;
Packaging
=========
- fully-automated packaging (e.g. on lxcisa0):
- hg up -r DISTNAME && Admin/build_release -J .../java11 -D /p/home/isabelle/dist -b HOL -l -R DISTNAME
+ hg up -r DISTNAME && Admin/build_release -D /p/home/isabelle/dist -b HOL -l -R DISTNAME
- Docker image:
isabelle build_docker -o Dockerfile -E -t makarius/isabelle:Isabelle2021-1 Isabelle2021-1_linux.tar.gz
docker login
docker push makarius/isabelle:Isabelle2021-1
docker tag ... latest
docker push makarius/isabelle:latest
https://hub.docker.com/r/makarius/isabelle
https://docs.docker.com/engine/reference/commandline/push
Post-release
============
- update Admin/Release/official
- update /p/home/isabelle and /p/home/isabelle/html-data
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,940 +1,952 @@
/* Title: Pure/Admin/build_release.scala
Author: Makarius
Build full Isabelle distribution from repository.
*/
package isabelle
object Build_Release
{
/** 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
+ private def bash_java_opens(args: String*): String =
+ Bash.strings(args.toList.flatMap(arg => List("--add-opens", arg + "=ALL-UNNAMED")))
+
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_arm =>
Bundle_Info(platform, "Linux (ARM)", dist_name + "_linux_arm.tar.gz")
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)
}
/** 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
{
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)
Bytes.write(archive_path, bytes)
execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1)
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 **/
/* 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())) :::
Platform.Family.list.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("#")
} 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) } 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))
}
/** build release **/
/* build heaps */
private def build_heaps(
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
local_dir: Path): Unit =
{
val server_option = "build_host_" + platform.toString
val ssh =
options.string(server_option) match {
case "" =>
if (Platform.family == platform) SSH.Local
else error("Undefined option " + server_option + ": cannot build heaps")
case SSH.Target(user, host) =>
SSH.open_session(options, host = host, user = user)
case s => error("Malformed option " + server_option + ": " + quote(s))
}
try {
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),
"tar -cf tmp.tar heaps")
ssh.execute(remote_commands.mkString(" && "), settings = false).check
ssh.read_file(remote_tmp_tar, local_tmp_tar)
})
execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar))
})
}
finally { ssh.close() }
}
/* 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=($(grep -v '^#' "$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.jedit.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.Family.standard(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 */
def use_release_archive(
context: Release_Context,
archive: Release_Archive,
id: String = ""): Unit =
{
if (id.nonEmpty && id != archive.id) {
error("Mismatch of release identification " + id + " vs. archive " + archive.id)
}
if (!context.isabelle_archive.is_file || Bytes.read(context.isabelle_archive) != archive.bytes) {
Bytes.write(context.isabelle_archive, archive.bytes)
}
}
def build_release_archive(
context: Release_Context,
version: String,
parallel_jobs: Int = 1): Unit =
{
val progress = context.progress
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("Preparing release " + context.dist_name + " ...")
Isabelle_System.new_directory(context.dist_dir)
hg.archive(context.isabelle_dir.expand.implode, rev = id, options = "--type files")
for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) {
(context.isabelle_dir + Path.explode(name)).file.delete
}
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)
context.make_announce(id)
context.make_contrib()
execute(context.isabelle_dir, """find . -print | xargs chmod -f u+rw""")
record_bundled_components(context.isabelle_dir)
/* build tools and documentation */
val other_isabelle = context.other_isabelle(context.dist_dir)
other_isabelle.init_settings(
other_isabelle.init_components(
components_base = context.components_base, catalogs = List("main")))
other_isabelle.resolve_components(echo = true)
try {
other_isabelle.bash(
"export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" +
"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
}
catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
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 release archive " + context.isabelle_archive + " ...")
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))
}
}
def default_platform_families: List[Platform.Family.Value] = Platform.Family.list0
def build_release(
options: Options,
context: Release_Context,
afp_rev: String = "",
platform_families: List[Platform.Family.Value] = default_platform_families,
- java_home: Path = default_java_home,
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
/* 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(context.bundle_info)
for (bundle_info <- bundle_infos) {
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(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(context.components_base, bundled_components,
target_dir = Some(contrib_dir),
copy_dir = Some(context.dist_dir + Path.explode("contrib")),
progress = progress)
val more_components_names =
more_components.map(Components.unpack(contrib_dir, _, progress = progress))
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
val classpath1 = Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH"))
val classpath2 = Path.split(other_isabelle.getenv("ISABELLE_SETUP_CLASSPATH"))
(classpath1 ::: classpath2).map(path =>
{
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
case None => error("Bad classpath element: " + abs_path)
}
})
}
val jedit_options = Path.explode("src/Tools/jEdit/etc/options")
val jedit_props =
Path.explode(other_isabelle.getenv("JEDIT_HOME") + "/properties/jEdit.props")
// build heaps
if (build_sessions.nonEmpty) {
progress.echo("Building heaps " + commas_quote(build_sessions) + " ...")
build_heaps(options, platform, build_sessions, isabelle_target)
}
// application bundling
Components.purge(contrib_dir, platform)
platform match {
case Platform.Family.linux_arm | 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)
progress.echo("Packaging " + bundle_info.name + " ...")
execute_tar(tmp_dir,
"-czf " + File.bash_path(context.dist_dir + bundle_info.path) + " " +
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, 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
progress.echo("Packaging " + bundle_info.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(context.dist_dir + bundle_info.path) + " " +
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 = bundle_info.path
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 + "\\"))
+ val java_opts =
+ bash_java_opens(
+ "java.base/java.io",
+ "java.base/java.lang",
+ "java.base/java.lang.reflect",
+ "java.base/java.text",
+ "java.base/java.util",
+ "java.desktop/java.awt.font")
+ val launch4j_jar =
+ Path.explode("windows_app/launch4j-" + Platform.family + "/launch4j.jar")
+
execute(tmp_dir,
- "env JAVA_HOME=" + File.bash_platform_path(java_home) +
- " \"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
+ cat_lines(List(
+ "export LAUNCH4J=" + File.bash_platform_path(launch4j_jar),
+ "isabelle java " + java_opts + " -jar \"$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(context.dist_dir + isabelle_exe,
Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
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 (context.dist_dir + bundle_info.path).is_file
} yield (bundle_info.name, bundle_info)
val isabelle_link =
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(context.dist_name)),
List(
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 + " bundle"))) })),
HTML.subsection("Repositories"),
HTML.itemize(
List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
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 (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 =
context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
val other_isabelle = context.other_isabelle(tmp_dir)
+ Isabelle_System.make_directory(other_isabelle.etc)
+ File.write(other_isabelle.etc_settings, "ML_OPTIONS=\"--minheap 1000 --maxheap 4000\"\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(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"))
})
}
}
}
/** command line entry point **/
- def default_java_home: Path = Path.explode("$JAVA_HOME").expand
-
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 java_home = default_java_home
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]
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 ".")
- -J JAVA_HOME Java version for running launch4j (e.g. version 11)
-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: 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)),
- "J:" -> (arg => java_home = Path.explode(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()
if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok)
error("Building for windows requires 7z")
val progress = new Console_Progress()
def make_context(name: String): Release_Context =
Release_Context(target_dir,
release_name = name,
components_base = components_base,
progress = 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, progress = progress)
val context = make_context(archive.identifier)
Isabelle_System.make_directory(context.dist_dir)
use_release_archive(context, archive, id = rev)
context
}
build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
- java_home = java_home, more_components = more_components, build_sessions = build_sessions,
+ more_components = more_components, build_sessions = build_sessions,
build_library = build_library, parallel_jobs = parallel_jobs, website = website)
}
}
}
diff --git a/src/Pure/Admin/build_status.scala b/src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala
+++ b/src/Pure/Admin/build_status.scala
@@ -1,625 +1,625 @@
/* Title: Pure/Admin/build_status.scala
Author: Makarius
Present recent build status information from database.
*/
package isabelle
object Build_Status
{
/* defaults */
val default_target_dir = Path.explode("build_status")
val default_image_size = (800, 600)
val default_history = 30
def default_profiles: List[Profile] =
Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles
/* data profiles */
sealed case class Profile(
description: String, history: Int = 0, afp: Boolean = false, bulky: Boolean = false, sql: String)
{
def days(options: Options): Int = options.int("build_log_history") max history
def stretch(options: Options): Double =
(days(options) max default_history min (default_history * 5)).toDouble / default_history
def select(options: Options, columns: List[SQL.Column], only_sessions: Set[String]): SQL.Source =
{
Build_Log.Data.universal_table.select(columns, distinct = true,
sql = "WHERE " +
Build_Log.Data.pull_date(afp) + " > " + Build_Log.Data.recent_time(days(options)) +
" AND " +
SQL.member(Build_Log.Data.status.ident,
List(
Build_Log.Session_Status.finished.toString,
Build_Log.Session_Status.failed.toString)) +
(if (only_sessions.isEmpty) ""
else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
" AND " + SQL.enclose(sql))
}
}
/* build status */
def build_status(options: Options,
progress: Progress = new Progress,
profiles: List[Profile] = default_profiles,
only_sessions: Set[String] = Set.empty,
verbose: Boolean = false,
target_dir: Path = default_target_dir,
ml_statistics: Boolean = false,
image_size: (Int, Int) = default_image_size): Unit =
{
val ml_statistics_domain =
Iterator(ML_Statistics.heap_fields, ML_Statistics.program_fields, ML_Statistics.tasks_fields,
ML_Statistics.workers_fields).flatMap(_._2).toSet
val data =
read_data(options, progress = progress, profiles = profiles,
only_sessions = only_sessions, verbose = verbose,
ml_statistics = ml_statistics, ml_statistics_domain = ml_statistics_domain)
present_data(data, progress = progress, target_dir = target_dir, image_size = image_size)
}
/* read data */
sealed case class Data(date: Date, entries: List[Data_Entry])
sealed case class Data_Entry(
name: String, hosts: List[String], stretch: Double, sessions: List[Session])
{
def failed_sessions: List[Session] =
sessions.filter(_.head.failed).sortBy(_.name)
}
sealed case class Session(
name: String, threads: Int, entries: List[Entry],
ml_statistics: ML_Statistics, ml_statistics_date: Long)
{
require(entries.nonEmpty, "no entries")
lazy val sorted_entries: List[Entry] = entries.sortBy(entry => - entry.date)
def head: Entry = sorted_entries.head
def order: Long = - head.timing.elapsed.ms
def finished_entries: List[Entry] = sorted_entries.filter(_.finished)
def finished_entries_size: Int = finished_entries.map(_.date).toSet.size
def check_timing: Boolean = finished_entries_size >= 3
def check_heap: Boolean =
finished_entries_size >= 3 &&
finished_entries.forall(entry =>
entry.maximum_heap > 0 ||
entry.average_heap > 0 ||
entry.stored_heap > 0)
def make_csv: CSV.File =
{
val header =
List("session_name",
"chapter",
"pull_date",
"afp_pull_date",
"isabelle_version",
"afp_version",
"timing_elapsed",
"timing_cpu",
"timing_gc",
"ml_timing_elapsed",
"ml_timing_cpu",
"ml_timing_gc",
"maximum_code",
"average_code",
"maximum_stack",
"average_stack",
"maximum_heap",
"average_heap",
"stored_heap",
"status")
val date_format = Date.Format("uuuu-MM-dd HH:mm:ss")
val records =
for (entry <- sorted_entries) yield {
CSV.Record(name,
entry.chapter,
date_format(entry.pull_date),
entry.afp_pull_date match { case Some(date) => date_format(date) case None => "" },
entry.isabelle_version,
entry.afp_version,
entry.timing.elapsed.ms,
entry.timing.cpu.ms,
entry.timing.gc.ms,
entry.ml_timing.elapsed.ms,
entry.ml_timing.cpu.ms,
entry.ml_timing.gc.ms,
entry.maximum_code,
entry.average_code,
entry.maximum_stack,
entry.average_stack,
entry.maximum_heap,
entry.average_heap,
entry.stored_heap,
entry.status)
}
CSV.File(name, header, records)
}
}
sealed case class Entry(
chapter: String,
pull_date: Date,
afp_pull_date: Option[Date],
isabelle_version: String,
afp_version: String,
timing: Timing,
ml_timing: Timing,
maximum_code: Long,
average_code: Long,
maximum_stack: Long,
average_stack: Long,
maximum_heap: Long,
average_heap: Long,
stored_heap: Long,
status: Build_Log.Session_Status.Value,
errors: List[String])
{
val date: Long = (afp_pull_date getOrElse pull_date).unix_epoch
def finished: Boolean = status == Build_Log.Session_Status.finished
def failed: Boolean = status == Build_Log.Session_Status.failed
def present_errors(name: String): XML.Body =
{
if (errors.isEmpty)
HTML.text(name + print_version(isabelle_version, afp_version, chapter))
else {
HTML.tooltip_errors(HTML.text(name), errors.map(s => HTML.text(Symbol.decode(s)))) ::
HTML.text(print_version(isabelle_version, afp_version, chapter))
}
}
}
sealed case class Image(name: String, width: Int, height: Int)
{
def path: Path = Path.basic(name)
}
def print_version(
isabelle_version: String, afp_version: String = "", chapter: String = AFP.chapter): String =
{
val body =
proper_string(isabelle_version).map("Isabelle/" + _).toList :::
(if (chapter == AFP.chapter) proper_string(afp_version).map("AFP/" + _) else None).toList
if (body.isEmpty) "" else body.mkString(" (", ", ", ")")
}
def read_data(options: Options,
progress: Progress = new Progress,
profiles: List[Profile] = default_profiles,
only_sessions: Set[String] = Set.empty,
ml_statistics: Boolean = false,
- ml_statistics_domain: String => Boolean = (key: String) => true,
+ ml_statistics_domain: String => Boolean = _ => true,
verbose: Boolean = false): Data =
{
val date = Date.now()
var data_hosts = Map.empty[String, Set[String]]
var data_stretch = Map.empty[String, Double]
var data_entries = Map.empty[String, Map[String, Session]]
def get_hosts(data_name: String): Set[String] =
data_hosts.getOrElse(data_name, Set.empty)
val store = Build_Log.store(options)
using(store.open_database())(db =>
{
for (profile <- profiles.sortBy(_.description)) {
progress.echo("input " + quote(profile.description))
val afp = profile.afp
val columns =
List(
Build_Log.Data.pull_date(afp = false),
Build_Log.Data.pull_date(afp = true),
Build_Log.Prop.build_host,
Build_Log.Prop.isabelle_version,
Build_Log.Prop.afp_version,
Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
Build_Log.Settings.ML_PLATFORM,
Build_Log.Data.session_name,
Build_Log.Data.chapter,
Build_Log.Data.groups,
Build_Log.Data.threads,
Build_Log.Data.timing_elapsed,
Build_Log.Data.timing_cpu,
Build_Log.Data.timing_gc,
Build_Log.Data.ml_timing_elapsed,
Build_Log.Data.ml_timing_cpu,
Build_Log.Data.ml_timing_gc,
Build_Log.Data.heap_size,
Build_Log.Data.status,
Build_Log.Data.errors) :::
(if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil)
val Threads_Option = """threads\s*=\s*(\d+)""".r
val sql = profile.select(options, columns, only_sessions)
progress.echo_if(verbose, sql)
db.using_statement(sql)(stmt =>
{
val res = stmt.execute_query()
while (res.next()) {
val session_name = res.string(Build_Log.Data.session_name)
val chapter = res.string(Build_Log.Data.chapter)
val groups = split_lines(res.string(Build_Log.Data.groups))
val threads =
{
val threads1 =
res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
case Threads_Option(Value.Int(i)) => i
case _ => 1
}
val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1)
threads1 max threads2
}
val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
val ml_platform_64 =
ml_platform.startsWith("x86_64-") || ml_platform.startsWith("arm64-")
val data_name =
profile.description +
(if (ml_platform_64) ", 64bit" else "") +
(if (threads == 1) "" else ", " + threads + " threads")
res.get_string(Build_Log.Prop.build_host).foreach(host =>
data_hosts += (data_name -> (get_hosts(data_name) + host)))
data_stretch += (data_name -> profile.stretch(options))
val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
val afp_version = res.string(Build_Log.Prop.afp_version)
val ml_stats =
ML_Statistics(
if (ml_statistics) {
Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics), cache = store.cache)
}
else Nil,
domain = ml_statistics_domain,
heading = session_name + print_version(isabelle_version, afp_version, chapter))
val entry =
Entry(
chapter = chapter,
pull_date = res.date(Build_Log.Data.pull_date(afp = false)),
afp_pull_date =
if (afp) res.get_date(Build_Log.Data.pull_date(afp = true)) else None,
isabelle_version = isabelle_version,
afp_version = afp_version,
timing =
res.timing(
Build_Log.Data.timing_elapsed,
Build_Log.Data.timing_cpu,
Build_Log.Data.timing_gc),
ml_timing =
res.timing(
Build_Log.Data.ml_timing_elapsed,
Build_Log.Data.ml_timing_cpu,
Build_Log.Data.ml_timing_gc),
maximum_code = ml_stats.maximum(ML_Statistics.CODE_SIZE).toLong,
average_code = ml_stats.average(ML_Statistics.CODE_SIZE).toLong,
maximum_stack = ml_stats.maximum(ML_Statistics.STACK_SIZE).toLong,
average_stack = ml_stats.average(ML_Statistics.STACK_SIZE).toLong,
maximum_heap = ml_stats.maximum(ML_Statistics.HEAP_SIZE).toLong,
average_heap = ml_stats.average(ML_Statistics.HEAP_SIZE).toLong,
stored_heap = ML_Statistics.mem_scale(res.long(Build_Log.Data.heap_size)),
status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
errors =
Build_Log.uncompress_errors(
res.bytes(Build_Log.Data.errors), cache = store.cache))
val sessions = data_entries.getOrElse(data_name, Map.empty)
val session =
sessions.get(session_name) match {
case None =>
Session(session_name, threads, List(entry), ml_stats, entry.date)
case Some(old) =>
val (ml_stats1, ml_stats1_date) =
if (entry.date > old.ml_statistics_date) (ml_stats, entry.date)
else (old.ml_statistics, old.ml_statistics_date)
Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date)
}
if ((!afp || chapter == AFP.chapter) &&
(!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) {
data_entries += (data_name -> (sessions + (session_name -> session)))
}
}
})
}
})
val sorted_entries =
(for {
(name, sessions) <- data_entries.toList
sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order))
}
yield {
val hosts = get_hosts(name).toList.sorted
val stretch = data_stretch(name)
Data_Entry(name, hosts, stretch, sorted_sessions)
}).sortBy(_.name)
Data(date, sorted_entries)
}
/* present data */
def present_data(data: Data,
progress: Progress = new Progress,
target_dir: Path = default_target_dir,
image_size: (Int, Int) = default_image_size): Unit =
{
def clean_name(name: String): String =
name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
HTML.write_document(target_dir, "index.html",
List(HTML.title("Isabelle build status")),
List(HTML.chapter("Isabelle build status"),
HTML.par(
List(HTML.description(
List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
HTML.par(
- List(HTML.itemize(data.entries.map({ case data_entry =>
+ List(HTML.itemize(data.entries.map(data_entry =>
List(
HTML.link(clean_name(data_entry.name) + "/index.html",
HTML.text(data_entry.name))) :::
(data_entry.failed_sessions match {
case Nil => Nil
case sessions =>
HTML.break :::
List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) :::
List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
})
- }))))))
+ ))))))
for (data_entry <- data.entries) {
val data_name = data_entry.name
val (image_width, image_height) = image_size
val image_width_stretch = (image_width * data_entry.stretch).toInt
progress.echo("output " + quote(data_name))
val dir = Isabelle_System.make_directory(target_dir + Path.basic(clean_name(data_name)))
val data_files =
(for (session <- data_entry.sessions) yield {
val csv_file = session.make_csv
csv_file.write(dir)
session.name -> csv_file
}).toMap
val session_plots =
Par_List.map((session: Session) =>
Isabelle_System.with_tmp_file(session.name, "data") { data_file =>
Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file =>
def plot_name(kind: String): String = session.name + "_" + kind + ".png"
File.write(data_file,
cat_lines(
session.finished_entries.map(entry =>
List(entry.date.toString,
entry.timing.elapsed.minutes.toString,
entry.timing.resources.minutes.toString,
entry.ml_timing.elapsed.minutes.toString,
entry.ml_timing.resources.minutes.toString,
entry.maximum_code.toString,
- entry.maximum_code.toString,
+ entry.average_code.toString,
+ entry.maximum_stack.toString,
entry.average_stack.toString,
- entry.maximum_stack.toString,
- entry.average_heap.toString,
+ entry.maximum_heap.toString,
entry.average_heap.toString,
entry.stored_heap.toString).mkString(" "))))
val max_time =
(session.finished_entries.foldLeft(0.0) {
case (m, entry) =>
m.max(entry.timing.elapsed.minutes).
max(entry.timing.resources.minutes).
max(entry.ml_timing.elapsed.minutes).
max(entry.ml_timing.resources.minutes)
} max 0.1) * 1.1
val timing_range = "[0:" + max_time + "]"
def gnuplot(plot_name: String, plots: List[String], range: String): Image =
{
val image = Image(plot_name, image_width_stretch, image_height)
File.write(gnuplot_file, """
set terminal png size """ + image.width + "," + image.height + """
set output """ + quote(File.standard_path(dir + image.path)) + """
set xdata time
set timefmt "%s"
set format x "%d-%b"
set xlabel """ + quote(session.name) + """ noenhanced
set key left bottom
plot [] """ + range + " " +
plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
val result =
Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
if (!result.ok)
result.error("Gnuplot failed for " + data_name + "/" + plot_name).check
image
}
val timing_plots =
{
val plots1 =
List(
""" using 1:2 smooth sbezier title "elapsed time (smooth)" """,
""" using 1:2 smooth csplines title "elapsed time" """)
val plots2 =
List(
""" using 1:3 smooth sbezier title "cpu time (smooth)" """,
""" using 1:3 smooth csplines title "cpu time" """)
if (session.threads == 1) plots1 else plots1 ::: plots2
}
val ml_timing_plots =
List(
""" using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
""" using 1:4 smooth csplines title "ML elapsed time" """,
""" using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
""" using 1:5 smooth csplines title "ML cpu time" """)
val heap_plots =
List(
""" using 1:10 smooth sbezier title "heap maximum (smooth)" """,
""" using 1:10 smooth csplines title "heap maximum" """,
""" using 1:11 smooth sbezier title "heap average (smooth)" """,
""" using 1:11 smooth csplines title "heap average" """,
""" using 1:12 smooth sbezier title "heap stored (smooth)" """,
""" using 1:12 smooth csplines title "heap stored" """)
def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image =
{
val image = Image(plot_name, image_width, image_height)
val chart =
session.ml_statistics.chart(
fields._1 + ": " + session.ml_statistics.heading, fields._2)
Graphics_File.write_chart_png(
(dir + image.path).file, chart, image.width, image.height)
image
}
val images =
(if (session.check_timing)
List(
gnuplot(plot_name("timing"), timing_plots, timing_range),
gnuplot(plot_name("ml_timing"), ml_timing_plots, timing_range))
else Nil) :::
(if (session.check_heap)
List(gnuplot(plot_name("heap"), heap_plots, "[0:]"))
else Nil) :::
(if (session.ml_statistics.content.nonEmpty)
List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields),
jfreechart(plot_name("program_chart"), ML_Statistics.program_fields)) :::
(if (session.threads > 1)
List(
jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields),
jfreechart(plot_name("workers_chart"), ML_Statistics.workers_fields))
else Nil)
else Nil)
session.name -> images
}
}, data_entry.sessions).toMap
HTML.write_document(dir, "index.html",
List(HTML.title("Isabelle build status for " + data_name)),
HTML.chapter("Isabelle build status for " + data_name) ::
HTML.par(
List(HTML.description(
List(
HTML.text("status date:") -> HTML.text(data.date.toString),
HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) ::
HTML.par(
List(HTML.itemize(
data_entry.sessions.map(session =>
HTML.link("#session_" + session.name, HTML.text(session.name)) ::
HTML.text(" (" + session.head.timing.message_resources + ")"))))) ::
data_entry.sessions.flatMap(session =>
List(
HTML.section(HTML.id("session_" + session.name), session.name),
HTML.par(
HTML.description(
List(
HTML.text("data:") ->
List(HTML.link(data_files(session.name).file_name, HTML.text("CSV"))),
HTML.text("timing:") -> HTML.text(session.head.timing.message_resources),
HTML.text("ML timing:") -> HTML.text(session.head.ml_timing.message_resources)) :::
ML_Statistics.mem_print(session.head.maximum_code).map(s =>
HTML.text("code maximum:") -> HTML.text(s)).toList :::
ML_Statistics.mem_print(session.head.average_code).map(s =>
HTML.text("code average:") -> HTML.text(s)).toList :::
ML_Statistics.mem_print(session.head.maximum_stack).map(s =>
HTML.text("stack maximum:") -> HTML.text(s)).toList :::
ML_Statistics.mem_print(session.head.average_stack).map(s =>
HTML.text("stack average:") -> HTML.text(s)).toList :::
ML_Statistics.mem_print(session.head.maximum_heap).map(s =>
HTML.text("heap maximum:") -> HTML.text(s)).toList :::
ML_Statistics.mem_print(session.head.average_heap).map(s =>
HTML.text("heap average:") -> HTML.text(s)).toList :::
ML_Statistics.mem_print(session.head.stored_heap).map(s =>
HTML.text("heap stored:") -> HTML.text(s)).toList :::
proper_string(session.head.isabelle_version).map(s =>
HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
proper_string(session.head.afp_version).map(s =>
HTML.text("AFP version:") -> HTML.text(s)).toList) ::
session_plots.getOrElse(session.name, Nil).map(image =>
HTML.size(image.width / 2, image.height / 2)(HTML.image(image.name)))))))
}
}
/* Isabelle tool wrapper */
val isabelle_tool =
Isabelle_Tool("build_status", "present recent build status information from database",
Scala_Project.here, args =>
{
var target_dir = default_target_dir
var ml_statistics = false
var only_sessions = Set.empty[String]
var options = Options.init()
var image_size = default_image_size
var verbose = false
val getopts = Getopts("""
Usage: isabelle build_status [OPTIONS]
Options are:
-D DIR target directory (default """ + default_target_dir + """)
-M include full ML statistics
-S SESSIONS only given SESSIONS (comma separated)
-l DAYS length of relevant history (default """ + options.int("build_log_history") + """)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-s WxH size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
-v verbose
Present performance statistics from build log database, which is specified
via system options build_log_database_host, build_log_database_user,
build_log_history etc.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
"M" -> (_ => ml_statistics = true),
"S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
"l:" -> (arg => options = options + ("build_log_history=" + arg)),
"o:" -> (arg => options = options + arg),
"s:" -> (arg =>
- space_explode('x', arg).map(Value.Int.parse(_)) match {
+ space_explode('x', arg).map(Value.Int.parse) match {
case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
case _ => error("Error bad PNG image size: " + quote(arg))
}),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress
build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose,
target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size)
})
}
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,652 +1,652 @@
/* 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.java_path, current_log.java_path)
})
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, 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", "i21of4", user = "i21isatest",
proxy_host = "lxbroy10", proxy_user = "i21isatest",
self_update = true,
options = "-m32 -M1x4,2,4" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_MLTON=mlton" +
" -e ISABELLE_SMLNJ=sml" +
" -e ISABELLE_SWIPL=swipl",
args = "-a -d '~~/src/Benchmarks'"),
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 A", "augsburg1",
- options = "-m32 -B -M1x2,2,4" +
+ options = "-m32 -B -M4" +
" -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
" -e ISABELLE_GHC_SETUP=true" +
" -e ISABELLE_MLTON=mlton" +
" -e ISABELLE_SMLNJ=sml" +
" -e ISABELLE_SWIPL=swipl",
self_update = true, args = "-a -d '~~/src/Benchmarks'")),
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 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,76 +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): Unit =
{
Isabelle_System.with_tmp_dir("isadist")(target_dir =>
{
Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
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,
- java_home = Path.explode("$BUILD_JAVA_HOME"),
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/ML/ml_statistics.scala b/src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala
+++ b/src/Pure/ML/ml_statistics.scala
@@ -1,319 +1,324 @@
/* Title: Pure/ML/ml_statistics.scala
Author: Makarius
ML runtime statistics.
*/
package isabelle
import scala.annotation.tailrec
import scala.collection.mutable
import scala.collection.immutable.{SortedSet, SortedMap}
import scala.swing.{Frame, Component}
import org.jfree.data.xy.{XYSeries, XYSeriesCollection}
import org.jfree.chart.{JFreeChart, ChartPanel, ChartFactory}
import org.jfree.chart.plot.PlotOrientation
object ML_Statistics
{
/* properties */
val Now = new Properties.Double("now")
def now(props: Properties.T): Double = Now.unapply(props).get
/* memory status */
val Heap_Size = new Properties.Long("size_heap")
val Heap_Free = new Properties.Long("size_heap_free_last_GC")
val GC_Percent = new Properties.Int("GC_percent")
sealed case class Memory_Status(heap_size: Long, heap_free: Long, gc_percent: Int)
{
def heap_used: Long = (heap_size - heap_free) max 0
def heap_used_fraction: Double =
if (heap_size == 0) 0.0 else heap_used.toDouble / heap_size
def gc_progress: Option[Double] =
if (1 <= gc_percent && gc_percent <= 100) Some((gc_percent - 1) * 0.01) else None
}
def memory_status(props: Properties.T): Memory_Status =
{
val heap_size = Heap_Size.get(props)
val heap_free = Heap_Free.get(props)
val gc_percent = GC_Percent.get(props)
Memory_Status(heap_size, heap_free, gc_percent)
}
/* monitor process */
def monitor(pid: Long,
stats_dir: String = "",
delay: Time = Time.seconds(0.5),
consume: Properties.T => Unit = Console.println): Unit =
{
def progress_stdout(line: String): Unit =
{
val props = Library.space_explode(',', line).flatMap(Properties.Eq.unapply)
if (props.nonEmpty) consume(props)
}
val env_prefix =
if (stats_dir.isEmpty) "" else "export POLYSTATSDIR=" + Bash.string(stats_dir) + "\n"
Bash.process(env_prefix + "\"$POLYML_EXE\" -q --use src/Pure/ML/ml_statistics.ML --eval " +
Bash.string("ML_Statistics.monitor " + ML_Syntax.print_long(pid) + " " +
ML_Syntax.print_double(delay.seconds)),
cwd = Path.ISABELLE_HOME.file)
.result(progress_stdout = progress_stdout, strict = false).check
}
/* protocol handler */
class Handler extends Session.Protocol_Handler
{
private var session: Session = null
private var monitoring: Future[Unit] = Future.value(())
override def init(session: Session): Unit = synchronized
{
this.session = session
}
override def exit(): Unit = synchronized
{
session = null
monitoring.cancel()
}
private def consume(props: Properties.T): Unit = synchronized
{
if (session != null) {
val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics()))
session.runtime_statistics.post(Session.Runtime_Statistics(props1))
}
}
private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized
{
msg.properties match {
case Markup.ML_Statistics(pid, stats_dir) =>
monitoring =
Future.thread("ML_statistics") {
monitor(pid, stats_dir = stats_dir, consume = consume)
}
true
case _ => false
}
}
override val functions = List(Markup.ML_Statistics.name -> ml_statistics)
}
/* memory fields (mega bytes) */
def mem_print(x: Long): Option[String] =
if (x == 0L) None else Some(x.toString + " M")
def mem_scale(x: Long): Long = x / 1024 / 1024
def mem_field_scale(name: String, x: Double): Double =
if (heap_fields._2.contains(name) || program_fields._2.contains(name))
mem_scale(x.toLong).toDouble
else x
val CODE_SIZE = "size_code"
val STACK_SIZE = "size_stacks"
val HEAP_SIZE = "size_heap"
/* standard fields */
type Fields = (String, List[String])
val tasks_fields: Fields =
("Future tasks",
List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive",
"tasks_urgent", "tasks_total"))
val workers_fields: Fields =
("Worker threads", List("workers_total", "workers_active", "workers_waiting"))
val GC_fields: Fields =
("GCs", List("partial_GCs", "full_GCs", "share_passes"))
val heap_fields: Fields =
("Heap", List(HEAP_SIZE, "size_allocation", "size_allocation_free",
"size_heap_free_last_full_GC", "size_heap_free_last_GC"))
val program_fields: Fields =
("Program", List("size_code", "size_stacks"))
val threads_fields: Fields =
("Threads", List("threads_total", "threads_in_ML", "threads_wait_condvar",
"threads_wait_IO", "threads_wait_mutex", "threads_wait_signal"))
val time_fields: Fields =
("Time", List("time_elapsed", "time_elapsed_GC", "time_CPU", "time_GC"))
val speed_fields: Fields =
("Speed", List("speed_CPU", "speed_GC"))
private val time_speed = Map("time_CPU" -> "speed_CPU", "time_GC" -> "speed_GC")
val java_heap_fields: Fields =
("Java heap", List("java_heap_size", "java_heap_used"))
val java_thread_fields: Fields =
("Java threads", List("java_threads_total", "java_workers_total", "java_workers_active"))
val main_fields: List[Fields] =
List(heap_fields, tasks_fields, workers_fields)
val other_fields: List[Fields] =
List(threads_fields, GC_fields, program_fields, time_fields, speed_fields,
java_heap_fields, java_thread_fields)
val all_fields: List[Fields] = main_fields ::: other_fields
/* content interpretation */
final case class Entry(time: Double, data: Map[String, Double])
{
def get(field: String): Double = data.getOrElse(field, 0.0)
}
val empty: ML_Statistics = apply(Nil)
def apply(ml_statistics0: List[Properties.T], heading: String = "",
- domain: String => Boolean = (key: String) => true): ML_Statistics =
+ domain: String => Boolean = _ => true): ML_Statistics =
{
require(ml_statistics0.forall(props => Now.unapply(props).isDefined), "missing \"now\" field")
val ml_statistics = ml_statistics0.sortBy(now)
val time_start = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.head)
val duration = if (ml_statistics.isEmpty) 0.0 else now(ml_statistics.last) - time_start
val fields =
SortedSet.empty[String] ++
(for {
props <- ml_statistics.iterator
(x, _) <- props.iterator
if x != Now.name && domain(x) } yield x)
val content =
{
var last_edge = Map.empty[String, (Double, Double, Double)]
val result = new mutable.ListBuffer[ML_Statistics.Entry]
for (props <- ml_statistics) {
val time = now(props) - time_start
// rising edges -- relative speed
val speeds =
(for {
(key, value) <- props.iterator
key1 <- time_speed.get(key)
if domain(key1)
} yield {
val (x0, y0, s0) = last_edge.getOrElse(key, (0.0, 0.0, 0.0))
val x1 = time
val y1 = java.lang.Double.parseDouble(value)
val s1 = if (x1 == x0) 0.0 else (y1 - y0) / (x1 - x0)
if (y1 > y0) {
last_edge += (key -> (x1, y1, s1))
(key1, s1.toString)
}
else (key1, s0.toString)
}).toList
val data =
SortedMap.empty[String, Double] ++
(for {
(x, y) <- props.iterator ++ speeds.iterator
if x != Now.name && domain(x)
z = java.lang.Double.parseDouble(y) if z != 0.0
} yield { (x.intern, mem_field_scale(x, z)) })
result += ML_Statistics.Entry(time, data)
}
result.toList
}
new ML_Statistics(heading, fields, content, time_start, duration)
}
}
final class ML_Statistics private(
val heading: String,
val fields: Set[String],
val content: List[ML_Statistics.Entry],
val time_start: Double,
val duration: Double)
{
+ override def toString: String =
+ if (content.isEmpty) "ML_Statistics.empty"
+ else "ML_Statistics(length = " + content.length + ", fields = " + fields.size + ")"
+
+
/* content */
def maximum(field: String): Double =
content.foldLeft(0.0) { case (m, e) => m max e.get(field) }
def average(field: String): Double =
{
@tailrec def sum(t0: Double, list: List[ML_Statistics.Entry], acc: Double): Double =
list match {
case Nil => acc
case e :: es =>
val t = e.time
sum(t, es, (t - t0) * e.get(field) + acc)
}
content match {
case Nil => 0.0
case List(e) => e.get(field)
case e :: es => sum(e.time, es, 0.0) / duration
}
}
/* charts */
def update_data(data: XYSeriesCollection, selected_fields: List[String]): Unit =
{
- data.removeAllSeries
+ data.removeAllSeries()
for (field <- selected_fields) {
val series = new XYSeries(field)
content.foreach(entry => series.add(entry.time, entry.get(field)))
data.addSeries(series)
}
}
def chart(title: String, selected_fields: List[String]): JFreeChart =
{
val data = new XYSeriesCollection
update_data(data, selected_fields)
ChartFactory.createXYLineChart(title, "time", "value", data,
PlotOrientation.VERTICAL, true, true, true)
}
def chart(fields: ML_Statistics.Fields): JFreeChart =
chart(fields._1, fields._2)
def show_frames(fields: List[ML_Statistics.Fields] = ML_Statistics.main_fields): Unit =
fields.map(chart).foreach(c =>
GUI_Thread.later {
new Frame {
iconImage = GUI.isabelle_image()
title = heading
contents = Component.wrap(new ChartPanel(c))
visible = true
}
})
}