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

Re: [PVS-Help] Re-running proof does not update proof status in *.prf file



Hi Sam,

Thank you very much for your response. I tried the patch you gave me and
PVS seemed to accept it fine. When PVS loaded up, in the status bar I got:

Compiling patch file .pvs
Compilation complete: loading ~/.pvs.lfasl
Context changed to ...
Loading pvs-load...done

If I take a file with initial proofs, run prove-theory, close PVS and then
re-open it, it remembers the proof status which I don't think it was doing
before. However, it seems to be doing this via *.bin files, not the *.prf
files. The *.prf file is still not being updated.

I re-checked my initial proof file format and it is slightly different
from what I described in my previous email. I am setting the proof status
to be 'nil', not 'untried'. I don't think that is relevant but I thought I
would tell you in case it is. I tried using 'untried' and 'unproved' as my
initial proof statuses but those didn't seem to work either.

Thanks,
Thomas


On Thu, May 24, 2007 6:56 pm, Sam Owre wrote:
> Hi Thomas,
>
> I view this as a bug; the .prf files should save this.
>
> Could you try adding the following code to your ~/.pvs.lisp file
> and see if that fixes it?  I haven't had time to test it much
> directly, but it should work.
>
> Thanks,
> Sam
>
> --Add to ~/.pvs.lisp----
>
> (defun pvs-prove-decl (decl retry?)
>   (setq *current-theory* (module decl))
>   (cond ((and (or (justification decl)
> 		  (eq (kind decl) 'tcc))
> 	      (or retry?
> 		  (unproved? decl)))
> 	 (let ((*rerunning-proof* (format nil "Proving ~a.~a"
> 				    (id *current-theory*) (id decl)))
> 	       (*rerunning-proof-message-time* (get-internal-real-time))
> 	       (orig-status (proof-status decl)))
> 	   (setf (proof-status decl) 'unproved)
> 	   (cond ((justification decl)
> 		  (pvs-message "Rerunning proof of ~a" (id decl))
> 		  (let ((pstat (rerun-prove decl)))
> 		    (pvs-message
> 			"~a ~aproved in ~,2,-3f real, ~,2,-3f cpu seconds"
> 		      (id decl) (if (unproved? decl) "un" "")
> 		      (real-proof-time decl) (run-proof-time decl))
> 		    (when (eq (proof-status decl) 'unproved)
> 		      (setf (proof-status decl) 'unfinished))
> 		    (update-context-proof-status decl)
> 		    pstat))
> 		 (t (pvs-message "Proving ~a..." (id decl))
> 		    (prove-tcc decl)))
> 	   (unless (eq (proof-status decl) orig-status)
> 	     (setq *justifications-changed* t))))
> 	((or (justification decl)
> 	     (not (unproved? decl)))
> 	 (pvs-message "~a is already proved" (id decl))
> 	 nil)
> 	(t (pvs-message "~a has no proof" (id decl))
> 	   nil)))
>
> ------------
>
> Thomas Wilson <thomas@twil.net> wrote:
>
>> Date: Wed, 23 May 2007 15:34:30 +0100 (BST)
>> From: "Thomas Wilson" <thomas@twil.net>
>> To: pvs-help@csl.sri.com
>> Subject: [PVS-Help] Re-running proof does not update proof status in
>> *.prf
>> 	file
>>
>> Hi,
>>
>> I am using PVS version 3.1 (Feb 14, 2003) to prove Verification
>> Conditions
>> generated by my verification tool. I generate PVS theories with the
>> conjectures, along with *.prf files with initial proof attempts.
>> Currently
>> these initial proofs are simply '(grind)' which along with the
>> auto-rewrites can prove some simple VCs automatically. I flag their
>> proof
>> status as 'untried' initially. My tool reads the *.prf files to allow
>> the
>> user to track the progress of PVS proofs together with the details of
>> the
>> other forms of verification.
>>
>> My idea was to 're-run' these initial proofs for each theory to
>> discharge
>> any trivial VCs before interactively proving the remainder of the VCs. I
>> can do this using prove-theory and the initial proofs do work sometimes
>> but PVS does not update the details of the proofs in the *.prf file. I
>> had
>> expected it to change the status of the proofs to be 'proved' if the
>> proofs succeed but they remain 'untried' despite being reported as
>> 'proved' by display-proofs-theory. It only seems to update the *.prf
>> file
>> if I re-do a proof manually from scratch. At that point it also updates
>> the details of the other proofs and updates successful initial proofs to
>> 'proved'.
>>
>> I also get the same problem when I manually edit a *.prf file to copy
>> portions of a proof from one VC to another. PVS will accept the new
>> proof
>> script but, again, it doesn't write back to the *.prf file that it is
>> proved.
>>
>> How can I get PVS to update the details of my non-PVS-generated proofs
>> when I re-run them? Is there a workaround that you could suggest?
>>
>> If all the VCs in a file are proved by the initial proof attempts, the
>> only way I can get PVS to update the *.prf file is to arbitrarily
>> re-prove
>> one of the VCs manually. In the latest file I have been working on, I
>> had
>> to interactively verify all the VCs and I copied parts of the script
>> from
>> one proof to another. PVS again accepts the proofs and reports them as
>> 'proved' in display-proofs-theory but won't update the *.prf file. I
>> don't
>> want to have to manually re-enter one of the long proofs in this file to
>> force an update of the *.prf file! I don't really want to have to
>> manually
>> set the proof status of proofs to be 'proved' myself either, I would
>> rather PVS did that.
>>
>> I would be grateful for any advice you could give me.
>>
>> Thanks,
>> Thomas
>