Email Gateway (Apr 22 2025 at 17:49): Email Gateway (Apr 22 2025 at 17:49):From: Florian Haftmann <florian.haftmann@cit.tum.de>
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
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Apr 22 2025 at 18:58):From: Peter Lammich <lammich@in.tum.de>
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
Email Gateway (Apr 23 2025 at 17:19):From: Florian Haftmann <florian.haftmann@cit.tum.de>
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
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Apr 23 2025 at 18:40):From: Peter Lammich <lammich@in.tum.de>
Ok, if the goal is to only have one efficient code target theory, then I can
see where these changes are going
Peter
On 23 Apr 2025 19:11, Florian Haftmann <florian.haftmann@cit.tum.de> wrote:
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,
FlorianOn 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
Last updated: May 31 2025 at 01:44 UTC