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

*To*: "Sam Owre" <owre@xxxxxxxxxxx>*Subject*: Re: [PVS-Help] Re-running proof does not update proof status in *.prf file*From*: "Thomas Wilson" <thomas@xxxxxxxx>*Date*: Thu, 24 May 2007 21:14:26 +0100 (BST)*Cc*: pvs-help@xxxxxxxxxxx*In-Reply-To*: <7817.1180029379@photon.csl.sri.com>*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <3531.86.112.205.33.1179930870.squirrel@www.cs.stir.ac.uk><7817.1180029379@photon.csl.sri.com>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx*User-Agent*: SquirrelMail/1.4.5

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 >

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

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

- Prev by Date:
**Re: [PVS-Help] Re-running proof does not update proof status in *.prffile** - Next by Date:
**[PVS-Help] Error: Expression must be a record type** - Prev by thread:
**Re: [PVS-Help] Re-running proof does not update proof status in *.prffile** - Next by thread:
**[PVS-Help] Simple (?) question on PVS - constants of functions ofother constants** - Index(es):