acl2 - 为什么 cert.pl 抱怨 ttags

Question

在认证 ACL2 书籍时，我经常收到以下错误消息：

| ACL2 Error in ( INCLUDE-BOOK "something" ...):  The ttag :FAST-CAT
| associated with file /elided/acl2/books/std/string\
| s/fast-cat.lisp is not among the set of ttags permitted in the current
| context, specified as follows:
|   NIL.
| See :DOC defttag.

怎么了？

Answer 1

需要将一个<something>.acl2文件（通常cert.acl2工作得很好）添加到包含您要认证的书的目录中。该<something>.acl2文件需要直接cert.pl使用ttags，例如，使用以下代码：

(in-package "ACL2")

; cert-flags: ? t :ttags :all