[Top][All Lists]

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

[Gcl-devel] More on proclaim error

From: dshardin
Subject: [Gcl-devel] More on proclaim error
Date: Fri, 5 Dec 2003 15:10:57 -0600

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


that the form:

 '(ftype (function
               ((satisfies integerp))

results in the error:

Error: (satisfies integerp) is not of type STRING

Camm noted in


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)

 '(ftype (function
               ((satisfies mypredp))

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.



reply via email to

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