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

Re: [PVS-Help] PVS crashes on fc6 x86_64

Hi Robert,

There is an SBCL for x86_64, and SBCL is derived from CMU Lisp.  I
started to port PVS to SBCL, but it turned out the differences were
bigger than expected.  When I have time, I'll try and get back to

In the meantime, the 32 bit CMU Lisp version should work on a 64
bit machine (which is what I'm using), so I think there is a real
bug there.

Sam Owre

Robert Goldman <rpgoldman@sift.info> wrote:

> Aditya Kanade wrote:
> > Hi,
> > I installed PVS 4.1 (CMUCL version) on fc6 x86_64 and I am trying to
> > retypecheck and reprove all my existing PVS specifications which were
> > developed and checked using PVS 3.2 (on x86_32). However, the new
> > installation of PVS crashes while typechecking these specifications.
> > Particularly, I have several directories and I use
> > load-prelude-library option to import them in other subdirectories.
> > PVS simply gives an error message "Restarts:" while typechecking
> > theories.
> > 
> > I am suspecting if there is a problem with the installation of PVS on
> > x86_64. In that case someone else may have experienced similar
> > problem. Any suggestions to solve this problem?
> > Thank you,
> > Aditya.
> > 
> I can't help you for certain, but I'm pretty sure there's an SBCL for
> x86_64.  Would you care to try that instead of cmucl?