[isabelle-dev] Grouping ISABELLE_FULL_TEST?

[Lars Hupel]

> Building with SML/NJ configuration is trivial. It would be "just another
> job" in Jenkins. I'd just need to know about what to build precisely.
> Can you explain to me what the ML_SYSTEM_POLYML variable means?

I was speaking too early. Here's what I get when trying to build Pure
with SML/NJ:


Standard ML of New Jersey v110.76 [built: Sun Jun 29 03:29:51 2014]
!* unable to process `' (unknown extension `<none>')
- [autoloading]

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"
ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo
"$HEAP_SUFFIX")


Interestingly enough, "isabelle build" doesn't complain. The error only
becomes apparent in the log file.

Cheers
Lars