[isabelle-dev] AFP

Makarius makarius at sketis.net
Fri May 16 11:16:36 CEST 2014

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:


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 


More information about the isabelle-dev mailing list