Email Gateway (Apr 14 2025 at 09:49): Email Gateway (Apr 14 2025 at 09:49):From: Makarius <makarius@sketis.net>
I have tested a recent repository version of Poly/ML
https://github.com/polyml/polyml/commit/e266a93fe8fe with current
Isabelle/9e5f645d6000.
This causes a problem in line 83 of theory
"Codegenerator_Test.Generate_Target_Bit_Operations.thy":
*** Evaluation for PolyML failed:
*** exception Fail raised (line 5): Bad max
Looking only superficially, I don't quite understand what is the intention of
the test.
Note that there have been recent changes in Poly/ML on word arithmetic.
Makarius
Email Gateway (Apr 14 2025 at 09:53):From: Makarius <makarius@sketis.net>
On 14/04/2025 11:49, Makarius wrote:
I have tested a recent repository version of Poly/ML https://github.com/
polyml/polyml/commit/e266a93fe8fe with current Isabelle/9e5f645d6000.
I should also say that this can be built like this:
isabelle component_polyml -V e266a93fe8fe
Makarius
Email Gateway (Apr 15 2025 at 07:36):From: Florian Haftmann <florian.haftmann@cit.tum.de>
I have tested a recent repository version of Poly/ML https://github.com/
polyml/polyml/commit/e266a93fe8fe with current Isabelle/9e5f645d6000.This causes a problem in line 83 of theory
"Codegenerator_Test.Generate_Target_Bit_Operations.thy":*** Evaluation for PolyML failed:
*** exception Fail raised (line 5): Bad maxLooking only superficially, I don't quite understand what is the
intention of the test.Note that there have been recent changes in Poly/ML on word arithmetic.
The explanation for this test can be found (admittedly, very indirect
and implicit) at
https://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Code_Numeral.thy#l1014
reading
val max_index = pow (fromInt 2, Int.- (Word.wordSize, 3)) - fromInt 1;
(experimentally determined)
This is the maximum value usable as index in bit shifts.
The check in Generate_Target_Bit_Operations.thy then asserts that this
is really the maximum.
I am uncertain where to proceed from here. If this max_index is no
longer unique across different ML versions, it is maybe best to drop the
line
Ie. just assert that the index is small enough.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Apr 18 2025 at 20:21 UTC