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