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 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:
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.