Tidbits for People Wanting to Modify ACL2

Commonly Desired Information

Instructions for Building ACL2 without Make. Note that when a build fails, file workxxx contains instructions you can paste into your Lisp to replicate the failure.
Guide to the ACL2 proof process (waterfall) call structure and the ACL2 documentation on the waterfall and hints.

An ACL2 command for tracing functions related to the waterfall.
(trace$ waterfall waterfall1-lst waterfall1 waterfall0 waterfall0-with-hint-settings waterfall-step waterfall-step1 waterfall0-or-hit)
Guide to creating and testing patches for ACL2 - written by the ACL2 authors. Also see Kaufmann's suggestions for how to copy+paste a patch into the ACL2 source code using Emacs. The other consensus is that it is possible to test your patch on part of the regression suite by issuing a :q, load'ing your patch, and then calling save-exec. However, this doesn't work for all of the books, so if you really want to test a patch, you probably need to follow Kaufmann's instructions. Here's a link to the email discussion on the matter.

Note: to add your patch file to the list of files that ACL2 uses to make tag searches, append the patch directory and filename below "parallel-raw.lisp" at the end of the definition for make-tags, in file acl2-init.lisp. I've only gotten the emacs "tags-search" command to work, and it loops through everything twice, but at least it's something.

Another note: While ACL2's mutual-recursion mechanism is helpful for detecting when non-mutually-recursive functions should be defined outside a (mutual-recursion block, it is not perfect. So be aware that you might need to think a bit when you install those definitions into the ACL2 source code.
Jared Davis's note on creating books that are raw-Lisp only:

I recommend using tools/include-raw. It has some documentation and you can also see an example of using it in serialize/serialize.lisp.

Typically, foo.lisp is a book that (1) has some "phony" definitions of any functions I want to be visible in the logic, (2) has a "defttag" allowing me to call include-raw, then (3) ends with (include-raw "foo-raw.lsp"). Meanwhile, foo-raw.lsp has the raw-lisp definitions that smash the "phony" definitions, and also has any other raw-lisp code needed to support these definitions.

Keeping the raw-lisp code in a separate file works better than trying to use "set-raw-mode" because, e.g., you can use packages that aren't known to ACL2 (e.g., CCL::), floating-point numbers, etc., which are forbidden even in set-raw-mode code. And include-raw is basically intended to load a raw-lisp file "correctly," handling issues like when the book should be compiled so that parallel make doesn't cause trouble, whether and when the compiled file gets loaded, etc.
Book books/hints/basic-tests.lisp can be used as a very small set of syntax tests for ACL2. It contains forms that are checked to not admit by using make-event.
Lisp function pprint can be used to pretty print any term that looks ugly.
Using Hashtables to Find the Generation Point of a Problematic Cons in CCL. As an alternative, you can look into CCL's trace :backtraceargument.

To find out the shape of a function's return value, you can use function stobjs-out, e.g., as follows.

		ACL2 p!>(stobjs-out 'binary-append (w state))
		(NIL)
		ACL2 p!>(stobjs-out 'rewrite (w state))
		(NIL NIL)
		ACL2 p!>(stobjs-out 'waterfall (w state))
		(NIL NIL NIL STATE)
		ACL2 p!>

To find out what functions, macros, etc. changed between two versions of ACL2, you can use this script.
"Rune" is short for "rule-name".

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