[isabelle-dev] AFP

[Makarius]

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