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 ;-)
> Tobias

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.