[isabelle-dev] Word Libraries

[Florian Haftmann]

Hi Gerwin and all reading this thread,

I went through the repositories’ history and my memory to recap what
happened here in the post-Isabelle2020 and post-Isabelle2021 time.

Overall, the changes at a glance are guided by the following aims,
quoted from the write-up at
<https://isabelle.in.tum.de/~haftmann/bits_and_word/>:

* Theory Word contains the word type and its operations proper, located
in session HOL-Library.

* Additional material of somehow unclear status in relevance is
modularized into separate theories and moved to session Word_Lib in the AFP.

* The historically grown Word_Lib is minimally structured and augmented
with a guide.

* The ultimate goal is that future development can happen mostly in the AFP.

Some of that work has already happened before Isabelle2021; what
happened for Isabelle2021-1 as far as I can see from the history:

* Some disentanglement of theory dependencies to enable users to use the
library more selectively (»Word_Lib is minimally structured«) – this
affects genuine Word_Lib material .

* Movement of material from the distribution / HOL-Library.Word to
Word_Lib (»moved to session Word_Lib in the AFP«)

* Restructuring of that (originally non-Word_Lib (!)) material
(»modularized into separate theories«).

(I emphasize here that most of the changes seen in the AFP actually
originate from the Bit/Word material in the distribution, where the
cumulative reworking over two releases gives me kind of responsibility
and »legitimacy« for proactive developments. Coming back to the original
aims: »The ultimate goal is that future development can happen mostly in
the AFP.« Ie. without subtle and hard to maintain dependencies between
AFP and distribution. Note also that the changes towards Isabelle2021
are far more massive than those afterwards.)

If these intentions and measures *by itself* infringe your authorship or
the intended purpose or usability of Word_Lib, this is a fundamental
issue and we should make a stop here and find a way to work that out in
particular.

Otherwise I would appreciate to get to the particular problems with the
current matter of affairs. I thankfully accept any hints on slips,
omissions, misperceptions, doubtful quality, theory and tool break-downs
both in the visible and the non-visible universe – be it due to changes
or not. In that manner both authors and non-authors of Word_Lib in
private conversation have already given feedback and also contributions.

Generally: If there are any repositories I should have a look at for
some kind of assessment, please let me know. Also if there is particular
experience of the migration to Isabelle2021 I should take into
consideration.

> For instance, who on earth wants to read something like "is_aligned (push_bit m k) m" instead of "is_aligned (k << m) m"? . The syntax was introduced for good reasons. It is fine to make it a bundle to not pollute a global syntax space, it is not fine to change original material that was written with a purpose.

If your point is to to apply the ‹_ << _› syntax etc. thoroughly and
consistently among Word_Lib theories, I am happy to look after these slips.

> It is *absolutely* not fine to produce commits like "dropped junk" which removes a theory that was critical to how this library is used after in previous commits having made it unusable, entirely missing the point of its existence. Please revert that entire series of commits and reproduce the old setup.

After a second study of history I notice that I messed this up already
in the AFP release for Isabelle2021; the change after that point of
reference was indeed just a cleanup of dead theories. Looks I should
just revert to pre-Isabelle2021 there?

> Further, a whole lot of constants have been moved around. Why? What does this improve? This can cause major amounts of renaming work for no gain to anyone. Please either produce a convincing argument for the benefit of these moves or revert them

These moves AFAICS originate from the distribution (see above), where
the elimination of the ancient HOL-Word session for Isabelle2021 already
had massive impact on internal names for operations. Is your concern
about renaming work just abstract or based on concrete observations? I
am asking since if any tool survived the Isabelle2021 movements, there
is little reason to assume that it won’t survive the current state of
affairs – Isabelle is far more robust against such things as, say, 15
years ago.

> Changing definitions such as shiftl1 to input abbreviations is likely to cause major breakage because term structure changes significantly.

The shift*1 Operations have been auxiliary definitions in the
distribution to bootstrap the bit shifts operations, similarly to
iszero, equipped only with a minimal set of lemmas. If one tool out
there relies on it as explicit constant i. e. due to pattern matching, I
won’t shed a tear to keep it as constant.

(Aside, the primitive definitions then would be maybe: shiftl1 a = (a <<
1), shiftr1 a = (a >> 1), sshiftr1 a = (a >>> 1)).

Cheers,
	Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20211006/50c5797b/attachment.sig>