replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
more robust Component.Archive name: avoid rm_tree accidents;
--- 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).
--- /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"
--- 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"
-}
--- 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)
+ })
}
--- 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)