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

[Kyongho Min <min@xxxxxxxxxxxxxxx>]

Dear members,

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