[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] show proofs


There is a bug here, due to a change in the way proofs are stored in PVS
5.0, though I'm not certain why you're having problems in 4.2.  Could you
try adding the following code to ~/.pvs.lisp (create it if it doesn't
exist), restart PVS, and let me know if the problem is still there?

Sam Owre

(in-package :pvs)

(defun get-editable-justification (prf)
  (if (integerp (cadr prf))
      (let ((mprf (nth (cadr prf) (cddr prf))))
	 (if (> (length mprf) 9) (fifth mprf) (fourth mprf))))
      ;; Old style proof - need to remove (:new-ground? t) entry if there
      (if (consp (car (cdr prf)))
	  (editable-justification (cddr prf))
	  (editable-justification (cdr prf)))))


许庆国 <qgxu@mail.shu.edu.cn> wrote:

> Hello, 
> every one
> When the command "show-proofs-pvs-file " is issued,  
>  PVS give the error message "SPC-scroll, I-Igore.... B-break:" in the  min buffer and  the hints  "Error:  No methods applicable for generic function" in some buffer.
>  the other simliar command such as  "show-proofs-theory" give me the same error.
> Note: 1) Both PVS 5.0 and PVS 4.2 have the same  symptom.
>          2) PVS is running in the Ubuntu 10.10 under the the VMware workstation 7.0.1.  
>         2) my emacs' version is  23.1.1. 
> Thanks for your help!
> 2011-06-19 
> Q.G., XU