		Search-engine friendly clone of the ACL2 documentation.

Developers-guide

Developers-guide-examples

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 (.mov format).

Abstract:

(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 books/system/to-do.txt). (Of course, this will change when J and I are no longer the ACL2 maintainers.)

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.

EXAMPLE 1:
NEW FEATURE SET-WARNINGS-AS-ERRORS

Mark Greenstreet found that when he used ACL2, "Use" warnings would often be followed by proof failures. So he wanted those warnings to be errors in his sessions. Quoting :DOC note-8-6:

Added utility set-warnings-as-errors, which can change warnings to hard errors. Thanks to Mark Greenstreet for the idea and for discussions that were helpful in refining it.

This is a good time to take a look at the documentation for set-warnings-as-errors.

APPROACH: CONVERT WARNINGS TO HARD ERRORS

I changed warnings to hard errors, not soft errors, because changing them to soft errors could be a massive undertaking.

A soft error (er soft ...) returns (mv t nil state) after doing some printing. There is no error “signaled” — the caller needs to handle this appropriately.
The primary warning macro, warning$, returns state.
So how can we signal an error when a function returns state?

Example call stack:

print-summary [which returns state]
  calls
print-redefinition-warning [which returns state]
  calls
warning$

Another issue: warning$-cw0 returns nil, which makes it impossible to convert to a soft error (returning state). More on that is below.

SOLUTION. Convert warnings to hard errors, (er hard ...), which are really aborts.

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.

KEY SURPRISE: TIME TAKEN

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.

COMPLICATION 1: COMMENT-WINDOW WARNINGS

Note that while warning$ takes and returns state, warning$-cw0 does “comment window” printing without taking or returning state.

The definitions of warning$ and warning$-cw1 lead to similar calls of the macro, warning1-form. The lack of state available to warning$-cw1 leads to the use of the state-vars record (shown below), which contains state information and was originally introduced so that translate11, the main “translate” function, has access to some state components without taking state.

I'm not sure I'd use a macro like warning1-form now. I might instead just write analogous code for warning$ and warning$-cw1 and comments about keeping them in sync.
But as a rule, I take an incremental approach to ACL2 code development: building on what's there seems less error-prone and time-consuming than ripping things apart (unless there's a good reason rather than a minor stylistic one).

I had to add to state-vars, but I didn't want to worry about impacting efficiency. So my modification had minimal effect on only one existing field, namely, do-expressionp. From the source code at the time (comments omitted here):

