makarius at sketis.net
Sat Feb 13 13:07:22 CET 2016
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
x86 address model, and lacks the smart heap sharing of Poly/ML.
The formal result of that are many conditions on ML_SYSTEM_POLYML in
src/HOL/ROOT (e.g. in Isabelle/8bbbe07cd0ee). HOL-Library also fails,
although it is not formally marked there.
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?
SML/NJ used to have a use for time travel into the past: Isabelle versions
from many years ago can still be run on current machines with current
SML/NJ. The extreme stability of SML/NJ -- due to lack of progress in the
past two decades -- makes an advantage here. This application loses its
relevance when major parts of Isabelle/HOL libraries no longer work.
We have AFP today to collect Isabelle applications that are worth to
update continuosly. So there is rarely a need to travel into the past.
Discontinuing SML/NJ will have far-reaching consequences in Isabelle/Pure:
many system modules will shrink to just one version for Poly/ML, without
conditions about the availability of ML threads, advanced compiler
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.
More information about the isabelle-dev