[isabelle-dev] Isabelle and AFP
florian.haftmann at informatik.tu-muenchen.de
Wed Aug 17 21:18:49 CEST 2011
I repeatedly stumble over duplication among the Isabelle distribution
and the AFP, c.f.
(btw. it took me considerable time to figure out how the class hierarchy
for complete lattices should look like, just to see now that somebody
else got to the same conclusion independently already).
Can we somehow avoid this? The AFP is now creeping towards hundred
entries, which indeed is a success, but also raises new questions
concerning maintainance. How can we ensure that generic
»Preliminaries«, »Basics« or »Fundamentals« etc. can be incorporated
into the distribution, leading to more reuse? I guess neither the
editors nor the submitters can be burdened with such a task alone, the
editors for purely economical reasons, the submitters since their
knowledge about the Isabelle distribution theories is usually not that
intimate. But could there be a process to get more people involved,
e.g. by introducing generic parts of AFP submissions on the dev (or even
user) mailing list, to encourage discussion (and hopefully subsequent
action, and also awareness)?
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev