| author | wenzelm | 
| Tue, 08 Mar 2016 11:18:21 +0100 | |
| changeset 62555 | fd6e64133684 | 
| parent 50529 | b2aa899b3f2d | 
| child 68649 | f849fc1cb65e | 
| permissions | -rw-r--r-- | 
| 50529 | 1 | Some notes on maintaining the Isabelle component repository at TUM | 
| 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 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 7 | $ install /home/isabelle/components/screwdriver-3.14.tar.gz | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 8 | $ install /home/isabelle/contrib/screwdriver-3.14/ | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 9 | $ edit Admin/components/main: screwdriver-3.14 | 
| 50528 | 10 | $ isabelle components_checksum -u | 
| 50332 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 11 | $ hg diff | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 12 | $ hg commit | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 13 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 14 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 15 | Unique names | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 16 | ------------ | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 17 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 18 | 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 | 19 | 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 | 20 | 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 | 21 | like this: | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 22 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 23 | screwdriver-3.14 #default packaging/publishing, no index | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 24 | screwdriver-3.14-1 #another refinement of the same | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 25 | screwdriver-3.14-2 #yet another refinement of the same | 
| 
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 | 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 | 28 | 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 | 29 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 30 | Components are registered in Admin/components/main (or similar) for | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 31 | use of that particular Isabelle repository version, subject to regular | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 32 | Mercurial history. This allows to bisect Isabelle versions with full | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 33 | record of the required components for testing. | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 34 | |
| 
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 | Authentic archives | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 37 | ------------------ | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 38 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 39 | Isabelle components are managed as authentic .tar.gz archives in | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 40 | /home/isabelle/components from where they are made publicly available | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 41 | on http://isabelle.in.tum.de/components/. | 
| 
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 | 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 | 44 | 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 | 45 | regular components should be world-readable. | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 46 | |
| 50527 | 47 | The file Admin/components/components.sha1 contains SHA1 identifiers | 
| 48 | within the Isabelle repository, for integrity checking of the archives | |
| 50528 | 49 | that are exposed to the public file-system. The components_checksum | 
| 50 | tool helps to update these hash-keys wrt. the information within the | |
| 51 | Isabelle repository. | |
| 50332 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 52 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 53 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 54 | Unpacked copy | 
| 
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 | |
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 57 | A second unpacked copy is provided in /home/isabelle/contrib/. This | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 58 | allows users within the TUM network to activate arbitrary snapshots of | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 59 | the repository with all standard components being available, without | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 60 | extra copying or unpacking of the authentic archives. Testing | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 61 | services like "isatest" and "mira" do this routinely, and will break | 
| 
2c7479865e07
some notes on the Isabelle component repository at TUM;
 wenzelm parents: diff
changeset | 62 | accordingly if this is omitted. |