Some notes on maintaining 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 $ isabelle components_checksum -u $ hg diff $ hg commitUnique names------------Component names are globally unique over time and space: names ofpublished components are never re-used. If some component needs to bere-packaged, extra indices may be added to the official version numberlike 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 sameThere is no standard format for the structure of component names: theyare compared for equality only, without any guess at an ordering.Components are registered in Admin/components/main (or similar) foruse of that particular Isabelle repository version, subject to regularMercurial history. This allows to bisect Isabelle versions with fullrecord 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 availableon 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/components/components.sha1 contains SHA1 identifierswithin the Isabelle repository, for integrity checking of the archivesthat are exposed to the public file-system. The components_checksumtool helps to update these hash-keys wrt. the information within theIsabelle repository.Unpacked copy-------------A second unpacked copy is provided in /home/isabelle/contrib/. Thisallows users within the TUM network to activate arbitrary snapshots ofthe repository with all standard components being available, withoutextra copying or unpacking of the authentic archives. Testingservices like "isatest" and "mira" do this routinely, and will breakaccordingly if this is omitted.