Failure of AFP/Native_Word_Test_SMLNJ2 with SML/NJ

[Florian Haftmann]

See now https://isabelle.in.tum.de/repos/isabelle/rev/e23bd621eddb

I plan to add an explicit check on that also.

	Florian

Am 26.01.25 um 17:30 schrieb Florian Haftmann:
> Seems like my business.
> 
> Thanks for reporting.
> 
>      Florian
> 
> Am 26.01.25 um 17:28 schrieb Makarius:
>> We have a failure of AFP/Native_Word_Test_SMLNJ2 with SML/NJ, using 
>> Isabelle/989e661398d6 + AFP/5cb6756ec5b0 and ISABELLE_SMLNJ=/usr/bin/ 
>> sml in $ISABELLE_HOME_USER/etc/settings (e.g. with the regular Ubuntu 
>> package for smlnj):
>>
>> /tmp/isabelle-makarius/process8926374598986055100/Code_Test5534440/ 
>> generated.sml:222.22-223.61 Error: case object and rules don't agree 
>> [tycon mismatch]
>>    rule domain: ?.int * int
>>    object: int * int
>>    in expression:
>>      (case ((div_mod k) max_index)
>>        of (b,s) => word_of_int s :: (replicate <exp>) word_max_index)
>>
>> uncaught exception Error
>>
>>
>>      Makarius
>>
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 22777 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250127/705ab9ae/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250127/705ab9ae/attachment.sig>