# HG changeset patch # User wenzelm # Date 1354563820 -3600 # Node ID 2c7479865e07f441ea0d1f68bf10b872f06f046c # Parent 4b6dc5077e98868379aafcbc8db45567fe105f75 some notes on the Isabelle component repository at TUM; diff -r 4b6dc5077e98 -r 2c7479865e07 Admin/component_repository/README --- /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 +on http://isabelle.in.tum.de/components/. + +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.