[isabelle-dev] SML/NJ

[Lars Hupel]

> With such a painfully slow and incomplete SML/NJ test, it is time to ask
> the canonical question:
> 
>   Are there remaining uses of SML/NJ, or can it be discontinued now?

I have mixed feelings about this.

On one hand, supporting multiple compiler platforms keeps us honest,
i.e. to make sure we're not relying on accidental deviations from the ML
Definition. Other systems targeting languages like OCaml don't have that
luxury, because the ecosystem is a monoculture around a single compiler.

On the other hand, Isabelle is de facto reliant on Poly/ML for various
other reasons, of which performance is the major one.

> Thus we can roar ahead faster, but we are also leaving behind the
> conceptual support by an alternative platform. Today this "support" is
> probably just symbolic, because SML/NJ has become practically unusable.

This is true and can't be argued away easily. Hence I'm in favour of
discontinuing SML/NJ.

Cheers
Lars