[Termtools] certified - strange proofs

[Frederic Blanqui]

On Wed, 6 Jun 2007, Christian Sternagel wrote:

> It seems as there was a second missunderstanding between me and the
> Rainbow(runscript)-authors. I assumed that everything except a
> correct XML-file is interpreted as a wrong proof. But I saw

Result for tool TTT2+Rainbow+CoLoR on problem id: TRS/SK90 - 2.26

YES

Standard error:

Fatal error: exception Invalid_argument("not a proofMAYBE")

rainbow does not recognized MAYBE as a valid proof but the answer is YES. what 
are your runme and checkme scripts?

> that everytime when ttt2-cert outputs `MAYBE' (instead of an XML-file)
> there is a YES in the coq-proof output followed by an exception.
> The real strange thing is, that Coq afterwards succeeds in certifying,
> but there is no proof at all.

the reason is that when running coqc with an empty file, the exit status is 0!

11:08 ~ echo '' > zo.v
11:08 ~ coqc zo.v
11:08 ~ echo $?
0

=> we should check that the coq files indeed have a proved statement for 
termination!