Re: [isabelle] New AFP theory: List Index
Perhaps a useful model to emulate is Hackage. For those who don't know,
hackage is a website (similar to the AFP) for hosting haskell packages. One thing that
makes it so useful is the cabal utility --- somewhat like debian's apt tool --- which
allows you to download a package and all its dependencies automatically. This seems
to encourage both reuse and participation.
Whether or not this would work for the Isabelle community is debatable --- the
the haskell community is much larger. Having said that, we might be able to co-opt
some of the tech used in cabal and hackage ...
On 21/02/2010, at 6:44 AM, Tobias Nipkow wrote:
> This theory provides functions for finding the index of an element in a
> list, by predicate and by value.
> Above I have intentionally not used the word "article" but "theory" to
> emphasize that this is a small contribution (a single theory of modest
> size) - but a reusable one! I would like to use this opportunity to
> remind readers of this list of the purpose of the AFP:
> "The Archive of Formal Proofs is a collection of proof libraries,
> examples, and larger scientific developments."
> At the moment the majority of contributions are large (sometimes
> impressively so), monolithic developments. Very rarely are parts of such
> developments reused elsewhere. That is, the library aspect is
> underdeveloped. The above theory "List Index" used to be hidden in the
> article "Jinja is not Java" and I have (after 5 years!) finally gotten
> around to making it a separate contribution.
> This is a call for reusable AFP entries. I am sure many of you have such
> theories hidden away in their drawers (or their AFP entries): Do take
> the time to polish and submit them to the AFP (or refactor some existing
> AFP article), for the benefit of the whole community (and your fame).
> Don't think publication, think reuse!
> Sorry about getting carried away ;-)
This archive was generated by a fusion of
Pipermail (Mailman edition) and