README
1Some notes on maintaining the Isabelle component repository at TUM
2==================================================================
3
4Quick reference
5---------------
6
7 $ install /home/isabelle/components/screwdriver-3.14.tar.gz
8 $ install /home/isabelle/contrib/screwdriver-3.14/
9 $ edit Admin/components/main: screwdriver-3.14
10 $ isabelle components_checksum -u
11 $ hg diff
12 $ hg commit
13
14
15Unique names
16------------
17
18Component names are globally unique over time and space: names of
19published components are never re-used. If some component needs to be
20re-packaged, extra indices may be added to the official version number
21like this:
22
23 screwdriver-3.14 #default packaging/publishing, no index
24 screwdriver-3.14-1 #another refinement of the same
25 screwdriver-3.14-2 #yet another refinement of the same
26
27There is no standard format for the structure of component names: they
28are compared for equality only, without any guess at an ordering.
29
30Components are registered in Admin/components/main (or similar) for
31use of that particular Isabelle repository version, subject to regular
32Mercurial history. This allows to bisect Isabelle versions with full
33record of the required components for testing.
34
35
36Authentic archives
37------------------
38
39Isabelle components are managed as authentic .tar.gz archives in
40/home/isabelle/components from where they are made publicly available
41on https://isabelle.in.tum.de/components/.
42
43Visibility on the HTTP server depends on local Unix file permission:
44nonfree components should omit "read" mode for the Unix group/other;
45regular components should be world-readable.
46
47The file Admin/components/components.sha1 contains SHA1 identifiers
48within the Isabelle repository, for integrity checking of the archives
49that are exposed to the public file-system. The components_checksum
50tool helps to update these hash-keys wrt. the information within the
51Isabelle repository.
52
53
54Unpacked copy
55-------------
56
57A second unpacked copy is provided in /home/isabelle/contrib/. This
58allows users within the TUM network to activate arbitrary snapshots of
59the repository with all standard components being available, without
60extra copying or unpacking of the authentic archives. Testing
61services like "isatest" and "mira" do this routinely, and will break
62accordingly if this is omitted.
63