Email Gateway (Jul 26 2025 at 17:58): Email Gateway (Jul 26 2025 at 17:58):From: Makarius <makarius@sketis.net>
There is a notable slowdown AFP/Native_Word:
Isabelle/e4207dfa36b5 AFP/16cb1cb993ae
Finished HOL (0:01:46 elapsed time, 0:05:36 cpu time, factor 3.16)
Finished Word_Lib (0:00:26 elapsed time, 0:01:37 cpu time, factor 3.70)
Finished Native_Word (0:01:36 elapsed time, 0:01:23 cpu time, factor 0.86)
Isabelle/3704717ed7bf AFP/ccc0b8182357
Finished HOL (0:01:47 elapsed time, 0:05:41 cpu time, factor 3.17)
Finished Word_Lib (0:00:25 elapsed time, 0:01:36 cpu time, factor 3.81)
Finished Native_Word (0:03:27 elapsed time, 0:03:16 cpu time, factor 0.94)
In the above changeset intervals, I see many changes on words and code
generation setup by Florian Haftmann, both in Isabelle and AFP.
He needs to say if the effect on Native_Word is to be expected, or if this a
problem that has been overlooked.
Makarius
Email Gateway (Jul 27 2025 at 17:26):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Hi Makarius,
Isabelle/e4207dfa36b5 AFP/16cb1cb993ae
Finished HOL (0:01:46 elapsed time, 0:05:36 cpu time, factor 3.16)
Finished Word_Lib (0:00:26 elapsed time, 0:01:37 cpu time, factor 3.70)
Finished Native_Word (0:01:36 elapsed time, 0:01:23 cpu time, factor 0.86)Isabelle/3704717ed7bf AFP/ccc0b8182357
Finished HOL (0:01:47 elapsed time, 0:05:41 cpu time, factor 3.17)
Finished Word_Lib (0:00:25 elapsed time, 0:01:36 cpu time, factor 3.81)
Finished Native_Word (0:03:27 elapsed time, 0:03:16 cpu time, factor 0.94)
thanks for figuring that out.
Honestely, these are things were I miss the plain old isatest with its
generated charts.
Anyway, I will look after those issues, but it will take some time
before I can actually dive into.
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jul 27 2025 at 17:59):From: Makarius <makarius@sketis.net>
On 27/07/2025 19:25, Florian Haftmann wrote:
Honestely, these are things were I miss the plain old isatest with its
generated charts.
These charts are now here:
https://isatest.sketis.net/devel/build_status/index.html
The most reliable test hardware is presently:
* mini3: macOS 13 Ventura (ARM)
* studio1: macOS 14 Sonoma (ARM)
When I have figured out how to rent an old-fashioned server room in Augsburg
for a reasonable price, I will put a proper Linux + Windows test machine
there, too.
Makarius
Email Gateway (Jul 31 2025 at 10:20):From: Florian Haftmann <florian.haftmann@cit.tum.de>
There is a notable slowdown AFP/Native_Word:
Isabelle/e4207dfa36b5 AFP/16cb1cb993ae
Finished HOL (0:01:46 elapsed time, 0:05:36 cpu time, factor 3.16)
Finished Word_Lib (0:00:26 elapsed time, 0:01:37 cpu time, factor 3.70)
Finished Native_Word (0:01:36 elapsed time, 0:01:23 cpu time, factor 0.86)Isabelle/3704717ed7bf AFP/ccc0b8182357
Finished HOL (0:01:47 elapsed time, 0:05:41 cpu time, factor 3.17)
Finished Word_Lib (0:00:25 elapsed time, 0:01:36 cpu time, factor 3.81)
Finished Native_Word (0:03:27 elapsed time, 0:03:16 cpu time, factor 0.94)In the above changeset intervals, I see many changes on words and code
generation setup by Florian Haftmann, both in Isabelle and AFP.He needs to say if the effect on Native_Word is to be expected, or if
this a problem that has been overlooked.
This decay stems from calls to code_simp.
The deviation comes from the code equations for int_of_integer: in the
previous situations, there was a compromise in the code setup which used
a variant of int_of_integer to speed up execution of code_simp in trade
for that the code setup would not be executable stand-alone in a plain
target language built would need additional modifications of the code setup.
The equations in question are
‹int_of_integer 0 = 0›
‹int_of_integer (Code_Numeral.Pos n) = Int.Pos n›
‹int_of_integer (Code_Numeral.Neg n) = Int.Neg n›
‹int_of_integer k = …› (*)
where for real target languages only the last one is used (*), where the
conversion happens by explicit binary cuts, which is fine for an unknown
representation, but does not compute that well in the logic.
The first three equations are fine for abstract representations (Pure,
NBE). For NBE there is no decay, so it seems to work as intended there.
But for some unknown reason, the simplifier prefers the last equation,
as can be seen in HOL-Main:
declare int_of_integer_code_nbe [code nbe]
declare int_of_integer_code [code]
declare [[code_simp_trace]]
lemma
‹P (int_of_integer (Code_Numeral.Pos Num.One))›
apply code_simp
Can anybody familiar with the simplifier explain what is going on?
Bzw. the timing panel in Isabelle/jEdit is an excellent tool to pin down
such things.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Aug 31 2025 at 20:21 UTC