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

[dshardin]

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