[isabelle-dev] Grouping ISABELLE_FULL_TEST?

[Makarius]

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