[Termtools] certified - strange proofs

[Koprowski, A.]

  Dear Claude,

 attached is the fixed script (also as a patch below). An alternative was to keep the script as it was and change TTT2 to exit with non-zero status for non-successful proofs.

  Best wishes,
   Adam


*** runme-ttt   2007-06-06 17:36:41.000000000 +0200
--- runme       2007-06-06 17:37:38.758860000 +0200
***************
*** 12,15 ****
--- 12,16 ----
  prf=./tmp/prf$$.xml
  tpdb=$1
+ coq=./tmp/prf$$.v

  ./TTT2/ttt2-cert $tpdb > $prf
***************
*** 19,27 ****
    echo "MAYBE"
  else
-   echo "YES"
    tpdb2xml $tpdb > $pb
!   prf2coq $pb $prf
! fi

! rm ./tmp/*.xml

--- 20,34 ----
    echo "MAYBE"
  else
    tpdb2xml $tpdb > $pb
!   prf2coq $pb $prf > $coq
!   if test $? -ne 0
!   then
!      echo "MAYBE"
!   else
!      echo "YES"
!      cat $coq
!   fi

! fi

+ rm ./tmp/*.xml ./tmp/*.v

-----Original Message-----
From: termtools-bounces at lists.lri.fr on behalf of Claude Marché
Sent: Wed 6/6/2007 17:10
To: termtools at lri.fr
Subject: RE: [Termtools] certified - strange proofs
 

The purpose of "disqualification" is to make clear on the web page
that some YES answers may be wrong. And to warn people that would like
to download the tool and use it may get wrong answer. 

To avoid disqualification, I need to change the result page so that
wrong answers do not appear in green anymore. For that, I need a fix:
please send me new runme/checkme scripts.

- Claude


-- 
Claude Marché                          | tel: +33 1 72 92 59 69           
INRIA Futurs - ProVal                  | mobile: +33 6 33 14 57 93 
Parc Orsay Université - ZAC des Vignes | fax: +33 1 74 85 42 29   
3, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |




 

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools


-------------- next part --------------
A non-text attachment was scrubbed...
Name: runme
Type: application/octet-stream
Size: 409 bytes
Desc: runme
Url : http://lists.lri.fr/pipermail/termtools/attachments/20070606/aad5e0a1/runme.obj