Email Gateway (Aug 23 2022 at 09:01): Email Gateway (Aug 23 2022 at 09:01):From: "Fernandez, Matthew" <matthew.fernandez@intel.com>
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.
Email Gateway (Aug 23 2022 at 09:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Email Gateway (Aug 23 2022 at 09:12):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
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.
Best,
Andreas
Email Gateway (Aug 23 2022 at 09:12):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,
Native_Word as a whole has a very clear concept and purpose and it will
definitely remain a separate AFP entry. Indeed my hope is that there is
room for movement in the opposite direction: move specialized material
from the distribution into the AFP.
Cheers,
Florian
signature.asc
Email Gateway (Aug 23 2022 at 09:12):From: "Klein, Gerwin (Data61, Kensington NSW)" <Gerwin.Klein@data61.csiro.au>
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
Last updated: Apr 25 2024 at 16:19 UTC