<div dir='auto'>Ok, if the goal is to only have one efficient code target theory, then I can see where these changes are going <div dir="auto"><br></div><div dir="auto">Peter </div></div><div class="gmail_extra"><br><div class="gmail_quote">On 23 Apr 2025 19:11, Florian Haftmann <florian.haftmann@cit.tum.de> wrote:<br type="attribution" /><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">Hi Peter, <br>
<br>
 > These <br>
 > theories where meant to provide a default sensible setup for the code <br>
 > generator, by combining several Code_Target theories. You have now <br>
 > removed that abstraction, and inlined it where it was used. <br>
<br>
The combination of several theories over time has boiled down to  <br>
HOL-Library.Code_Target_Numeral as the only one. This is an official  <br>
hook which users can import if they want that particular setup. This is  <br>
a deliberate decision not supposed to be obscured by transitive imports. <br>
<br>
Why? Changing the code setup if non-monotonous. Technically, you get a  <br>
default setup if you do nothing special, and you may change that default  <br>
setup by importing particular theories. But then there is no supported  <br>
way back again. <br>
<br>
Admittedly I have recently blurred that simple picture by introducing  <br>
HOL-Library.Code_Bit_Shifts_for_Arithmetic, but this is likely to be  <br>
transient situation: if this theory proves what it promises it could be  <br>
incorporated into HOL-Library.Code_Target_Numeral. <br>
<br>
 > I do not understand why you got rid of the Code_Target_ICF theory (and <br>
 > you could, along the same lines, get rid of CAVA_Code_Target) <br>
<br>
CAVA_Code_Target is still there. <br>
<br>
> This sounds like a very fragile (and dangerous) change. It will affect  <br>
> all code-exports in theories that depend on the changed theories. <br>
<br>
Indeed. One of my aims is to get rid of transitive, unintentional  <br>
imports of HOL-Library.Code_Target_Numeral. I had a look at the  <br>
immediate neighborhood of the affected places and tried best to identify  <br>
spots where the import of HOL-Library.Code_Target_Numeral is intentional  <br>
/ appropriate, but the situation got very intricate over the years and  <br>
there might be subtle dependency paths. <br>
<br>
> The observable effects may only be in the performance (and bindings to  <br>
> external code), which you won't see in the standard AFP tests. <br>
<br>
There is an important observable effect of AFP test performance: the  <br>
duration of the long sessions as well as the ability to test the whole  <br>
AFP within reasonable time and resource limits. <br>
<br>
Of course there is a chance applications may degrade in performance  <br>
unnoticed, but for actively maintained applications there are still a  <br>
few months before the next release where things can be ironed out. <br>
<br>
There have been so many re-arrangements of that material in recent times  <br>
that the change in question only adds modestly to that general risk. <br>
<br>
Cheers, <br>
Florian <br>
<br>
> On 22/04/2025 19:40, Florian Haftmann wrote: <br>
>> In AFP entries Separation_Logic_Imperative_HOL, CAVA_Automata,  <br>
>> Collections and Ordinary_Differential_Equations, there were some  <br>
>> (indirect) imports of Code_* theories from HOL-Library where actually  <br>
>> no code generation was involved. <br>
>> <br>
>> I have removed these in https://foss.heptapod.net/isa-afp/afp-devel/-/  <br>
>> commit/ccc0b81823579c3d522a916b165bcc0bdf0d1ffb with no directly  <br>
>> observable effect, but since these imports have been in place for  <br>
>> quite a long time there might be applications where it is appropriate  <br>
>> to explicitly import HOL-Library.Code_Target_Numeral and similar. <br>
>> <br>
>>     Florian <br>
<br>
</p>
</blockquote></div><br></div>