[isabelle-dev] Sporadic failures of CoreC++

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Dec 27 10:04:33 CET 2013

Hi all,

around http://isabelle.in.tum.de/repos/isabelle/rev/c21a2465cac1 and AFP

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,


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20131227/42e4ff12/attachment.asc>

More information about the isabelle-dev mailing list