[isabelle-dev] Grouping ISABELLE_FULL_TEST?

Lars Hupel hupel at in.tum.de
Sun Jan 31 22:50:07 CET 2016

> 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
No such file or directory]
  raised at: Basis/Implementation/IO/bin-io-fn.sml:617.25-617.71

Settings are:

ML_OPTIONS="@SMLdebug=/dev/null @SMLalloc=1024"
ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo

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


More information about the isabelle-dev mailing list