Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type
- To: christian.urban at kcl.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 23:07:30 +0900
- Cc: Christian Sternagel <c-sterna at jaist.ac.jp>, isabelle-users at cl.cam.ac.uk
- In-reply-to: <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> <email@example.com>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.1) Gecko/20120209 Thunderbird/10.0.1
On 02/17/2012 10:34 PM, Christian Urban wrote:
Seconded. Maybe I did not state it that way above, but actually I also
want the AFP to stay publication-like (and I viewed it like that until
now; if nothing else, to value the effort that is put into such entries).
On Friday, February 17, 2012 at 22:06:31 (+0900), Christian Sternagel wrote:
> 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?).
I very much agree with that. AFP-entries have
the character of a publication (they are refereed
to some degree) and are attached to an author or authors.
While it is technically possible to amend the authorship
of an AFP-entry, it is a psychological hassle.I had an
instance of this last year where I had to make amendments
to an AFP-entry by Alexander and Tobias. What made this even
more complicated is that they also published their entry in JAR.
So I was in the quandary whether to make changes to their
development or not, having in the back in my mind that they
might have a complete different opinion how things should be
done than me (and my co-authors). In the end, my changes were
minimal, but still it was a huge hassle.
AFP-entries should stay publication-like things. They
should not be a place where things are under rapid development.
Maybe there could be a different AFP "branch" that is purely library
Concerning Tobias original mail (on small AFP entries): Strange how one
can forget mailing list discussions that were actually read with great
interest ;). What is the current state w.r.t. the discussion that
followed in 2010? IIRC, the points were roughly
- module name spaces
- visibility of syntax
- installing entries (+ dependencies; something like cabal for Haskell)
Is there any way in which non-developers (like me) could contribute to
anything of the above?
This archive was generated by a fusion of
Pipermail (Mailman edition) and