Re: [isabelle] Word authorship

Dear Florian,

Thanks for driving the development of Isabelle's word library. From my side, it's perfectly fine if auxiliary material from Native_Word moves into the Isabelle distribution in whatever form. If you want to move the whole AFP entry into the distribution, then that's also fine with me, but then I'd like to be mentioned in the theory headers. The main reason for creating Native_Word as an AFP entry in the first place was that the code_printing declarations therein enlarge the trusted code base. So even if Native_Word moves as a whole into the distribution, I think it would still be good to keep it separate from the rest of the HOL-Word formalization.

IIRC Peter Lammich's contribution to Native_Word is essentially contained in the Uint type of unspecified bit size.


On 23/05/2020 16:00, Florian Haftmann 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

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?


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