Failure of AFP/Native_Word_Test_SMLNJ2 with SML/NJ

Makarius makarius at sketis.net
Mon Jan 27 12:42:15 CET 2025


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



More information about the isabelle-dev mailing list