Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type
- To: Christian Sternagel <c-sterna at jaist.ac.jp>
- Subject: Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type
- From: Lukas Bulwahn <bulwahn at in.tum.de>
- Date: Fri, 17 Feb 2012 14:53:16 +0100
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <4F3E50D7.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> <4F3E50D7.firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux i686; rv:9.0) Gecko/20111229 Thunderbird/9.0
On 02/17/2012 02:06 PM, Christian Sternagel wrote:
Tobias has encouraged small contributions. Don't think about it like a
publication, but like a library! (something like hackage, in your words.)
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?).
Of course, the authors and the content can be extended. There is no
reason to be reluctant, many theory developments are being continued to
be completed, so there is no fear that an entry is rejected because it
is incomplete, as long as it is in a comprehensible state.
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?
In the follow-ups of the mail above, the issues of reusing AFP entries
was discussed, but those issues should NOT stop you and others
contributing to the AFP.
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