[isabelle-dev] Future and maintainance of ~isabelle/contrib_devel at TUM NFS
makarius at sketis.net
Wed Jun 27 13:32:37 CEST 2012
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/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
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
More information about the isabelle-dev