[Gcl-devel] More on proclaim error

[dshardin]

Hi, I'm David Hardin, and I'm working with Dave Greve and Matt Wilding on some ACL2 projects.  On 18 September, Dave reported an error with proclaim that appeared somewhere between GCL 2.2.2 and GCL 2.5.0, and that persisted in GCL 2.6.1.  Dave reported in 

http://mail.gnu.org/archive/html/gcl-devel/2003-09/msg00117.html

that the form:

(proclaim
 '(ftype (function
               ((satisfies integerp))
               t)
              foo))

results in the error:

Error: (satisfies integerp) is not of type STRING 


Camm noted in 

http://mail.gnu.org/archive/html/gcl-devel/2003-09/msg00158.html

that a preliminary fix had been made to gcl_predlib.lsp.  I applied this fix to my gcl-2.6.1-9 environment, and confirmed that Dave's original example problem was now fixed.  However, the real problem we are seeing in our ACL2 models is with user-defined predicates.  So, if I alter Dave's example slightly:

(defun mypredp (x) t)

(proclaim
 '(ftype (function
               ((satisfies mypredp))
               t)
              foo))

and run with the most recent gcl_predlib.lsp fix, I still get an error:

Fast links are on: do (si::use-fast-links nil) for debugging
Error signalled by PROCLAIM.
Broken at SYSTEM::NORMALIZE-TYPE.  Type :H for Help.


BTW, clisp 2.31 digests this latter example correctly, returning nil.


This problem is currently impeding our progress in a number of places, so any additional help would be appreciated.  We can't really go back to an older gcl where the problem does not occur (e.g., gcl 2.2.2 on Solaris), because we have moved from Solaris to Linux, and the older gcl's won't build on Linux.  BTW, we really need to use GCL, and not clisp or CMU CL, because we need C source code generation.


Thanks,

David