[isabelle-dev] SML/NJ happiness
makarius at sketis.net
Fri Nov 16 21:23:05 CET 2012
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 the spot why isatest gave uninformative "exception Option
raised" here for almost two weeks, but it was relatively easy to see the
point of failure in the mira reports.
SML/NJ might appear like a cruel tool for torture now, but it is just a
look back in time. 10 years ago, SML/NJ and Poly/ML were almost equal in
performance, and SML/NJ had slightly better error messages than Poly/ML.
The difference is that a lot of work has been done on Poly/ML and its
integration into Isabelle (both Isar and Prover IDE), to make the comfy
chair really comfortable.
More information about the isabelle-dev