> 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 would also prefer a second usable ML implementation as reference, but
we have to face that only maintained platforms as P
I don't see the point of continuing with SML/NJ any longer.
Larry
> On 13 Feb 2016, at 12:07, Makarius wrote:
>
> Are there remaining uses of SML/NJ, or can it be discontinued now?
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanb
> 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 w
Every 10 years it is time to reconsider the SML/NJ problem seriously.
For the Isabelle2016 release, I've made full SML/NJ tests as usual (which
takes more than one night to build). This time many sessions did not build
at all: out-of-memory after long hours. SML/NJ is still bound to the small
Isabelle/5e01e32dadbe is the result of spending some hours with SML/NJ and
the ever growing HOL image. In the end it turned out as rather trivial
thing: Time.+ needs to be used in this qualified manner, since the adhoc
overloading of + on different ML systems works differently.
I can't say on
