Admin/components/README
author wenzelm
Tue, 20 Apr 2021 22:53:24 +0200
changeset 73593 e60333aa18ca
parent 71335 2afdd24ff707
permissions -rw-r--r--
proper use of antiquotations;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69429
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
     1
Notes on maintaining the Isabelle component repository at TUM
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
     2
=============================================================
50332
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     3
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     4
Quick reference
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     5
---------------
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
     6
69429
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
     7
  * ensure that Isabelle/Scala/SSH can connect to the host specified via
71335
2afdd24ff707 improved Markdown-like display in Phabricator;
wenzelm
parents: 69429
diff changeset
     8
    system option `isabelle_components_server`; this may require to install
69429
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
     9
    an unencrypted ssh host key as follows:
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    10
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    11
      $ ssh-keyscan -t rsa lxbroy10.informatik.tu-muenchen.de >> ~/.ssh/known_hosts
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    12
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    13
  * local setup (and test) of component directory, e.g. in
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    14
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    15
      screwdriver-3.14/
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    16
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    17
  * packaging (with associated SHA1 digest), e.g.
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    18
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    19
      $ isabelle build_components screwdriver-3.14
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    20
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    21
  * publishing, e.g.
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    22
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    23
      $ isabelle build_components -P screwdriver-3.14.tar.gz
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    24
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    25
  * manual editing of Admin/components/main: screwdriver-3.14
50332
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    26
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    27
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    28
Unique names
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    29
------------
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    30
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    31
Component names are globally unique over time and space: names of
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    32
published components are never re-used.  If some component needs to be
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    33
re-packaged, extra indices may be added to the official version number
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    34
like this:
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    35
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    36
  screwdriver-3.14    #default packaging/publishing, no index
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    37
  screwdriver-3.14-1  #another refinement of the same
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    38
  screwdriver-3.14-2  #yet another refinement of the same
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    39
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    40
There is no standard format for the structure of component names: they
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    41
are compared for equality only, without any guess at an ordering.
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    42
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    43
Components are registered in Admin/components/main (or similar) for
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    44
use of that particular Isabelle repository version, subject to regular
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    45
Mercurial history.  This allows to bisect Isabelle versions with full
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    46
record of the required components for testing.
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    47
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    48
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    49
Authentic archives
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    50
------------------
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    51
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    52
Isabelle components are managed as authentic .tar.gz archives in
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    53
/home/isabelle/components from where they are made publicly available
68649
f849fc1cb65e prefer HTTPS;
wenzelm
parents: 50529
diff changeset
    54
on https://isabelle.in.tum.de/components/.
50332
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    55
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    56
Visibility on the HTTP server depends on local Unix file permission:
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    57
nonfree components should omit "read" mode for the Unix group/other;
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    58
regular components should be world-readable.
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    59
71335
2afdd24ff707 improved Markdown-like display in Phabricator;
wenzelm
parents: 69429
diff changeset
    60
The file `Admin/components/components.sha1` contains SHA1 identifiers
50527
2f9b5b0e388d just one Admin/components/ directory;
wenzelm
parents: 50332
diff changeset
    61
within the Isabelle repository, for integrity checking of the archives
69429
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    62
that are exposed to the public file-system.  The command-line tool
71335
2afdd24ff707 improved Markdown-like display in Phabricator;
wenzelm
parents: 69429
diff changeset
    63
`isabelle build_components` maintains these hash-keys automatically.
50332
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    64
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    65
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    66
Unpacked copy
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    67
-------------
2c7479865e07 some notes on the Isabelle component repository at TUM;
wenzelm
parents:
diff changeset
    68
71335
2afdd24ff707 improved Markdown-like display in Phabricator;
wenzelm
parents: 69429
diff changeset
    69
A second unpacked copy is provided in `/home/isabelle/contrib/`. This allows
69429
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    70
users and administrative services within the TUM network to activate arbitrary
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    71
snapshots of the repository with all standard components being available,
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    72
without extra copying or unpacking of the authentic archives. The
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    73
isabelle_cronjob does this routinely: it will break if the unpacked version is
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    74
omitted.
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    75
71335
2afdd24ff707 improved Markdown-like display in Phabricator;
wenzelm
parents: 69429
diff changeset
    76
The command-line tool `isabelle build_components -P` takes care of uploading
69429
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    77
the .tar.gz archive and unpacking it, unless it is a special component (e.g.
dc5fbcb07c7b replaced "isabelle components_checksum" shell script by "isabelle build_components" in Scala, with more functionality;
wenzelm
parents: 68649
diff changeset
    78
for multiplatform application bundling).