changeset 50527 2f9b5b0e388d
parent 50332 2c7479865e07
child 50528 c29af5ffe98a
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/components/README	Fri Dec 14 16:02:31 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/components/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/components/components.sha1 contains SHA1 identifiers
+within the Isabelle repository, for integrity checking of the archives
+that are exposed to the public file-system.  The script
+Admin/components/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.