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

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




Sam, this is very useful, thanks.  I think this gets me to the point 
where I can consider the problem "benign" as suggested in the posting I 
found :-).

One thing that is not explicitly stated in your email is that once you 
have got back the the * prompt, you then need to go and restart the 
proof, and thereafter (he says optimistically after very limited testing 
:-)) there are no problems.  When I was unable to make any progress in 
the debugger window previously, I felt that I had no option but to kill 
pvs and start again, and thus I could never get to the point of seeing 
this as benign.  In case these answers are available to others, adding 
this point explicitly may help others too.

Thanks again!

Cheers

Mark

Sam Owre wrote:
> 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
>>
>>
>>
>>
>>
>>