Email Gateway (Jan 27 2025 at 12:16): Email Gateway (Jan 27 2025 at 12:16):From: Florian Haftmann <florian.haftmann@cit.tum.de>
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
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jan 28 2025 at 12:04):From: Florian Haftmann <florian.haftmann@cit.tum.de>
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
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Feb 01 2025 at 20:19 UTC