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

Re: ILISP interrupt

John ---

If the prover breaks into lisp, for whatever reason, this
is a bug.  We don't believe that any prover commands break
like this in the new release of PVS (due shortly --- watch
this space!) but I'd be interested in receiving a description
of the errors you've encountered to make sure they've been
fixed.  Please send them to pvs-bugs@csl.sri.com

As for recovery, type (restore) to the lisp prompt to return
to the proof state prior to the crash into lisp.


Dr Dave Stringer-Calvert, Software Engineer, Computer Science Laboratory,
SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025-3493, USA.
Phone: (650) 859-3291    Fax: (650) 859-2844   Email: dave_sc@csl.sri.com