[isabelle-dev] Grouping ISABELLE_FULL_TEST?
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
Standard ML of New Jersey v110.76 [built: Sun Jun 29 03:29:51 2014]
!* unable to process `' (unknown extension `<none>')
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
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