Failures caused by useless-runes
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,
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 .email@example.com
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
; cert-flags: ? t :useless-runes nil