[isabelle-dev] Isabelle and AFP

[Florian Haftmann]

Hi all,

I repeatedly stumble over duplication among the Isabelle distribution
and the AFP, c.f.

Library/AssocList.thy
and
http://afp.hg.sourceforge.net/hgweb/afp/afp/file/dce6fbc4d6c0/thys/BytecodeLogicJmlTypes/AssocLists.thy

Complete_Lattices.thy
and
http://afp.hg.sourceforge.net/hgweb/afp/afp/file/dce6fbc4d6c0/thys/DataRefinementIBP/Preliminaries.thy
(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)?

Cheers,
    Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110817/28086d5e/attachment.asc>