[Top][All Lists]

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

[Gcl-devel] Another proclaim problem in GCL 2.7.0 t1 and t2

From: dshardin
Subject: [Gcl-devel] Another proclaim problem in GCL 2.7.0 t1 and t2
Date: Sat, 2 Jul 2005 05:01:10 -0500


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 :


Also note my follow-up message, which generalized the issue:


which led to a  second patch:


With 2.7.0 t1 and 2.7.0 t2, Dave's original example works OK:

(proclaim '(ftype (function ((satisfies symbol-listp)) t) foo))


But, try, for example

(proclaim '(ftype (function ((satisfies symbol-listp)) t) goo))


(defun mypredp (x) t)

 '(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

reply via email to

[Prev in Thread] Current Thread [Next in Thread]