author wenzelm
Sat, 08 Dec 2018 22:31:34 +0100
changeset 69429 dc5fbcb07c7b
parent 68649 f849fc1cb65e
child 71335 2afdd24ff707
permissions -rw-r--r--
replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality; more robust Component.Archive name: avoid rm_tree accidents;

Notes on maintaining the Isabelle component repository at TUM

Quick reference

  * 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 >> ~/.ssh/known_hosts

  * local setup (and test) of component directory, e.g. in


  * 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

Component names are globally unique over time and space: names of
published components are never re-used.  If some component needs to be
re-packaged, extra indices may be added to the official version number
like this:

  screwdriver-3.14    #default packaging/publishing, no index
  screwdriver-3.14-1  #another refinement of the same
  screwdriver-3.14-2  #yet another refinement of the same

There is no standard format for the structure of component names: they
are compared for equality only, without any guess at an ordering.

Components are registered in Admin/components/main (or similar) for
use of that particular Isabelle repository version, subject to regular
Mercurial history.  This allows to bisect Isabelle versions with full
record of the required components for testing.

Authentic archives

Isabelle components are managed as authentic .tar.gz archives in
/home/isabelle/components from where they are made publicly available

Visibility on the HTTP server depends on local Unix file permission:
nonfree components should omit "read" mode for the Unix group/other;
regular components should be world-readable.

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 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 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

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).