		Search-engine friendly clone of the ACL2 documentation.

Developers-guide

Developers-guide-miscellany

Miscellaneous Information

The initial version of this chapter is little more than a stub. It will probably always benefit from expansion to cover more topics.

Trust tags

See defttag for user-level information about trust tags. The ``Essay on Trust Tags (Ttags)'' provides a lot of relevant background on trust tags at the implementation level. A particularly important point to be emphasized here is the following: The critical aspect of trust tags is that whenever a trust tag is activated, the string "TTAG NOTE" must be printed to *standard-co* (see the definition of print-ttag-note), with the exception that if ttag notes are deferred then initially, only the first such is printed; see set-deferred-ttag-notes. The paper ``Hacking and Extending ACL2'' from the 2007 ACL2 Workshop may be helpful.

Fixnums

In general, Common Lisp computations with numbers are much faster when they only deal with ``small'' numbers called fixnums. See the ``Essay on Fixnum Declarations'' for information about fixnums and ACL2, including a description of the ranges for 32-bit fixnums in different Common Lisp implementations as of this writing. There may be some opportunities made available by modern Lisps that have 64-bit implementations. (CMUCL seems to be an exception.)

Infix printing is no longer supported

At one time ACL2 had support for infix printing, which was used rarely if at all. Infix code is still present, conditioned by feature :acl2-infix, but it has probably been quite some time since it was tested. Perhaps it is time to remove all such code; indeed, the release notes for Version 8.0 (see note-8-0) say that ``The (minimal) support for infix printing has been removed.''

NEXT SECTION: developers-guide-releases