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