Email Gateway (Jan 26 2025 at 16:29): Email Gateway (Jan 26 2025 at 16:29):From: Makarius <makarius@sketis.net>
We have a failure of AFP/Native_Word_Test_SMLNJ2 with SML/NJ, using
Isabelle/989e661398d6 + AFP/5cb6756ec5b0 and ISABELLE_SMLNJ=/usr/bin/sml in
$ISABELLE_HOME_USER/etc/settings (e.g. with the regular Ubuntu package for smlnj):
/tmp/isabelle-makarius/process8926374598986055100/Code_Test5534440/generated.sml:222.22-223.61
Error: case object and rules don't agree [tycon mismatch]
rule domain: ?.int * int
object: int * int
in expression:
(case ((div_mod k) max_index)
of (b,s) => word_of_int s :: (replicate <exp>) word_max_index)
uncaught exception Error
Makarius
Email Gateway (Jan 26 2025 at 16:30):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Seems like my business.
Thanks for reporting.
Florian
Am 26.01.25 um 17:28 schrieb Makarius:
We have a failure of AFP/Native_Word_Test_SMLNJ2 with SML/NJ, using
Isabelle/989e661398d6 + AFP/5cb6756ec5b0 and ISABELLE_SMLNJ=/usr/bin/sml
in $ISABELLE_HOME_USER/etc/settings (e.g. with the regular Ubuntu
package for smlnj):/tmp/isabelle-makarius/process8926374598986055100/Code_Test5534440/
generated.sml:222.22-223.61 Error: case object and rules don't agree
[tycon mismatch]
rule domain: ?.int * int
object: int * int
in expression:
(case ((div_mod k) max_index)
of (b,s) => word_of_int s :: (replicate <exp>) word_max_index)uncaught exception Error
Makarius
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jan 27 2025 at 06:41):From: Florian Haftmann <florian.haftmann@cit.tum.de>
See now https://isabelle.in.tum.de/repos/isabelle/rev/e23bd621eddb
I plan to add an explicit check on that also.
Florian
Am 26.01.25 um 17:30 schrieb Florian Haftmann:
Seems like my business.
Thanks for reporting.
Florian
Am 26.01.25 um 17:28 schrieb Makarius:
We have a failure of AFP/Native_Word_Test_SMLNJ2 with SML/NJ, using
Isabelle/989e661398d6 + AFP/5cb6756ec5b0 and ISABELLE_SMLNJ=/usr/bin/
sml in $ISABELLE_HOME_USER/etc/settings (e.g. with the regular Ubuntu
package for smlnj):/tmp/isabelle-makarius/process8926374598986055100/Code_Test5534440/
generated.sml:222.22-223.61 Error: case object and rules don't agree
[tycon mismatch]
rule domain: ?.int * int
object: int * int
in expression:
(case ((div_mod k) max_index)
of (b,s) => word_of_int s :: (replicate <exp>) word_max_index)uncaught exception Error
Makarius
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jan 27 2025 at 11:43):From: Makarius <makarius@sketis.net>
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
Last updated: Feb 01 2025 at 20:19 UTC