MLton [was: Failure of AFP/Native_Word_Test_SMLNJ2 with SML/NJ]

[Florian Haftmann]

See now https://isabelle.in.tum.de/repos/isabelle/rev/513f8fa74c82 which 
hopefully closes this subject.

	Florian

Am 27.01.25 um 13:16 schrieb Florian Haftmann:
> There is an issue in PAC_Checker and MLton which I will also address 
> hopefully during the upcoming days.
> 
>      Florian
> 
> Am 27.01.25 um 12:42 schrieb Makarius:
>> On 26/01/2025 17:43, Lawrence Paulson wrote:
>>> Didn’t we drop support for SML/NJ about 100 years ago?
>>
>> We still have it as target for codegeneration from HOL. It can be 
>> considered a clean implementation of Standard ML, and usually does not 
>> cause problems.
>>
>> We also have Mlton in that position: It does cause problems, 
>> especially on macOS.
>>
>> My inclination is to keep both SML platforms in our portfolio: this 
>> means I need to revisit Mlton once again for this release.
>>
>>
>>      Makarius
>>
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 19169 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250128/0657effe/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/20250128/0657effe/attachment.sig>