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

[PVS-Help] Problems with CMU Lisp version of PVS 4.2


I am having a problem using the CMU Lisp version of PVS 4.2 for Linux. 
My collaborator, who is in an academic institution and therefore uses 
the Allegro-based version, does not have the same problems.

There are a handful of problems I've seen so far, all similar in nature, 
so I'll start with this one.  Whenever I type


during a proof, I get the following error message:

Help! 12 nested errors.  KERNEL:*MAXIMUM-ERROR-DEPTH* exceeded.

Debug  (type H for help)

(UNIX::SIGSEGV-HANDLER #<unused-arg> #<unused-arg> #.(SYSTEM:INT-SAP 

Run time  = 0.056 secs.
Real time = 2.599 secs.

Whatever I try from this point doesn't get me anywhere.  I've tried 
ctrl-d, q, 0, H, etc.  For example, if I type q, I get this message:

Error in KERNEL::UNBOUND-SYMBOL-ERROR-HANDLER:  the variable Q is unbound.
    [Condition of type UNBOUND-VARIABLE]

   0: [ABORT] Return to Top-Level.

Debug  (type H for help)

Source: Error finding source:
Error in function DEBUG::GET-FILE-TOP-LEVEL-FORM:  Source file no longer 

0 and H don't work here, and I just get more of these kinds of error 

I have seen this thread:


which looks similar, but I cannot get to the point where I can consider 
the problem "benign", as I cannot recover from this, and always have to 
kill pvs and try again, and then I hit the same problem again.

It seems hard to imagine that I could have screwed up the installations 
instructions, since they are trivial.

Any suggestions how I can either resolve or work around this problem? 
Do other people have the same problem?  Thanks.