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

[Sam Owre <owre@xxxxxxxxxxx>]

Hi Henning,

It sounds like you may have run into a bug here - could you send me your
specs so I can try and resolve it?  Also, let me know which version of PVS
you're using.

Thanks,
Sam

Henning Thielemann <lemming@henning-thielemann.de> wrote:

> 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.