Hi all,

around http://isabelle.in.tum.de/repos/isabelle/rev/c21a2465cac1 and AFP
http://sourceforge.net/p/afp/code/ci/33dd66ae7530fd7404c37162b87504b1d47d955e/

I could often observe sporadic failures when running on lxbroy10, e.g.
due to heavy load:

>       Reached timeout during execution of values
>       At command "values" (line 1103 of 
> "/tmp/mira/workbench/11425-139898784548608/AFP/thys/CoreC++/Execute.thy")

I am uncertain what to do best about it.  One option would be to
increase the corresponding timeout in the predicate compiler.  Another
one to increase it only for CoreC++.

But I am uncertain whether this timeout should be restricted to
interactive mode anyway.

Any suggestions?

Thanks a lot,
        Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature

_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to