[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-DEVEL] CMU Lisp port update
On 30 May, 2006, at 21:33, Sam Owre wrote:
> I just thought I'd let you know where things stand.
Thank you for the update.
> I have merged in the changes into the PVS 3.3 sources, compiled
> everything in CMU CL 19c, and have typechecked and proved the prelude.
> I'm now working on getting through the validation suite.
> Here are some of the more significant changes I've made:
> - There is a strange behavior in CMU CL wrt slot names. For some
> reason, things like "(make-instance 'name-expr 'id 'foo)" works fine
> when interpreted, but when compiled an error is reported that
> "ID" is
> unbound. I tried to distill this to a small example so I could
> send a
> bug report, but I wasn't able to. The workaround is to change
> this to
> use keywords instead: "(make-instance 'name-expr :id 'foo)". It's a
> bit of a pain, but it does work in both Allegro and CMU CL.
This sounds familiar; we/I have experienced similar strangeness on
the earlier PVS work and on my OBJ3 work.
> - When I saved an image with mu.so preloaded, I could not get
> things to
> work - it segment faults (and reloading mu.so doesn't help). Not
> preloading mu.so causes problems loading bdd-cmu.lisp and mu-
> so I ended up moving the foreign function bits to bdd-cmu-load.lisp
> and mu-cmu-load.lisp, and modified pvs-init to load those.
Again, sounds familiar.
> - We moved to a case-sensitive version of Allegro a while back, and I
> had to make a few changes to be able to properly read in proofs
> in that form. It seems to be working OK so far.
> - In addition to those, there are lots of little things that came up,
> but they were generally easy to fix.
> It seems to run on my 64 bit linux machine, though I can't build it
> I will try to finish the validation this week, and checkin my changes
> shortly thereafter.
I'm very much looking forward to giving the new port a whirl.
School of Computer Science and Informatics