Orphaned Code_* theory imports

[Florian Haftmann]

Hi Peter,

 > These
 > theories where meant to provide a default sensible setup for the code
 > generator, by combining several Code_Target theories. You have now
 > removed that abstraction, and inlined it where it was used.

The combination of several theories over time has boiled down to 
HOL-Library.Code_Target_Numeral as the only one. This is an official 
hook which users can import if they want that particular setup. This is 
a deliberate decision not supposed to be obscured by transitive imports.

Why? Changing the code setup if non-monotonous. Technically, you get a 
default setup if you do nothing special, and you may change that default 
setup by importing particular theories. But then there is no supported 
way back again.

Admittedly I have recently blurred that simple picture by introducing 
HOL-Library.Code_Bit_Shifts_for_Arithmetic, but this is likely to be 
transient situation: if this theory proves what it promises it could be 
incorporated into HOL-Library.Code_Target_Numeral.

 > I do not understand why you got rid of the Code_Target_ICF theory (and
 > you could, along the same lines, get rid of CAVA_Code_Target)

CAVA_Code_Target is still there.

> This sounds like a very fragile (and dangerous) change. It will affect 
> all code-exports in theories that depend on the changed theories.

Indeed. One of my aims is to get rid of transitive, unintentional 
imports of HOL-Library.Code_Target_Numeral. I had a look at the 
immediate neighborhood of the affected places and tried best to identify 
spots where the import of HOL-Library.Code_Target_Numeral is intentional 
/ appropriate, but the situation got very intricate over the years and 
there might be subtle dependency paths.

> The observable effects may only be in the performance (and bindings to 
> external code), which you won't see in the standard AFP tests.

There is an important observable effect of AFP test performance: the 
duration of the long sessions as well as the ability to test the whole 
AFP within reasonable time and resource limits.

Of course there is a chance applications may degrade in performance 
unnoticed, but for actively maintained applications there are still a 
few months before the next release where things can be ironed out.

There have been so many re-arrangements of that material in recent times 
that the change in question only adds modestly to that general risk.

Cheers,
	Florian

> On 22/04/2025 19:40, Florian Haftmann wrote:
>> In AFP entries Separation_Logic_Imperative_HOL, CAVA_Automata, 
>> Collections and Ordinary_Differential_Equations, there were some 
>> (indirect) imports of Code_* theories from HOL-Library where actually 
>> no code generation was involved.
>>
>> I have removed these in https://foss.heptapod.net/isa-afp/afp-devel/-/ 
>> commit/ccc0b81823579c3d522a916b165bcc0bdf0d1ffb with no directly 
>> observable effect, but since these imports have been in place for 
>> quite a long time there might be applications where it is appropriate 
>> to explicitly import HOL-Library.Code_Target_Numeral and similar.
>>
>>     Florian

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 22777 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250423/e875d051/attachment-0001.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250423/e875d051/attachment-0001.sig>