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

[Makarius]

On Tue, 26 Jun 2012, Florian Haftmann wrote:

> * Will the idea of platform-universal components revived?  If yes, the
> platform-sensitive components files can be discontinued.  I personally
> like the idea, though?

You are doing this in Isabelle/f06697f776b0 with ML_PLATFORM, but this is 
way has been long obsolete.  Many years ago, the ML system was the only 
platform specific thing, and its platform identifier was re-used for some 
time for other add on tools. Around 2009/2010 I've revised this scheme, as 
explained in Admin/PLATFORMS.  But that is already outdated again, and I 
will have to revise it once more based on the experience that I've gained 
together with Jasmin for Isabelle2011-1 and Isabelle2012.

The problem is that modern operating systems suffer from a 
multi-personality problem.  There is not "the" platform that you are 
running on, but every framework might have its own platform: ML, JVM, the 
settings environment (e.g. native windows vs. cygwin), certain tools.
So our classic universal component idea was already right, because it is 
then up to the component settings to work out the details of the platform.


> * How to deal with the non-free components?  Once a solution is found
> there, components can be required strictly, not liberal.
> * Cleanup and maintainance of nfsbroy:/home/isabelle/contrib

We now have several component directories, which is the real one?

   /home/isabelle/contrib                #haftmann
   /home/isabelle/contrib_devel          #haftmann
   /home/isabelle/public_components      #krauss
   /home/isabelle/website-Isabelle2012/dist/contrib  #wenzelm (official release)

If the naming scheme for components is taken with care, we should be able 
to have just /home/isabelle/contrib with monotonic addition of new 
versions as they emerge.  (Overwriting with same name only for equivalent 
components; otherwise by adding funny -1, -2, -3 suffixes for the 
different "builds", only where this is really needed.)

The isatest/mira jobs would project from that single store via 
Admin/components

Official releases project via copying the distributed components.

A pulished version of /home/isabelle/contrib (via http) would suppress 
certain things that are specified in some file as "nonfree".

Once we know where *the* component store is, I will put a universal JVM 
1.6 there.


 	Makarius