Orphaned Code_* theory imports

[Peter Lammich]

Hi Florian

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

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


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). 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

--

   Peter


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