Re: [isabelle] New AFP theory: List Index

My immediate plea is for modular library components. Having those as
top-level entries dramatically increases the likelyhood that they are

But you are quite right: Hackage offers some things worth emulating:
- A listing of packages by category
- cabal
A complication is that Isabelle does not support hierarchical module
names in the way Haskell (or Java or ...) does.


Simon Winwood schrieb:
> 	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 ...
> 	Simon
> 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.