[isabelle-dev] Standard component setup (Re: NEWS)

Makarius makarius at sketis.net
Wed Jan 11 23:31:15 CET 2012


On Wed, 11 Jan 2012, Alexander Krauss wrote:

> * Components live in /home/isabelle/public_components as tarballs. The
> directory is regarded as append-only, possibly with infrequent garbage
> collection, which moves outdated packages to some archive location.
> The packages should be files, not symlinks (to make the directory more 
> self-contained)
> I'll volunteer to provide the initial content based on contrib_devel and 
> other sources, if people agree with the general idea.

This sounds fine to me, if this really observes the current standard 
naming conventions that can be now seen in 
/home/isabelle/dist/dist-Isabelle2011-1/contrib for example.

In particular: no aliases on names, versions, compression formats.  (The 
Admin scripts for bundling really expect foo.tar.gz not foo.tgz etc.)

(For historical reasons there are still some special tricks for polyml and 
ProofGeneral, but this is about to become more conformant at a later 
stage.)


> * The directory is accessible, cf. 
> http://isabelle.in.tum.de/devel/components As the path indicates, this 
> is mainly for developers. There could be a script in Admin/ that helps 
> to bootstrap the local clone from this source.

We could go one step further and call this 
http://isabelle.in.tum.de/contrib/

With explicit version information for the components, it could be shared 
between official releases and non-releases.  But this also means one needs 
to refrain from repackaging existing things under the same name-version. 
(Classic RPM naming conventions add another -NNN suffix for the package 
sequence number, but I would like to avoid this.)


> The above gives us a poor man's repository with several advantages over 
> the current state
>
> - single place to look for stuff
> - uniform usage (download, untar, init_component, that's it.)

Isabelle/Scala already can download and untar, so it is getting pretty 
close to some more formal component repository with minimal efforts.

At the same time the above scheme allows people to assemble things by hand 
for Isabelle repository clones right now.


 	Makarius



More information about the isabelle-dev mailing list