Re: [PVS-DEVEL] CMU Lisp port update

[Joseph Kiniry <kiniry@acm.org>]

Hi Sam,

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- 
> cmu.lisp,
>   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  
> saved
>   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  
> there.
>
> 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.

> Cheers,
> Sam

Joe
---
Joseph Kiniry
School of Computer Science and Informatics
UCD Dublin
http://secure.ucd.ie/
http://srg.cs.ucd.ie/