# HG changeset patch # User wenzelm # Date 1544304694 -3600 # Node ID dc5fbcb07c7b67788f5fcc64f893b138aa4ce7e1 # Parent 38ad311912105074e9cfa7eb916afc3a9d094cf5 replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality; more robust Component.Archive name: avoid rm_tree accidents; diff -r 38ad31191210 -r dc5fbcb07c7b Admin/components/README --- a/Admin/components/README Sat Dec 08 21:21:14 2018 +0100 +++ b/Admin/components/README Sat Dec 08 22:31:34 2018 +0100 @@ -1,15 +1,28 @@ -Some notes on maintaining the Isabelle component repository at TUM -================================================================== +Notes on maintaining the Isabelle component repository at TUM +============================================================= Quick reference --------------- - $ install /home/isabelle/components/screwdriver-3.14.tar.gz - $ install /home/isabelle/contrib/screwdriver-3.14/ - $ edit Admin/components/main: screwdriver-3.14 - $ isabelle components_checksum -u - $ hg diff - $ hg commit + * ensure that Isabelle/Scala/SSH can connect to the host specified via + system option "isabelle_components_server"; this may require to install + an unencrypted ssh host key as follows: + + $ ssh-keyscan -t rsa lxbroy10.informatik.tu-muenchen.de >> ~/.ssh/known_hosts + + * local setup (and test) of component directory, e.g. in + + screwdriver-3.14/ + + * packaging (with associated SHA1 digest), e.g. + + $ isabelle build_components screwdriver-3.14 + + * publishing, e.g. + + $ isabelle build_components -P screwdriver-3.14.tar.gz + + * manual editing of Admin/components/main: screwdriver-3.14 Unique names @@ -46,17 +59,20 @@ The file Admin/components/components.sha1 contains SHA1 identifiers within the Isabelle repository, for integrity checking of the archives -that are exposed to the public file-system. The components_checksum -tool helps to update these hash-keys wrt. the information within the -Isabelle repository. +that are exposed to the public file-system. The command-line tool +"isabelle build_components" maintains these hash-keys automatically. Unpacked copy ------------- -A second unpacked copy is provided in /home/isabelle/contrib/. This -allows users within the TUM network to activate arbitrary snapshots of -the repository with all standard components being available, without -extra copying or unpacking of the authentic archives. Testing -services like "isatest" and "mira" do this routinely, and will break -accordingly if this is omitted. +A second unpacked copy is provided in /home/isabelle/contrib/. This allows +users and administrative services within the TUM network to activate arbitrary +snapshots of the repository with all standard components being available, +without extra copying or unpacking of the authentic archives. The +isabelle_cronjob does this routinely: it will break if the unpacked version is +omitted. + +The command-line tool "isabelle build_components -P" takes care of uploading +the .tar.gz archive and unpacking it, unless it is a special component (e.g. +for multiplatform application bundling). diff -r 38ad31191210 -r dc5fbcb07c7b Admin/etc/options --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/etc/options Sat Dec 08 22:31:34 2018 +0100 @@ -0,0 +1,12 @@ +(* :mode=isabelle-options: *) + +section "Admin tools" + +option isabelle_components_server : string = "lxbroy10.informatik.tu-muenchen.de" + -- "user@host for SSH connection" + +option isabelle_components_dir : string = "/home/isabelle/components" + -- "webspace for ISABELLE_COMPONENT_REPOSITORY" + +option isabelle_components_contrib_dir : string = "/home/isabelle/contrib" + -- "unpacked components for remote build services" diff -r 38ad31191210 -r dc5fbcb07c7b Admin/lib/Tools/components_checksum --- a/Admin/lib/Tools/components_checksum Sat Dec 08 21:21:14 2018 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -#!/usr/bin/env bash -# -# Author: Alexander Krauss -# -# DESCRIPTION: compute and validate checksums for component repository - - -## diagnostics - -PRG="$(basename "$0")" - -function usage() -{ - echo - echo "Usage: $PRG [OPTIONS] [DIR]" - echo - echo " Options are:" - echo " -u update the recorded checksums in the repository" - echo " -c compare the actual checksums with the recorded ones" - echo - echo " Compute the checksums of component .tar.gz archives in DIR" - echo " (default \"/home/isabelle/components\") and synchronize them" - echo " with the Isabelle repository." - echo - exit 1 -} - -function fail() -{ - echo "$1" >&2 - exit 2 -} - - -## process command line - -# options - -UPDATE="" -CHECK="" -COMPONENTS_DIR="/home/isabelle/components" - -while getopts "uc" OPT -do - case "$OPT" in - u) - UPDATE=true - ;; - c) - CHECK=true - ;; - esac -done - -shift $(($OPTIND - 1)) - -[ -n "$UPDATE" ] || [ -n "$CHECK" ] || usage - - -# args - -[ "$#" -ge 1 ] && { COMPONENTS_DIR="$1"; shift; } -[ "$#" -ne 0 ] && usage - - -## compute checksums - -CHECKSUM_DIR="$ISABELLE_HOME/Admin/components" -CHECKSUM_FILE="$CHECKSUM_DIR/components.sha1" -CHECKSUM_TMP="$CHECKSUM_DIR/components.sha1.tmp" - -( - cd "$COMPONENTS_DIR" - sha1sum *.tar.gz | sort -k2 -f > "$CHECKSUM_TMP" -) - -[ -n "$UPDATE" ] && mv "$CHECKSUM_TMP" "$CHECKSUM_FILE" -[ -n "$CHECK" ] && { - diff "$CHECKSUM_FILE" "$CHECKSUM_TMP" || fail "Integrity error" -} diff -r 38ad31191210 -r dc5fbcb07c7b src/Pure/Admin/components.scala --- a/src/Pure/Admin/components.scala Sat Dec 08 21:21:14 2018 +0100 +++ b/src/Pure/Admin/components.scala Sat Dec 08 22:31:34 2018 +0100 @@ -17,8 +17,19 @@ object Archive { val suffix: String = ".tar.gz" - def apply(name: String): String = name + suffix - def unapply(archive: String): Option[String] = Library.try_unsuffix(suffix, archive) + + def apply(name: String): String = + if (name == "") error("Bad component name: " + quote(name)) + else name + suffix + + def unapply(archive: String): Option[String] = + { + for { + name0 <- Library.try_unsuffix(suffix, archive) + name <- proper_string(name0) + } yield name + } + def get_name(archive: String): String = unapply(archive) getOrElse error("Bad component archive name (expecting .tar.gz): " + quote(archive)) @@ -76,8 +87,8 @@ /* component directory content */ - def settings(dir: Path): Path = dir + Path.explode("etc/settings") - def components(dir: Path): Path = dir + Path.explode("etc/components") + def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings") + def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components") def check_dir(dir: Path): Boolean = settings(dir).is_file || components(dir).is_file @@ -87,4 +98,196 @@ def write_components(dir: Path, lines: List[String]): Unit = File.write(components(dir), terminate_lines(lines)) + + + /* component repository content */ + + val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") + + sealed case class SHA1_Digest(sha1: String, file_name: String) + { + override def toString: String = sha1 + " " + file_name + } + + def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] = + (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line => + Word.explode(line) match { + case Nil => None + case List(sha1, name) => Some(SHA1_Digest(sha1, name)) + case _ => error("Bad components.sha1 entry: " + quote(line)) + }) + + def write_components_sha1(entries: List[SHA1_Digest]) = + File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n")) + + + + /** build and publish components **/ + + def build_components( + options: Options, + components: List[Path], + progress: Progress = No_Progress, + publish: Boolean = false, + force: Boolean = false, + update_components_sha1: Boolean = false) + { + val archives: List[Path] = + for (path <- components) yield { + path.file_name match { + case Archive(_) => path + case name => + if (!path.is_dir) error("Bad component directory: " + path) + else if (!check_dir(path)) { + error("Malformed component directory: " + path + + "\n (requires " + settings() + " or " + Components.components() + ")") + } + else { + val component_path = path.expand + val archive_dir = component_path.dir + val archive_name = Archive(name) + + val archive = archive_dir + Path.explode(archive_name) + if (archive.is_file && !force) { + error("Component archive already exists: " + archive) + } + + progress.echo("Packaging " + archive_name + " ...") + Isabelle_System.gnutar("-czf " + Bash.string(archive_name) + " " + Bash.string(name), + dir = archive_dir).check + + archive + } + } + } + + if ((publish && archives.nonEmpty) || update_components_sha1) { + options.string("isabelle_components_server") match { + case SSH.Target(user, host) => + using(SSH.open_session(options, host = host, user = user))(ssh => + { + val components_dir = Path.explode(options.string("isabelle_components_dir")) + val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) + + for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { + error("Bad remote directory: " + dir) + } + + if (publish) { + for (archive <- archives) { + val archive_name = archive.file_name + val name = Archive.get_name(archive_name) + val remote_component = components_dir + archive.base + val remote_contrib = contrib_dir + Path.explode(name) + + // component archive + if (ssh.is_file(remote_component) && !force) { + error("Remote component archive already exists: " + remote_component) + } + progress.echo("Uploading " + archive_name) + ssh.write_file(remote_component, archive) + + // contrib directory + val is_standard_component = + Isabelle_System.with_tmp_dir("component")(tmp_dir => + { + Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check + check_dir(tmp_dir + Path.explode(name)) + }) + if (is_standard_component) { + if (ssh.is_dir(remote_contrib)) { + if (force) ssh.rm_tree(remote_contrib) + else error("Remote component directory already exists: " + remote_contrib) + } + progress.echo("Unpacking remote " + archive_name) + ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + + ssh.bash_path(remote_component)).check + } + else { + progress.echo_warning("No unpacking of non-standard component: " + archive_name) + } + } + } + + // remote SHA1 digests + if (update_components_sha1) { + val lines = + for { + entry <- ssh.read_dir(components_dir) + if entry.is_file && entry.name.endsWith(Archive.suffix) + } + yield { + progress.echo("Digesting remote " + entry.name) + Library.trim_line( + ssh.execute("cd " + ssh.bash_path(components_dir) + + "; sha1sum " + Bash.string(entry.name)).check.out) + } + write_components_sha1(read_components_sha1(lines)) + } + }) + case s => error("Bad isabelle_components_server: " + quote(s)) + } + } + + // local SHA1 digests + { + val new_entries = + for (archive <- archives) + yield { + val file_name = archive.file_name + progress.echo("Digesting local " + file_name) + val sha1 = SHA1.digest(archive).rep + SHA1_Digest(sha1, file_name) + } + val new_names = new_entries.map(_.file_name).toSet + + write_components_sha1( + new_entries ::: + read_components_sha1().filterNot(entry => new_names.contains(entry.file_name))) + } + } + + + /* Isabelle tool wrapper */ + + private val relevant_options = + List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") + + val isabelle_tool = + Isabelle_Tool("build_components", "build and publish Isabelle components", args => + { + var publish = false + var update_components_sha1 = false + var force = false + var options = Options.init() + + def show_options: String = + cat_lines(relevant_options.map(name => options.options(name).print)) + + val getopts = Getopts(""" +Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS... + + Options are: + -P publish on SSH server (see options below) + -f force: overwrite existing component archives and directories + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -u update all SHA1 keys in Isabelle repository Admin/components + + Build and publish Isabelle components as .tar.gz archives on SSH server, + depending on system options: + +""" + Library.prefix_lines(" ", show_options) + "\n", + "P" -> (_ => publish = true), + "f" -> (_ => force = true), + "o:" -> (arg => options = options + arg), + "u" -> (_ => update_components_sha1 = true)) + + val more_args = getopts(args) + if (more_args.isEmpty && !update_components_sha1) getopts.usage() + + val progress = new Console_Progress + + build_components(options, more_args.map(Path.explode), progress = progress, + publish = publish, force = force, update_components_sha1 = update_components_sha1) + }) } diff -r 38ad31191210 -r dc5fbcb07c7b src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Sat Dec 08 21:21:14 2018 +0100 +++ b/src/Pure/System/isabelle_tool.scala Sat Dec 08 22:31:34 2018 +0100 @@ -172,4 +172,5 @@ Build_PolyML.isabelle_tool2, Build_Status.isabelle_tool, Check_Sources.isabelle_tool, + Components.isabelle_tool, isabelle.vscode.Build_VSCode.isabelle_tool)