(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 warning$-cw in favor of warning$-cw0, aren't discussed here.

COMPLICATION 2: RUN-SCRIPT

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

Recall that *standard-co* is the default character output channel for standard output (see io and that (standard-co state) is the current such channel. Run-tests redirects output so that (standard-co state) points to a file (the generated *-log.out file). Also note that warning$-cw1 uses *standard-co* and not standard-co, since changes to files should be recorded in the ACL2 state but warning$-cw1 doesn't take or return state.

So, warnings produced by warning$-cw1 were going to the terminal, not to the intended output file. Therefore I put the following hack near the top of warnings-as-errors-input.lsp.

(redef+)
(make-event `(defconst *standard-co* ',(standard-co state)))
(redef-)

COMPLICATION 3: INTERFACE DESIGN ISSUES

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")')
If 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: T for causing an error only if the warning is to be printed, and :ALWAYS without 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?

Solution: Yes, using (set-inhibit-output-lst ... error ...) or using set-inhibit-er. Regarding the latter, in warning1-form we find the following call that deals with the summary string.
(hard-error ctx (cons summary str) alist)
Quoting :DOC set-warnings-as-errors:

When a warning of a given type (possibly nil type) 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.

No warning whose type specified by constant *uninhibited-warning-summaries* is converted to an error. Those types are the ones that belong, with a case-insensitive check, to the list ("Uncertified" "Provisionally certified" "Skip-proofs" "Defaxioms" "Ttags" "Compiled file" "User-stobjs-modified"). This exception overrides all discussion below.

ISSUE. How about make-event expansion? We allow make-event to change state global warnings-as-errors; see the definition of *protected-system-state-globals*. But that setting will revert after certify-book or include-book, as noted below.

ISSUE. If I ship you a book, you'll want certify-book to succeed even if you are setting warnings as errors. So, again quoting :DOC set-warnings-as-errors:

Previous evaluations of calls of set-warnings-as-errors are 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.

COMPLICATION 4: GUARD VERIFICATION

The “make devel-check” process verifies guards for quite a few built-in functions: see verify-guards-for-system-functions, though I follow a comment in *system-verify-guards-alist*.

For that devel-check process, I needed to modify guard verification for bind-macro-args. I added the following two forms to the ACL2 sources.

(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 section of boot-strap-pass-2-a.lisp.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Miscellaneous verify-termination and guard verification
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Guard verification for bind-macro-args is (I think) why I used ec-call in warning1-form (e.g., for the call of warning$-cw1 in bind-macro-args-keys1).

COMPLICATION 5: DOCUMENTATION AND COMMENTS

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 :default field 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.
(defrec warnings-as-errors
  (default . alist)
  nil)
Notice the ‘cheap’ flag of nil, which causes accesses to check that we indeed have a warnings-as-errors record. We can use :trans1 on the above defrec call to see how the generated definition of weak-warnings-as-errors-p depends on the cheap flag. Maybe some day I'll be confident enough to change that nil to t.

So, the access call below checks that we have a valid record. Note the use of defabbrev to avoid evaluating x more than once.
(defabbrev warnings-as-errors-default (x)
  (and x ; else default is nil
       (access warnings-as-errors x :default)))

SOME GENERAL ADVICE before modifying sources

This advice is from both me (Matt) and J.

Read relevant documentation.
Read relevant Lisp comments in the source code.
Make up tests of new or modified features.
Keep back-ups along the way, copying/moving the saved/ directory.
Do regression testing.
Try to follow precedents.
Update documentation, including release notes.
For each bug discovered, even if it's not related to what you're doing, either fix it or make a note to come back to it.

TESTING SUMMARY

When I change ACL2 sources, I always do a fresh “make regression-everything” (except for comment-only changes), e.g., as follows.

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.

make proofs

This causes ACL2 to “prove its way” through parts of the sources, adding a bit of extra assurance.
make devel-check

See verify-guards-for-system-functions for information about this test. That provides instructions, but I usually follow a comment in *system-verify-guards-alist*.

THE PATCH FILE: SUMMARY OF CHANGES

My patch file may be found in books/system/doc/warnings-as-errors-patch.lsp.

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, output-ignored-p, is to fix a bug encountered in the process: “Tweaked output production, in particular from :pso”. Details are in the message for commit 55f20c02c15f9a2d7626060d7381eed3fc849933, which has been added at the end of the patch file. I fixed that bug as part of the work, rather than deferring its fix, because that helped with the warnings-as-errors implementation.

EXAMPLE 2:
NEW FEATURE SET-LD-ALWAYS-SKIP-TOP-LEVEL-LOCALS

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 .port files by the build system (see build::cert.pl).

Sol requested this because cert.pl loads .port files of included books (stemming from .acl2 files), but those may contain expensive local include-book forms books that should be ignored.

(local (include-book ...)) ; form in a .port file to be ignored

After

understanding the requested change,
being convinced of the change's utility,
helpful discussions with Sol, and
a helpful chat with J,

then I decided to add an LD special (see ld — think, keyword argument of LD). So after this change, Sol arranged for cert.pl to load .port files roughly as follows (see books/build/make_cert_help.pl).

(ld "foo.port" :ld-always-skip-top-level-locals t)

An LD special is good because:

it's documented where users will see it; and
it's bound rather than merely set — the original value is restored when the LD call returns.

QUESTION:

Why not just do this by adding a new possible value for ld-skip-proofsp?

ANSWER:

There are two dimensions of ld-skip-proofsp:

Skip proofs or not

Skip locals or not

Values of ld-skip-proofsp already support three of the four combinations, as follows.

nil —
do not skip proofs, do not skip locals

'include-book —
skip proofs, skip locals

t —
skip proofs, do not skip locals

So why not have a fourth value as follows?

'skip-locals —
do not skip proofs, do skip locals

The reason is that it's too easy to make a mistake. In particular, a non-nil value 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-locals value is not about skipping proofs.

QUESTION:

So what did I do?

ANSWER:

I added a new LD special, ld-always-skip-top-level-locals.

OLD TRICK:

To add ld-always-skip-top-level-locals I tags-searched for ld-missing-input-ok to find code to modify; also, I searched books/ (both .lisp and .acl2 files).

IMPORTANT: Ignore the new LD special when appropriate.

It is bound to nil for certify-book, include-book, and encapsulate. Those need to behave as intended, without skipping local events.

Binding to nil for encapsulate but not progn was easy. The trick was to bind ld-always-skip-top-level-locals to nil in 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 encapsulate behavior. 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