Hi,
I am one of the co-maintainers of OpenMCL under the darwinports
infrastructure
(http://darwinports.opendarwin.org). I had previous set up OpenMCL to
automatically
bootstrap under darwinports, and versions 0.13.[567] had worked well.
I've also patched the theorem proving system ACL2 (version 2.7) to
build using
OpenMCL. (The patches should be incorporated into the next version.)
ACL2 is
a good test of a lisp, as it has a very extensive regression test suite.
Preliminaries aside, 0.14.1-pl1 breaks ACL2. The breakage is not
subtle, so the problem
is probably not too complicated. Starting openmcl with the acl2 heap
image
openmcl --eval "(acl2::lp)" --image-name <path to>/saved_acl2
is supposed to start the ACL2 theorem prover's internal repl (that's
what the (acl2::lp)
does). But the internal repl doesn't seem to recognize ACL2's
definitions. For example,
it just hangs forever when you try the simplest example,
(thm (equal (car (cons (x y)) x))
which would prove that the car of the list (x y) is x. This should take
only a few milliseconds.
Now, it's perfectly possible that OpenMCL is behaving completely
correctly. ACL2
usually builds under gcl, which is far from ANSI compliant, so maybe
the ANSI fixups
that Bryan O'Connor has worked so hard on have shown up a bug in ACL2.
But ACL2
also builds under Allegro CL, which is considerably more compliant than
gcl.
How do I start tracking down where the trouble lies? I didn't have any
failures during the
build of 0.14.1-pl1, and ACL2 builds a heap image without complaining,
but it doesn't
work properly.
Any advice would be appreciated.
Best Wishes,
Greg
Gregory Wright
Antiope Associates LLC
18 Clay Street
Fair Haven, New Jersey 07704
gwright@xxxxxxxxxxx
|
