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,886 @@ /* Title: Pure/Admin/build_release.scala Author: Makarius Build full Isabelle distribution from repository. */ package isabelle object Build_Release { - /** release info **/ + /** release context **/ + + 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 + Path.explode(dist_name + ".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_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): Release_Archive = + { + Isabelle_System.with_tmp_dir("tmp")(dir => + Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => + { + Bytes.write(archive_path, bytes) + Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path), + dir = dir, original_owner = true, strip = 1).check - def other_isabelle(dir: Path): Other_Isabelle = - Other_Isabelle(dir + isabelle, - isabelle_identifier = dist_name + "-build", - progress = progress) + val id = File.read(dir + ISABELLE_ID) + val tags = File.read(dir + ISABELLE_TAGS) + val identifier = File.read(dir + ISABELLE_IDENTIFIER) + new Release_Archive(bytes, id, tags, identifier) + }) + ) + } - 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") - } + def read(path: Path): Release_Archive = make(Bytes.read(path)) + } + + 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 build_release_archive( + context: Release_Context, + version: String, + parallel_jobs: Int = 1): Release_Archive = { - 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 progress = context.progress - 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) - } - - - /* make distribution */ + 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 (release.isabelle_archive.is_file) { - progress.echo_warning("Release archive already exists: " + release.isabelle_archive) + if (context.isabelle_archive.is_file) { + progress.echo_warning("Found existing release archive: " + context.isabelle_archive) - 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) - }) - - if (release.ident != archive_ident) { - error("Mismatch of release identification " + release.ident + - " vs. archive " + archive_ident) - } + val archive = Release_Archive.read(context.isabelle_archive) + if (id == archive.id) archive + else error("Mismatch of release identification " + id + " vs. archive " + archive.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" + Release_Archive.read(context.isabelle_archive) + } + } -rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle + def build_release( + options: Options, + context: Release_Context, + release_archive: Release_Archive, + 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 -rf "${DIST_NAME}-old" -""") + + /* release directory */ + + for (name <- List(context.dist_name, "Isabelle")) { + Isabelle_System.rm_tree(context.dist_dir + Path.explode(name)) } + Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => + { + Bytes.write(archive_path, release_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 + Path.explode("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, release_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(release_archive.id), + HTML.text("Isabelle/" + release_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.section(context.dist_name), HTML.subsection("Platforms"), HTML.itemize( website_platform_bundles.map({ case (bundle, bundle_info) => List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })), 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.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 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 -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) 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), "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() + val context = + Release_Context(target_dir, + release_name = release_name, + components_base = components_base, + 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, + val version = proper_string(rev) orElse proper_string(release_name) getOrElse "tip" + val release_archive = build_release_archive(context, version, parallel_jobs = parallel_jobs) + + build_release(options, context, release_archive, afp_rev = afp_rev, platform_families = if (platform_families.isEmpty) default_platform_families else 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) + val release_archive = Build_Release.build_release_archive(context, rev) + Build_Release.build_release(options, context, release_archive, 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 } }