Tidbits for People Wanting to Modify ACL2

Commonly Desired Information


Common Errors

Type of Detail Detail
Symptom: In CCL, Error: value NIL is not of the expected type NUMBER
Cause: State could be bound to NIL, because you are returning one less value in an MV than needed.
Solution: Find the offending MV call by either (1) backtracing (2) getting far enough along in the ACL2 build process so that ACL2's shape analysis can be performed or (3) copy+paste the modified functions into an already built ACL2. I don't pretend that these are an "ultimate solutions." Even with these tricks, it can still take me many hours to find the offending mv or mv-let.
You can also try tracing the waterfall functions mentioned above and looking for a nil where state should be.
Random tricks to try: :b and :raw [frame number] and :form [frame number]
Symptom: Anything strange when ld'ing a book.
Cause: You might have forgotten to :q and (lp!) when there were separate raw Lisp and ACL2-loop definitions.
Solution: Use :q and (lp!) of course!
Symptom: Segfaults when building anything
Cause: GNU Make 3.81 is known to cause problems.
Solution: Kaufmann recommends version 3.80.
Symptom: You get an error message like the following at the end of building ACL2:
Failed check for coverage of functions with acl2-loop-only code differences! Please send this error message to the ACL2 implementors.
Missing functions: ((*PRIMITIVE-MACROS-WITH-RAW-CODE* (MSG)) (*PRIMITIVE-PROGRAM-FNS-WITH-RAW-CODE* NIL) (*PRIMITIVE-LOGIC-FNS-WITH-RAW-CODE* NIL))
Cause: ACL2 checks the installed functions and macros for raw Lisp code to increase the assurance of the tool.
Solution: Add the offending function or macro to the appropriate constant. In this example, msg needed to be added to the end of constant *primitive-macros-with-raw-code*.

Home

Valid XHTML 1.1!