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

[Makarius]

On Sun, 27 May 2012, Florian Haftmann wrote:

> for years now, there was a silent convention that 
> ~isabelle/contrib_devel at the TUM NFS would contain references to 
> more-or-less up-to-date add-on components for Isabelle.  Is there 
> currently anybody still doing maintainance there?  Also, the local 
> Isabelle2012 distribution in ~isabelle/Isabelle2012 is not equipped with 
> any of the add-on components shipped with the distribution on the 
> website, e.g. there seems to be no readily usable Haskabelle2012 beneath 
> ~isabelle.
>
> What are users of Isabelle at the local TUM infrastructure (e.g. remote 
> runs on the macbroyXY machines) supposed to do?  Private installations? 
> Further, how to include the add-on components?  Currently I use special 
> ~/.isabelle/etc/settings for this, but maybe there is something more 
> direct?
>
> After all those years, I think we should agree upon (again) how we (i.e. 
> all those using Isabelle from TUM NFS) deal with all those issues.  For 
> such central issues I don't believe in private-only solutions.  Or does 
> meanwhile everybody use the testboard?

On Mon, 28 May 2012, Jasmin Christian Blanchette wrote:

>> A first step would be that the add-on components shipped with the 
>> current distribution are also available by NFS.
>
> I'm surprised they were taken out. They used to be there for 
> Isabelle2011-1.

I first intended to do the same as for Isabelle2011-1, but then realized 
that Isabelle2012 had diverged further from the old "universal" scheme of 
add-on packages: more and more components are specific for one of the 
platform families (linux, darwin, cygwin), and would have required some 
extra fiddling to put them all into one place and activate uniformly.

Moreover, my impression was that the role of the different contrib 
directories needs some rethinking anyway, which is what we are doing right 
now on this thread. There has always been a bit of chaos here, without 
grand-unified structure.  It does not mean we should not try again to get 
one.

Taking the current situation as a starting point, one could do the 
following:

   * /home/isabelle/contrib contains various add-on components cumulatively
     with explicit version information and without funny symlinks to other
     versions.

   * /home/isabelle/contrib_devel is discontinued, it is superseded by a
     cleaned version of contrib above; right now there is a symlink contrib
     -> contrib_devel anyway.

   * Admin/contributed_components within the repository documents
     semi-formally which components may be included into a certain version.

     The mira experts should be able to say more about the current used of
     that file in the testing framework.

We shall also need to make an effort to keep /home/isabelle/contrib 
up-to-date.  There is quite some divergence wrt. Isabelle2011-1 and 
Isabelle2012 right now.


 	Makarius