Camm,
I've been able to build ACL2 and certify its books using GCL 2.7.0 t1 and t2. In attempting to certify our local books, however, I seem to have come across a resurrected proclaim problem. Problems of this sort were first noticed by Dave Greve back in the fall of 2003, and you replied with a patch :
http://lists.gnu.org/archive/html/gcl-devel/2003-09/msg00137.html
Also note my follow-up message, which generalized the issue:
http://lists.gnu.org/archive/html/gcl-devel/2003-12/msg00051.html
which led to a second patch:
http://lists.gnu.org/archive/html/gcl-devel/2003-12/msg00113.html
With 2.7.0 t1 and 2.7.0 t2, Dave's original example works OK:
(proclaim '(ftype (function ((satisfies symbol-listp)) t) foo))
NIL
But, try, for example
(proclaim '(ftype (function ((satisfies symbol-listp)) t) goo))
or
(defun mypredp (x) t)
(proclaim '(ftype (function ((satisfies mypredp)) t) foo))
With GCL 2.6.5, for example, all of the above examples return NIL. However, GCL 2.7.0 t1 and t2 give
Error: (SATISFIES <predicate name>) is not of type STRING.
There have been a number of changes to gcl_predlib.lsp, which is where the earlier patches to address this issue were applied, so I suspect that something related to the earlier patches has been undone in the process.
Thanks in advance for any help you can provide on this; I suspect that if this problem were solved, I could successfully certify my books with GCL 2.7.0 t1 and t2, as I have been able to do with GCL 2.6.6 twc.
David Hardin
_______________________________________________ Gcl-devel mailing list [email protected] http://lists.gnu.org/mailman/listinfo/gcl-devel
