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

[Alexander Krauss]

On 05/29/2012 02:01 PM, Makarius wrote:
> * 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.

See my previous description on this list:

http://article.gmane.org/gmane.science.mathematics.logic.isabelle.devel/1316/

Of course, we can adapt this scheme if the conventions change, but to me 
it seems that it is perfectly compatible with your suggested scheme.

Note that mira does not use the symlink from /home/isabelle/contrib to 
contrib_devel. So there should be nothing in against replacing it with a 
freshly assembled, authentic, and symlink-free copy. The old 
contrib_devel can then remain as it is for a few months until issues are 
sorted out, but not longer.

To me, the main unsolved problem is the fact that components are no 
longer universal but depend on the platform. So our scheme must 
accommodate this somehow and the fact that it currently doesn't is the 
main source of the recent confusion. Here are some possibilies:

a) Subdirectories for each platform

   /home/isabelle/contrib/
     x86-linux/
     x86_64-linux/
     x86-cygwin/
     ...

   Then, the universal component packages must be copied, symlinked or
   hardlinked.

b) Different packages for different platforms, roughly as it is now...

   /home/isabelle/contrib/
     jdk-6u31_x86_64-linux/
     jdk-6u31_x86-linux/

   Then we need a /Admin/contributed_components file for each
   platform, which lists the components relevant for that platform.


My gut feeling is that version a) is slightly cleaner, but I'd be happy 
witch both variants.

When this structure is in place, more conveniences as pointed out by 
Florian can be considered as needed.

Alex