author | wenzelm |
Fri, 29 Oct 2021 19:43:32 +0200 | |
changeset 74627 | c690435c47ee |
parent 71335 | 2afdd24ff707 |
child 76153 | bf9f2f4069b9 |
permissions | -rw-r--r-- |
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 | 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 | 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 | 60 |
The file `Admin/components/components.sha1` contains SHA1 identifiers |
50527 | 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 | 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 | 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 | 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). |