On Sun, 1 Jul 2012, Alexander Krauss wrote:
So here is my latest low-tech proposal:
* /home/isabelle/components is the components repository, where all
components are stored. They are stored as tarballs.
* The existing php script can be used to serve this directory via HTTP.
* Non-free components are marked as such simply via file permissions, i.e.,
by having the world-readable flag unset. Since Apache runs under group
"isabelle", we might have to set the group to something else (e.g., an
imagined "isabelle-admin").
* Integrity of this directory is ensured by a cron job which compares the
output of "sha1sum /home/isabelle/components/*" with a file
in the Admin section of the Isabelle repository. So we can easily detect
accidents (and revert them, possibly with the help of the standard backups).
Such a script is easy to write, and I already have
some fragments lying around here.
* /home/isabelle/contrib is maintained automatically by unpacking the
contents of the tarballs (and setting permissions properly).
* A similar script in Admin/ can download components via HTTP and link them
into a clone of the Isabelle repository.
I would say that 30 lines of bash will do. And additional 30 lines of a
README, which goes into the same directory.
This is now converging to a very reasonable scheme. I also prefer to
archive official .tar.gz now, since permissions of individual files in the
file-system are often mangled. (There was another incident just last
week.)
BTW, when there is a robust script to download .tar.gz components on
demand and unpack them for the user, we could even discontinue the
/home/isabelle/contrib/ thing -- /home/tmp/USER provides cheap temporary
disk space for private copies of it, also for mira and isatest. Most
regular users are non-local anyway, using their laptop etc.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
