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

Re: [PVS-Help] PVS 4, errors in Proof buffer?

As Rusty said, that's what it looks like so far.  Maybe Sam has more 
information, but from my observations, it seems to be a benign problem 
under CMU Lisp that occurs only once near the beginning of a session.  
It usually happens when you reach the end of the first proof (or quit 
the first proof).  After that, it doesn't happen again.  Not comforting, 
to be sure, but so far it hasn't shown itself to cause other problems.

Ben Di Vito

Baldwin Rusty O Civ AFIT/ENGE wrote:
> I was at the PVS class in Nov this year and had the same question.  The
> answer appears to be that CMU-Lisp is the culprit.  This message does
> not occur with Allegro Lisp.
> It's seems to be benign (but disconcerting)...
> Rusty 
> -----Original Message-----
> From: pvs-help-bounces+rusty.baldwin=afit.edu@csl.sri.com
> [mailto:pvs-help-bounces+rusty.baldwin=afit.edu@csl.sri.com] On Behalf
> Of Steve Johnson
> Sent: Thursday, December 13, 2007 2:53 PM
> To: pvs-help@csl.sri.com; Paul S. Miner
> Subject: [PVS-Help] PVS 4, errors in Proof buffer?
> Does anyone recognize this symptom?
> I'm running PVS 4 on some old sources and get an error in the
> proof-buffer.
> The full buffer content is attached, but the last few lines are:
>     <PVS *proof* buffer>
>      .
>      .
>      .
>     Q.E.D.
>     Help! 12 nested errors.  KERNEL:*MAXIMUM-ERROR-DEPTH* exceeded.
>     Debug  (type H for help)
>     (UNIX::SIGSEGV-HANDLER #<unused-arg> #<unused-arg> #.(SYSTEM:INT-SAP
>     #x3FFFCA64))
>     Source:
>     *
> I removed existing *.pvscontext* and *pvsbin/ *before invoking the
> Prover.
> *M-x step-proof* does not generate this error.
> Any ideas?
> Thanks,
> Steve Johnson