[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Circular dependencies in judgements of PVS 4.0
On Wed, 12 Sep 2007, Sam Owre wrote:
> This is actually a bug reported in
> The bug is due to the improper treatment of judgements in checking for
> circularities. The (rather long) patch is available at the end of the
> above page. To use, simply copy the patch into ~/.pvs.lisp (creating it
> if necessary), and restart PVS.
Thanks for the pointer. However, with this fix the problem remains. How
can I check, that ~/.pvs.lisp was incorporated?
$ head ~/.pvs.lisp
;; Patch which eliminates wrong warnings on circular proofs
(eval-when (eval compile load)
(defvar *possible-judgements* nil)
(defun pc-complete (decl)
(let* ((*dependings* nil)
$ tail ~/.pvs.lisp
;; No need to include proof-refers-to in this case
(let ((decls (union (refers-to fdecl)
(pc-analyze* (union decls (possible-judgements fdecl)))))
(t (let ((decls (union (union (refers-to fdecl)
(pc-analyze* (union decls (possible-judgements fdecl))))))))))
Then I started PVS with the problematic PVS file and started
(prove-importchain). The proof is again marked as incomplete.