Re: [PVS-Help] On Individual formula proof in a batch mode

[Sam Owre <owre@xxxxxxxxxxx>]

Hi Min,

When there is no error, prove-formula returns a proof tree, and
status-flag returns a slot of that.  But when things go wrong
(formula not found, etc.), it returns nil.  So your code should
be more like:

(defun my-prove-formula (theoryname formname)
  (let* ((*suppress-printing* t)
	 (*printproofstate* nil)
	 (*proving-tcc* t)
	 (prooftree (prove-formula theoryname formname t)))
    (if (and prooftree (eq (status-flag prooftree) '!))
        (format t "~%Formula proved")
	(format t "~%Formula unproved"))))

However, this does not explain why you get a void-function
error - you should be getting a "no methods applicable" error
if status-flag is applied to something other than a
proof tree. Are you using your own package?  If so, you may
need to invoke 'pvs::status-flag', or import the PVS package.
If this doesn't explain it, let me know.

As for batch, prove-formula is really for interactive use, and
doesn't work well in batch mode.  For PVS validations I use
pvs-validate-typecheck-and-prove My batch file for what you're
trying to do would look something like:

(pvs-validate "pvsbatch.log"
 "/tmp_amd/kamen/import/1/min/Haskell/Codes/2PVS"
 (pvs-validate-typecheck-and-prove "pvsbatch" nil nil "pvsbatch" "c1"))

The arguments to pvs-validate-typecheck-and-prove are:

  (filename &optional show-proofp importchainp theory formula)
  
Where: filename is the pvs filename (without the .pvs extension)
       show-proofp is t to show the proof details
       importchainp is t to prove all formulas of the importchain
       theory is the theory name (recall that a single pvs file
              may have many theories)
       formula is the name of the formula to be proved
If formula and/or theory are given, importchainp must be nil.
If formula is not given, then all formulas of the
   theory/pvsfile/importchain  are attempted.

Hope this helps,
Sam Owre
	
Kyongho Min <min@xxxxxxxxxxxxxxx> wrote:

> I tried to run PVS in a batch mode to prove each formula in a theory.
> I found good help but it does not work.
> The function definition is:
> 
> (defun my-prove-formula (theoryname formname)
>   (let ((*suppress-printing* t)
> 	(*printproofstate* nil)
> 	(*proving-tcc* t))
>     (if (eq (status-flag (prove-formula theoryname formname t)) '!)
>         (format t "~%Formula proved")
> 	(format t "~%Formula unproved"))))
> 
> the function (status-flag) return void-function error.
> If any knows why?
> 
> In addition,
> I ran the following el file (pvsbatch.el) to get some stdout.
> But the function (prove-formula "pvsbatch" "c1") returns the following
> error message in "pvsbatch.log" file.
> 
> pvsbatch.el::
> 
> (let ((my-formula-result nil)
>       (msg (pvs-validate "pvsbatch.log"
> "/tmp_amd/kamen/import/1/min/Haskell/Codes/2PVS"
>                (let ((current-prefix-arg t))
>                    (prove-formulas-pvs-file "pvsbatch")
>                    (setq my-formula-result
>                             (prove-formula "pvsbatch" "c1" t)))
>                     )))
>          (print (list 'my-prove-formula-result my-formula-result)))
> 
> 
> >>
> pvsbatch.pvs::
> pvsbatch: THEORY
> 
> BEGIN
> 
>  x1, x2: VAR int
> 
>  c1: LEMMA (x1 > 0) AND (x2 > x1) IMPLIES (x2 > 0)
>  c2: LEMMA (x1 > x2) AND (x1 > 0) IMPLIES (x2 > 0)
> 
> END pvsbatch
> >>
> 
> The result of pvsbatch.log is::
> >>
> ...
> 
> PVS file c1 is not in the current context
> Typecheck error: Can't find file for theory c1
> >>
> 
> 
> Great thanks for your help.
> 
> regards,
> 
> min