[isabelle-dev] Grouping ISABELLE_FULL_TEST?
makarius at sketis.net
Sun Jan 31 23:12:59 CET 2016
On Sun, 31 Jan 2016, Lars Hupel wrote:
> unexpected exception (bug?) in SML/NJ: Io [Io: openIn failed on
> No such file or directory]
> raised at: Basis/Implementation/IO/bin-io-fn.sml:617.25-617.71
> Settings are:
/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
> 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.
More information about the isabelle-dev