[Termtools] certification failures

[Ulrich Schmidt-Goertz]

olivier.pons at cnam.fr schrieb:
> Hi all,
> 
> saying "RED with > 60 seconds is timeout, RED with < 60 seconds is
> failure" is not always true.  See for example
> 
> tpdb-5.0/TRS/TRCSR/Ex15_Luc98_C.trs,
> tpdb-5.0/TRS/TRCSR/Ex3_3_25_Bor03_C.trs,
> tpdb-5.0/TRS/TRCSR/Ex9_BLR02_C.trs or
> tpdb-5.0/TRS/TRCSR/PALINDROME_complete-noand_FR.trs for AProVE-A3PAT
> 
> where if I understand well, a timeout takes place after having written
> "yes" but before having written the complete coq source.

Yes, that's exactly what happened.

> Clearly this is
> not a certification failure and  this incomplete source should not even be
> passed to coqc.
> Maybe we can also implement an intelligent timeout to avoid that.

Well, the problem is that for AProVE, several seconds may pass between
the output of "YES" and of the certificate (we call an XSLT processor in
between, which takes some time). Rearranging the statements in our runme
script should be sufficient to minimize this delay.