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

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




Hello

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

   (undo)

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 
#x3FFFC6E4))
Source:


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]

Restarts:
   0: [ABORT] Return to Top-Level.

Debug  (type H for help)

(EVAL Q)
Source: Error finding source:
Error in function DEBUG::GET-FILE-TOP-LEVEL-FORM:  Source file no longer 
exists:
   target:code/eval.lisp.
0]



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

I have seen this thread:

   http://pvs.csl.sri.com/mail-archive/pvs-help/msg01368.html

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.

Cheers

Mark