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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
