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.


> On 23 May 2020, at 22:00, Florian Haftmann <florian.haftmann at> 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.