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

Dear all,

related to Lukas comment (that also small contributions are appropriate for the AFP) I have some thoughts:

(At least for me) the AFP has a somewhat formal flavor (like a publication). Furthermore, every entry is associated to fixed authors (is it possible to extend the author list later on?).

As for Option_Monad: this is a completely unfinished adhoc collection of functions and lemmas related to the option type, so I'm reluctant to send it to the AFP. What I do however want, is that other users that could make use of an option monad have access to the parts that have already been done and can contribute their own ideas.

It would be nice to have a common platform, where arbitrarily mature developments could be posted, discussed, and improved by the community (without any formal reviewing; what is useful to the community will evolve, what is not will decay). Something like hackage for Haskell. Maybe the AFP is exactly this platform and I was just not aware of it?



On 02/17/2012 09:33 PM, Makarius wrote:
On Fri, 17 Feb 2012, Lukas Bulwahn wrote:

Just two comments:

First, the discussion about this should be on the isabelle mailing
list, not the isabelle developer's mailing list.
There has been a discussion just a few days ago that the developer's
mailing list is limited to arbitrary repository versions and the
related development process, including administrative things like
isatest, mira etc.

Second, the AFP is a perfect place to also submit small library
developments. The List-Index theory is such an example.
So, the Option monad could be just turned into a small AFP entry.

I've also asked myself again this question about isabelle-users vs.
isabelle-dev, when looking at the message for 2min, but considered it is
a boundary case that could go either way.

In practice it is also a matter of the size of audience. There might be
yet unknown library contributions out there that could be joined in such
efforts. So there is definitely a tendency more towards isabelle-users.

(Oddly isabelle-dev appears to be much more active recently than
isabelle-users. Are there fewer users or fewer user problems now?)

isabelle-dev mailing list
isabelle-dev at

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