Re: [PVS-Help] Circular dependencies in judgements of PVS 4.0

[Henning Thielemann <lemming@xxxxxxxxxxxxxxxxxxxxx>]

Hi Sam,

On Wed, 12 Sep 2007, Sam Owre wrote:

> This is actually a bug reported in
>
>  http://pvs.csl.sri.com/cgi-bin/pvs-bug?id=978
>
> 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?

I have

$ head ~/.pvs.lisp
;; Patch which eliminates wrong warnings on circular proofs

(eval-when (eval compile load)
   (fmakunbound 'get-judgement-tcc))

(defvar *possible-judgements* nil)

(defun pc-complete (decl)
   (let* ((*dependings* nil)
          (*proved-dependings* nil)

$ tail ~/.pvs.lisp
                     ;; No need to include proof-refers-to in this case
                     (let ((decls (union (refers-to fdecl)
                                         (remove-if-not #'tcc?
                                           (generated fdecl)))))
                       (pc-analyze* (union decls (possible-judgements fdecl)))))
                    (t (let ((decls (union (union (refers-to fdecl)
                                                  (proof-refers-to fdecl))
                                           (remove-if-not #'tcc?
                                             (generated 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.