		Search-engine friendly clone of the ACL2 documentation.

Useless-runes-failures

When an event fails you may see the following message:

*NOTE*: Useless-runes were in use and can affect proof attempts.  See
:DOC useless-runes-failures.

This message may be printed after the usual failure message when a useless-runes file has been consulted during proofs, as is usually the case when using build system tools (see books-certification and build::cert.pl). It is intended to suggest that you consider removing or regenerating the associated useless-runes file in the situation described below.

Suppose that you have developed a book — say, foo.lisp — and placed it into the community-books. Then regression runs may occasionally generate (or regenerate) the associated useless-runes file. Now suppose you modify foo.lisp or some books that are included in it. You successfully run (certify-book "foo"); yet, certification of foo.lisp subsequently fails as part of a regression run or when you use build::cert.pl to certify foo.lisp. This could be unsettling!

In that case, what is probably happening is that the useless-runes file is no longer suitable. If you are a contributor to the ``ACL2 System and Community Books'' GitHub project (see git-quick-start), you can update repository as follows (followed by the usual actions when updating the repository).

git rm .sys/foo@useless-runes.lsp

Or, if you like, you could regenerate the useless-runes file, for example as follows.

(certify-book "foo" ? t :useless-runes :write)

Or if you prefer to avoid this useless-runes file from now on, you could add a line like the following to foo.acl2 (see build::custom-certify-book-commands) and also, ideally, delete the useless-runes file using the "git rm" command displayed above.

; cert-flags: ? t :useless-runes nil