Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type
- From: Christian Sternagel <c-sterna at jaist.ac.jp>
- Date: Fri, 17 Feb 2012 22:06:31 +0900
- In-reply-to: <alpine.LNX.firstname.lastname@example.org>
- References: <DE5AA7BA-DC9B-4DBE-876E-CDDF673FDC7E@uibk.ac.at> <4F3E363F.email@example.com> <4F3E3ADD.firstname.lastname@example.org> <alpine.LNX.email@example.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.1) Gecko/20120209 Thunderbird/10.0.1
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 in.tum.de
This archive was generated by a fusion of
Pipermail (Mailman edition) and