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

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



Hi Mark,

I still don't know exactly what is going on.  It seems that the CMU Lisp
build is in a state where the first error it encounters causes a nested
error problem.  Oddly, if you simply type :abort after that, things seem
to work correctly (at least for me).  I tried googling for this problem,
and have started looking into the CMU Lisp source code, but I still
don't know what is going on.

Could you try starting up PVS, then go to the end of the *pvs* buffer,
and type foo - it should give the same error, but after that it should
work correctly.  Hopefully this is a workaround until I can figure out
what is going on with the CMU Lisp build process.

CMU Lisp is a bit confusing in this state.  It first tries to drop you
in the debugger, and says to type H for help, but then hits the nested
error problem and aborts out of the debugger, where H no longer means
anything.  At this point you are not in the prover, nor in the debugger,
but at the lisp prompt (which is * in CMU Lisp).  Thus it tries to
interpret H, Q, etc as Lisp symbols, and they have no value.  Typing
them thus invokes the debugger (the * prompt is replaced with a number
followed by some square brackets), and now H and Q are interpreted as
debug commands.

In general, try to stay out of the debugger, as it is only useful if you
are trying to debug the Lisp code.  If you are not running a proof and
you notice the prompt is not *, type :abort at the prompt until a *
appears.  Normally, if you break into lisp during a proof, you can
recover by typing (restore), but this won't work with the very first
error after startup.  This is why I suggest forcing an error as above.

I hope this explains things,
Regards,
Sam Owre

Mark Moir <mark.moir@oracle.com> wrote:

> 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
> 
> 
> 
> 
> 
>