Problem with polyml-e266a93fe8fe and Generate_Target_Bit_Operations
Makarius
makarius at sketis.net
Mon Apr 14 11:49:14 CEST 2025
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
More information about the isabelle-dev
mailing list