[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
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 ...
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.
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.
> --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)))
> "~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)
> (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))
> (t (pvs-message "~a has no proof" (id decl))
> Thomas Wilson <email@example.com> wrote:
>> Date: Wed, 23 May 2007 15:34:30 +0100 (BST)
>> From: "Thomas Wilson" <firstname.lastname@example.org>
>> To: email@example.com
>> Subject: [PVS-Help] Re-running proof does not update proof status in
>> I am using PVS version 3.1 (Feb 14, 2003) to prove Verification
>> generated by my verification tool. I generate PVS theories with the
>> conjectures, along with *.prf files with initial proof attempts.
>> these initial proofs are simply '(grind)' which along with the
>> auto-rewrites can prove some simple VCs automatically. I flag their
>> status as 'untried' initially. My tool reads the *.prf files to allow
>> user to track the progress of PVS proofs together with the details of
>> other forms of verification.
>> My idea was to 're-run' these initial proofs for each theory to
>> 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
>> 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
>> 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
>> 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
>> script but, again, it doesn't write back to the *.prf file that it is
>> 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
>> one of the VCs manually. In the latest file I have been working on, I
>> to interactively verify all the VCs and I copied parts of the script
>> 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
>> 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
>> 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.