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

[PVS-DEVEL] CMU Lisp port update

I just thought I'd let you know where things stand.

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.

- 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.

- 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.