[isabelle-dev] Word Libraries

[Gerwin Klein]

Having finally managed to get some time to look over the changes to Word_Lib, I have strong concerns about this development and how it was made.

We only finished updating to Isabelle2021 a week ago -- it was major amount of work, mostly due to Word_Lib change, but I could see the value of the generalisations of the last round.

I do not see the value in most of these current changes. They have neither been articulated, nor are they obvious to me. In fact, to my mind the opposite is true for several of the changes.

For instance, who on earth wants to read something like "is_aligned (push_bit m k) m" instead of "is_aligned (k << m) m"? It is entirely unacceptable to make such a change in an AFP library without even consulting the original authors. I would never write this. Please revert it. 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.

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.

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.

Changing definitions such as shiftl1 to input abbreviations is likely to cause major breakage because term structure changes significantly. Again, what rationale has been considered, what cost/benefit analysis led to this decision? I strongly prefer definitions for these concepts. Please articulate these *before* you make such changes, and either convince the authors of the benefits or revert the change.

It is not acceptable to make such sweeping changes to other people's work without getting the author's consent first. As you very well know 90% of the use of this library is outside the AFP, and Word_Lib is the interface to that work, as well as an ingredient of a number of automated tools. 

Gerwin

> On 12 Aug 2021, at 17:24, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> Signed PGP part
> Hi Gerwin,
> 
>> This sounds good, but I don't quite remember any more what exactly that was, can you give a summary?
>> 
>> As you know, it's a bit of work to check that for l4v, esp since it is still on Isabelle2020 (no real issues, mostly organisational upheavals have taken up all available attention). It will take a while, but it looks like it will break in the usually hopefully small ways.
>> 
>> Do you have a list of changes that users will likely ned to apply?
> 
> it’s in the NEWS
> 
>> * Infix syntax for bit operations AND, OR, XOR is now organized in
>> bundle bit_operations_syntax. INCOMPATIBILITY.
>> 
>> * Bit operations set_bit, unset_bit and flip_bit are now class
>> operations. INCOMPATIBILITY.
>> 
>> * Theory Bit_Operations is now part of HOL-Main. Minor INCOMPATIBILITY.
>> 1
>> * Simplified class hierarchy for bit operations: bit operations reside
>> in classes (semi)ring_bit_operations, class semiring_bit_shifts is
>> gone.
>> 
>> * Abbreviation "max_word" has been moved to session Word_Lib in the AFP,
>> as also have constants "shiftl1", "shiftr1", "sshiftr1", "bshiftr1",
>> "setBit", "clearBit". See there further the changelog in theory Guide.
>> INCOMPATIBILITY.
> 
> and as a separate section in the »Guide« in session Word_Lib:
> 
>>  ➧[Changes since AFP 2021] ~
>> 
>>    ▪ Theory \<^theory>‹Word_Lib.Ancient_Numeral› is no part of \<^theory>‹Word_Lib.Word_Lib_Sumo›
>>      any longer.
>> 
>>    ▪ Infix syntax for \<^term>‹(AND)›, \<^term>‹(OR)›, \<^term>‹(XOR)› organized in
>>      syntax bundle \<^bundle>‹bit_operations_syntax›.
>> 
>>    ▪ Abbreviation \<^abbrev>‹max_word› moved from distribution into theory
>>      \<^theory>‹Word_Lib.Legacy_Aliases›.
>> 
>>    ▪ Operation \<^const>‹test_bit› replaced by input abbreviation \<^abbrev>‹test_bit›.
>> 
>>    ▪ Operation \<^const>‹shiftl› replaced by abbreviation \<^abbrev>‹shiftl›.
>> 
>>    ▪ Operation \<^const>‹shiftr› replaced by abbreviation \<^abbrev>‹shiftr›.
>> 
>>    ▪ Operation \<^const>‹sshiftr› replaced by abbreviation \<^abbrev>‹sshiftr›.
>> 
>>    ▪ Abbreviations \<^abbrev>‹bin_nth›, \<^abbrev>‹bin_last›, \<^abbrev>‹bin_rest›,
>>      \<^abbrev>‹bintrunc›, \<^abbrev>‹sbintrunc›, \<^abbrev>‹norm_sint›,
>>      \<^abbrev>‹bin_cat› moved into theory \<^theory>‹Word_Lib.Legacy_Aliases›.
>> 
>>    ▪ Operations \<^abbrev>‹shiftl1›, \<^abbrev>‹shiftr1›, \<^abbrev>‹sshiftr1›, \<^abbrev>‹bshiftr1›,
>>      \<^abbrev>‹setBit›, \<^abbrev>‹clearBit› moved from distribution into theory
>>      \<^theory>‹Word_Lib.Legacy_Aliases› and replaced by input abbreviations.
>> 
>>    ▪ Operation \<^const>‹complement› replaced by input abbreviation \<^abbrev>‹complement›.
> 
> Hope this helps,
> 	Florian
> 
> 
>