[Termtools] certification failures

olivier.pons at cnam.fr olivier.pons at cnam.fr
Wed Nov 12 15:14:33 CET 2008


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. 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.

olivier


More information about the Termtools mailing list