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

Florian Haftmann florian.haftmann at cit.tum.de
Mon Jan 27 13:16:12 CET 2025


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/20250127/5ef8b67e/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/5ef8b67e/attachment.sig>


More information about the isabelle-dev mailing list