Re: [isabelle] Word authorship



As one of the other listed authors of (2), I'm also fine with this. I don't recall which parts of this I authored, but the l4.verified commit logs would have the answer. I'm happy for any of this to migrate with or without attribution.

> -----Original Message-----
> From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-
> bounces at lists.cam.ac.uk> On Behalf Of Klein, Gerwin (Data61, Kensington NSW)
> Sent: Sunday, May 24, 2020 18:47
> To: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
> Cc: Isabelle-Users Mailinglist <isabelle-users at cl.cam.ac.uk>
> Subject: Re: [isabelle] Word authorship
> 
> I can’t speak for all authors of Word_Lib, but from my side I’m perfectly fine
> with material moving between the three sessions. I'd suspect that the other
> authors don’t mind either, we have done at least some of this before.
> 
> Cheers,
> Gerwin
> 
> > On 23 May 2020, at 22:00, Florian Haftmann <florian.haftmann at informatik.tu-
> muenchen.de> wrote:
> >
> > Hi all,
> >
> > I want to take attention to a maintainance issue concerning the
> > different word-related session.  IMHO these are:
> >
> > 1) HOL-Word (in the distribution)
> > 	Authors: a couple (according to theory file headers)
> >
> > 2) Word_Lib (in the AFP)
> > 	Authors: many (according to official AFP meta data)
> >
> > 3) Native_Word (in the AFP)
> > 	Authors: one plus one contributor (according to official AFP
> >          meta data)
> >
> > 1) and 2) are collections around word types, whereas 3) has a
> > particular focus, an observation which is based both on content and
> > the number of others.
> >
> > 2) and 3) have a tendency to augment developments from HOL-Word or
> > other HOL sessions in order to serve a certain purpose better.  An example:
> > Native_Word provides code equations for symbolic computation of bit
> > operations on ints, something which is typically directly provided by
> > the corresponding session.
> >
> > In the past this has already led to a silent spreading of material
> > from
> > 2) and 3) to 1), without a particular attribution of authorship.
> >
> > On the one hand, it is not so uncommon that scattered generic material
> > from AFP entries (often organized in theories named More_*, Auxiliary,
> > Preliminaries, …) finds its way to the distribution.
> >
> > On the other hand, this time the restructuring might turn out more
> > extensive in the end and deserve more explicit attribution of
> > authorship: one idea is that eventually HOL-Word vanishes into two or
> > three library theories in the distribution and special operations end
> > up in Word_Lib (caveat: this is just an idea).
> >
> > What do the authors of these sessions think?
> >
> > Cheers,
> > 	Florian
> >



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