[isabelle-dev] SML/NJ

[Makarius]

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 
features etc.

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.


 	Makarius