ACL2 development examples
This topic discusses issues encountered during ACL2 development using two examples. It consists of notes for the following talk.
Title: Some Illustrations of ACL2 Development
Speaker: Matt Kaufmann
Date/venue: March 31, 2023, over zoom
Follow this link to see a video recording of the talk (
(WARNING: This is *NOT* a typical ACL2 talk! It is focused on implementation, not ACL2 usage, to help those who may want to contribute ACL2 source code in the future. There are no specific prerequisites; but, for example, you'll be lost if you don't know what is meant by “error triple”.)
ACL2 development continues to be the responsibility of J Moore and me. But we envision a time when others may take on that role. To that end we hosted “Developer's Workshops” in 2017 and 2018, added documentation topic developers-guide to the manual, and added community-books file
books/system/to-do.txt. This talk continues towards developing developers.
This talk will use recent examples to illustrate ACL2 development.
WARNING. Although I'm trying to provide training for others to do
ACL2 development, contact me first if you want your development work to make
it into the system (as per “WARNINGS” near the top of community-book file
For another example illustration of ACL2 development issues, see my paper “Abbreviated Output for Input in ACL2: An Implementation Case Study”, either the slides or the paper, in Proceedings of ACL2 Workshop 2009.
Mark Greenstreet found that when he used ACL2,
This is a good time to take a look at the documentation for set-warnings-as-errors.
I changed warnings to hard errors, not soft errors, because changing them to soft errors could be a massive undertaking.
Example call stack:
print-summary [which returns state] calls print-redefinition-warning [which returns state] calls warning$
SOLUTION. Convert warnings to hard errors,
This illustrates an important trade-off: don't sacrifice quality, but if we can get something useful and correct for 10% (or less!) of the effort it would take to get something perfect — e.g., converting warnings to hard errors instead of soft errors — that's possibly quite fine. It's a judgment call.
This task took me something like 10 hours or maybe a bit more, even though this seemed like a relatively easy task. That's more time even than it took me for the more subtle changes in the second example below.
It took non-trivial time to develop tests and documentation; more on that below.
Note that while
The definitions of
I had to add to
(defrec state-vars (((safe-mode . boot-strap-flg) . (temp-touchable-vars . guard-checking-on)) . ((ld-skip-proofsp . temp-touchable-fns) . ((parallel-execution-enabled . in-macrolet-def) do-expressionp warnings-as-errors . inhibit-output-lst))) nil)
Related changes, for example deprecating
Testing is obviously important, and the run-script utility was very helpful, especially for this effort. During development I added to the tests incrementally, and I checked that new mods didn't introduce unfortunate changes to the output.
I added the following files to test output; see run-script.
books/system/tests/warnings-as-errors-input.lsp books/system/tests/warnings-as-errors-book.acl2 books/system/tests/warnings-as-errors-book.lisp books/system/tests/warnings-as-errors-log.txt
So, warnings produced by
(redef+) (make-event `(defconst *standard-co* ',(standard-co state))) (redef-)
This section discusses several design issues.
ISSUE. How does setting warnings as errors interact with inhibiting warnings?
Recall that essentially all warnings can be turned off (inhibited) with(set-inhibit-output-lst '(... warning ...))
or one can turn off only certain warning types (what the sources call the “summary strings”) with a call such as the following.(set-inhibit-warnings "theory" "use")')
warning$is called but the warning is inhibited, does that affect whether the warning is converted to an error?
Demo:(thm (equal x x) :hints (("Goal" :use nth))) ; warning (set-warnings-as-errors T '("use") state) (thm (equal x x) :hints (("Goal" :use nth))) ; error (set-inhibit-warnings "USE") (thm (equal x x) :hints (("Goal" :use nth))) ; quiet (set-warnings-as-errors :always '("use") state) (thm (equal x x) :hints (("Goal" :use nth))) ; error
The demo shows that I decided to provide two settings for converting warnings to errors:
Tfor causing an error only if the warning is to be printed, and :ALWAYSwithout that restriction.(set-warnings-as-errors T types state) (set-warnings-as-errors :ALWAYS types state)
ISSUE. Can we convert warnings to errors regardless of the type (summary string).
Solution:(set-warnings-as-errors flg :ALL state)
The documentation explains that we can do that and then go back to just warnings for specific types.
ISSUE. If a warning is converted to an error, is printing controllable?
(hard-error ctx (cons summary str) alist)
Quoting :DOC set-warnings-as-errors:
When a warning of a given type (possibly
niltype) is converted to a hard error as specified above, then whether that error is printed is controlled by the usual mechanism for suppressing error messages; see set-inhibit-er. Note that the error will still be signaled regardless of whether the error message is thus suppressed.
ISSUE. Some warnings are intended to be followed by errors, so we avoid converting those warnings to errors, as explained in :DOC set-warnings-as-errors. NOTE: Some of you may have noticed recent testing failures that were missing such warnings, and the following from that :DOC addresses that problem.
ISSUE. How about make-event expansion? We allow
Previous evaluations of calls of
set-warnings-as-errorsare ignored during certify-book and include-book. The handling of warnings as errors is restored at the end of these operations to what it was at the beginning.
For that devel-check process, I needed to modify guard verification for
(verify-termination-boot-strap warnings-as-errors-val-guard) ; and guards (verify-termination-boot-strap warnings-as-errors-val) ; and guards
But where did I put them? A guiding principle in ACL2 development is to
follow precedent when feasible. So I added those forms in the following
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; Miscellaneous verify-termination and guard verification ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
Guard verification for
Well, that's not exactly a complication — but documentation can be time-consuming to write!
For this task I documented set-warnings-as-errors. I think it helped that as I implemented stuff, I kept notes on what to remember to document.
J and I write a lot of comments, but here's a small remark on defrec and comments.
Maybe I should add a comment in the following that the
:defaultfield is nil, t, or :always. But I think that's pretty clear if one reads the :DOC for set-warnings-as-errors and does a tags-search for warnings-as-errors.
Notice the ‘cheap’ flag of
nil, which causes accesses to check that we indeed have a warnings-as-errorsrecord. We can use :trans1 on the above defrec call to see how the generated definition of weak-warnings-as-errors-pdepends on the cheap flag. Maybe some day I'll be confident enough to change that nilto t.
This advice is from both me (Matt) and J.
When I change ACL2 sources, I always do a fresh “
make clean-books ; (time nice make -j 16 regression-everything \ USE_QUICKLISP=1) >& \ make-regression-everything-ccl-quicklisp-j-16.log&
But when there are changes to logic-mode functions, I often run the following two tests as well.
This causes ACL2 to “prove its way” through parts of the sources, adding a bit of extra assurance.
See verify-guards-for-system-functions for information about this test. That provides instructions, but I usually follow a comment in
My patch file may be found in
It may be instructive to compare it with ACL2 sources from git commit 55d5fff82d920f9cd42943aa26cf58d44d6a333d, which was a version shortly before warnings-as-errors was added).
The very first function in that patch file,
Quoting :DOC note-8-6:
A new ld special, ld-always-skip-top-level-locals, has the effect of skipping local top-level forms. Thanks to Sol Swords for requesting such a capability, to support faster loading of
.portfiles by the build system (see build::cert.pl).
(local (include-book ...)) ; form in a .port file to be ignored
then I decided to add an
(ld "foo.port" :ld-always-skip-top-level-locals t)
Why not just do this by adding a new possible value for ld-skip-proofsp?
There are two dimensions of
- Skip proofs or not
- Skip locals or not
ld-skip-proofspalready support three of the four combinations, as follows.
do not skip proofs, do not skip locals
skip proofs, skip locals
skip proofs, do not skip locals
So why not have a fourth value as follows?
do not skip proofs, do skip locals
The reason is that it's too easy to make a mistake. In particular, a non-
nilvalue of (f-get-global 'ld-skip-proofsp state)currently means “proofs are being skipped”. That would no longer be the case if the value can be 'skip-locals— so many changes would have to be made, and some may be in proprietary books. Also, the name doesn't fit ld-skip-proofsp, since the new 'skip-localsvalue is not about skipping proofs.
So what did I do?
I added a new
ld-always-skip-top-level-localsI tags-searched for ld-missing-input-ok to find code to modify; also, I searched books/(both .lispand .acl2files).
IMPORTANT: Ignore the new
nilfor encapsulatebut not prognwas easy. The trick was to bind ld-always-skip-top-level-localsto nilin process-embedded-events, not eval-event-lst. One learns about such utilities over time.
WHAT'S IN A NAME?
At one point during development, the name was
ld-always-skip-locals; I changed it to ld-always-skip-top-level-locals,given the encapsulatebehavior. I don't mind that the name is long; I don't expect widespread usage, just occasional use in tools like cert.pl.
NEXT SECTION: developers-guide-ACL2-devel