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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
