some notes on the Isabelle component repository at TUM;
Mon, 03 Dec 2012 20:43:40 +0100
changeset 50332 2c7479865e07
parent 50331 4b6dc5077e98
child 50333 20c69b00e73c
some notes on the Isabelle component repository at TUM;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/component_repository/README	Mon Dec 03 20:43:40 2012 +0100
@@ -0,0 +1,62 @@
+Some notes on the Isabelle component repository at TUM
+Quick reference
+  $ install /home/isabelle/components/screwdriver-3.14.tar.gz
+  $ install /home/isabelle/contrib/screwdriver-3.14/
+  $ edit Admin/components/main: screwdriver-3.14
+  $ run Admin/component_repository/checksum -u
+  $ hg diff
+  $ hg commit
+Unique names
+Component names are globally unique over time and space: names of
+published components are never re-used.  If some component needs to be
+re-packaged, extra indices may be added to the official version number
+like this:
+  screwdriver-3.14    #default packaging/publishing, no index
+  screwdriver-3.14-1  #another refinement of the same
+  screwdriver-3.14-2  #yet another refinement of the same
+There is no standard format for the structure of component names: they
+are compared for equality only, without any guess at an ordering.
+Components are registered in Admin/components/main (or similar) for
+use of that particular Isabelle repository version, subject to regular
+Mercurial history.  This allows to bisect Isabelle versions with full
+record of the required components for testing.
+Authentic archives
+Isabelle components are managed as authentic .tar.gz archives in
+/home/isabelle/components from where they are made publicly available
+Visibility on the HTTP server depends on local Unix file permission:
+nonfree components should omit "read" mode for the Unix group/other;
+regular components should be world-readable.
+The file Admin/component_repository/contains SHA1 identifiers within
+the Isabelle repository, for integrity checking of the archives that
+are exposed to the public file-system.  The script
+Admin/component_repository/checksum helps to update these hash-keys
+wrt. the information within the Isabelle repository.
+Unpacked copy
+A second unpacked copy is provided in /home/isabelle/contrib/.  This
+allows users within the TUM network to activate arbitrary snapshots of
+the repository with all standard components being available, without
+extra copying or unpacking of the authentic archives.  Testing
+services like "isatest" and "mira" do this routinely, and will break
+accordingly if this is omitted.