On Thu, 15 May 2014, Makarius wrote:
We also have a total failure of existence with isatest, since HOL-Proofs
does not build on the initial test machine (lxbroy2) for the
documentation sessions. I still need to find out if it is the one lemma
addition by Tobias, my change of Poly/ML, or just that machine which is
constantly running some boring batch process: on all cores: 178027:57
diam_5
The true reason is still unclear, but I have applied some old trick in
/home/isatest/.isabelle/etc/settings to make sure that the initial
makedist with the documentation works:
case "$ISABELLE_IDENTIFIER" in
*-build)
ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
;;
esac
I.e. a new version of the old THIS_IS_ISABELLE_BUILD workaround.
So far the regular isatest run afterwards looks OK. The failure from
today was harmless: missing second copy of the polyml-5.5.2 component in
/home/polyml/.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
