[isabelle-dev] HOL-Predicate_Compile_Examples failure

Makarius makarius at sketis.net
Fri Apr 12 18:30:27 CEST 2013


On Fri, 12 Apr 2013, Account Isatest wrote:

> Test for platform at-poly-test failed. Log file attached.
> [...]
> Unfinished session(s): HOL-Predicate_Compile_Examples
> Finished at Fri Apr 12 02:42:04 CEST 2013
> 0:46:56 elapsed time, 3:11:32 cpu time, factor 4.08
> ------------------- test FAILED --- Fri Apr 12 02:42:04 CEST 2013 --- lxbroy2

isatest keeps complaining about HOL-Predicate_Compile_Examples, which is 
not the erratic behaviour (wrt. timing, CPU load, multithreading etc.) 
this time, but a problem of ~isabelle/contrib_devel/swipl/bin/swipl 
loading limgmp.so.3 -- due to recent OS updates; the local admins are 
informed.

Isabelle/0b0fc7dc4ce4 attempts to make the error behaviour of quickeck 
with prolog back-end more explicit, but it might be wrong again if return 
code != 0 happens in regular use.


Is there anybody actually maintaining these things?


 	Makarius


More information about the isabelle-dev mailing list