了解标签错误答案

【问题标题】：Understanding a ttags error了解标签错误
【发布时间】：2014-09-23 20:36:22
【问题描述】：

我正在尝试理解错误消息，以便我考虑修复它。修复以下错误的正确方法是什么？我是不是该将:oslib、:quicklisp 和:quicklisp.osicat 添加到包含书籍中在books/oslib/rmtree.lisp 里面？我的包含书表格错了吗？

ACL2 !>(include-book "oslib/top" :dir :system :ttags (oslib quicklisp
quicklisp.osicat))


ACL2 Error in ( INCLUDE-BOOK "oslib/top" ...):  The ttag :OSLIB associated
with file /<elided>/acl2/books/oslib/lisptype.lisp
is not among the set of ttags permitted in the current context, specified
as follows:

((:OSLIB "/<elided>/acl2/books/oslib/rmtree.lisp")
 :QUICKLISP :QUICKLISP.OSICAT).
See :DOC defttag.


Summary
Form:  ( INCLUDE-BOOK "oslib/top" ...)
Rules: NIL
Time:  0.47 seconds (prove: 0.00, print: 0.00, other: 0.47)

ACL2 Error in ( INCLUDE-BOOK "oslib/top" ...):  See :DOC failure.

******** FAILED ********
ACL2 !>

【问题讨论】：

标签： acl2

【解决方案1】：

我强烈建议始终在包含书籍上使用:ttags :all，或者完全省略:ttags 参数并抑制警告。例如，您可以这样做：

(include-book "oslib/top" :dir :system :ttags :all)

这看起来有点矫枉过正——既然知道本书只需要oslib、quicklisp 和quicklisp.osicat，为什么还要允许任何信任标签？只允许您知道自己需要的少数信任标签不是更安全吗？

问题是：尽管 oslib/top 书今天只需要这三个 ttag，但可能将来有人会以某种方式对其进行扩展，这将需要额外的信任标签.如果发生这种情况，您将必须更新每个已将其包含在此受限信任标记集中的位置。将其乘以许多书籍，您的手上就会一团糟。

无论如何，如果您真的想限制信任标签的使用，最好将这些限制放在您的cert.acl2 文件的cert-flags 部分中，这样您就可以在以下粒度上控制它们目录而不是单个包含。详情请见custom certify-book commands。

【讨论】：

【解决方案2】：

要允许书籍本身包含 ttags，请将 ttags 放在括号中，如下所示：

(include-book "oslib/top" :dir :system :ttags ((oslib) (quicklisp)
  (quicklisp.osicat)))

【讨论】：