[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?
(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)))))
许庆国 <firstname.lastname@example.org> wrote:
> 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!
> Q.G., XU