|
|
|---|
|
|
|
|---|
Topics Not Covered
There are many aspects of the ACL2 implementation, even major ones, that aren't covered in this Development Guide.
ACL2 has been maintained for more than 25 years by people who don't recall very much about large portions of the source code, probably the majority of it. The key is that when making changes, one explores relevant code, reading relevant user-level documentation and code comments (including Essays), and talking with other developer(s) about questions and issues. System maintenance generally gets easier with experience.
Here is a partial list of topics, in no particular order, that are left
uncovered by this guide, or largely so: defproxy and (except for brief
mention) defattach; stobjs, including nested stobjs and
abstract stobjs; arrays; hons, memoization, and fast-alists (see hons-and-memoization); the serialize reader and writer; apply$; make-event; metafunctions and clause-processors; hints, including computed-hints, default
hints, override-hints, and custom keyword hints; wormholes;
printing, including evisceration (see evisc-tuple), iprinting,
pretty-printing, fmt, cw, print-object$ and with-output; constraints and functional-instantiation; the
documentation system; the prover, including the waterfall, the
rewriter (for example break-rewrite, congruences and patterned
congruences, the rewrite-cache, etc.), the tau-system, forward-chaining, and much more; pathnames, including canonical-pathnames; encapsulate and functional-instantiation,
including the
But again, the Guide is not intended to be complete. In principle, at
least, you can learn about any of the topics above when necessary, by reading
user-level documentation and using the Emacs tags-search and
Perhaps this Guide will be expanded in the future. If so, the expansion should probably not duplicate code comments, but rather, provide overview information and perspective with pointers to those comments.
NEXT SECTION: developers-guide-examples