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

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



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