[isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS

[Makarius]

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