[isabelle-dev] Nominal and FinFuns from the AFP

[Makarius]

On Fri, 11 May 2012, Andreas Lochbihler wrote:

> Now, matters are different and -- as Lukas has pointed out -- I now have 
> write access to the Isabelle distribution, so there are no reasons for 
> not moving it to the AFP.

You have administrative push-access, which is much more than write access. 
This implies certain responsiblities and extra care.  Some of this is 
explained in README_REPOSITORY.


More generally, the deeper question behind the AFP/FunFun question is how 
to organize a scalable library of formalizations that are both stable and 
alive, i.e. changed continuosly.  Moving things to the main Isabelle 
repository means it is not really scalable to big things with many 
contributors.  It only works for individuals who are hooked on the 
"latest" repository version of Isabelle on their laptop.


> Moreover, Gerwin can then finally test the subsumed marker of the AFP

I don't understand the sentence.  Anyway, Gerwin did not explain any plan 
for publishing AFP for Isabelle2012 yet.  It could be started now, since 
the main release branch is practically stable.


 	Makarius