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