Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type



Dear all,

Agreeing to the below

On 02/19/2012 07:07 AM, Gerwin Klein wrote:
I don't see that a good reason for the AFP becoming a development platform with rapid development inside its repository. Similarly to hackage, cpan, ctan, and others, it should stay a release and collection place. Active development should happen elsewhere (own sourceforge project, bitbucket, etc). Regular releases from there could then go into the AFP.
I don't think a separate branch makes sense, but we could tag certain entries as libraries if that helps the psychology aspect. If they are actively developed, they can get a link to their home page/project page. That would also solve the problem of who to contact if you have something to contribute/request/etc. Technically we already support evolving versions of entries, and if things like author lists change, that can be marked in the change history.

I started a sourceforge project to develop a "library" for the option monad:

  http://sourceforge.net/p/optionmonad/

Of course in Isabelle/HOL it is difficult to have the "right" lemmas without actual applications. Some applications of the current version of Option_Monad.thy can be found in the theories Substitution, Ground_Context_Impl, Equational_Reasoning, and Check_Equational_Proof of

  http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR

That's where the current lemmas originate.

It would make sense to have example applications (for regression testing) as part of the project. Please join the project, contribute (monadic functions, properties, or example applications), and comment.

I would like to view this as a playground (to find out how such a kind of project works for Isabelle/HOL), so don't worry to much before changing something.

cheers

chris





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