My Favorite Things in ACL2 Versions 8.4 and 8.5
(to the tune of "My Favorite Things" in D Minor)
Matt Kaufmann, ACL2 Workshop 2022, May 27, 2022
Sung by Holly Bell

Comments with hide when we rewrite a ground term,
Errors with output that won't make us squirm.
Soundness bugs fixed and the pleasure that brings,
These are a few of my favorite things.

[pause]

Print-gv uses the world that it should use.
Formatted printing works better -- that's good news!
Defun-nx can take state with no strings.
These are a few of my favorite things.

Raw-mode messed up
When maintaining
Stobjs and cbd.
But not any more and there are ignor-
able arguments ... in defun-sk!

[pause]

Bind-free hypotheses better by far,
With linear rules and with brr.
Defstub and defun-sk make less noise.
That makes them two of my favorite toys!

Trace levels print to the right output channel.
Improvements to acl2-doc are substantial.
A suitable error now occurs when the LOGIC version
  of an abstract stobj export has the foundational
  stobj as a formal parameter that is declared as
  a stobj.

Screw it.  Just read the release notes!
[arpeggio]
The End!