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