On Sun, 31 Jan 2016, Lars Hupel wrote:
unexpected exception (bug?) in SML/NJ: Io [Io: openIn failed on
"/build/smlnj-tOOpSy/smlnj-110.76/sml.boot.x86-unix/smlnj/basis/.cm/x86-unix/basis.cm",
No such file or directory]
raised at: Basis/Implementation/IO/bin-io-fn.sml:617.25-617.71
../cm/util/safeio.sml:30.11
../compiler/TopLevel/interact/evalloop.sml:44.55
Settings are:
ML_SYSTEM=smlnj-110
ML_HOME="/usr/lib/smlnj/bin"
/usr/lib probably means that this is a "package" on the target system, and
thus it is usually broken by default.
I've never used anything else than a manual build of SML/NJ from the
official sources. It usually works out of the box, unchanged for many
decades.
Interestingly enough, "isabelle build" doesn't complain. The error only
becomes apparent in the log file.
Total existence failure of the outermost ML executable can lead to
problems with the Isabelle wrapper scripts. The same can happen for
Poly/ML under certain circumstances.
We are normally testing Isabelle applications, not ML installations.
Nonetheless, I hope to make this more robust at some point, by replacing
the shell scripts with Isabelle/Scala. Not having SML/NJ anymore could
accelerate that move.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
