了解ttags错误

Question

我试图弄清楚错误消息，以便我可以考虑修复它 。什么是解决以下错误的正确方法？ 是否应将: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 !> 

Answer 1

为了让书籍包括ttags自己，将ttags在括号，就像这样：

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

Answer 2

我会强烈建议您始终使用 :ttags :all上包括书籍，或者只是省略完全的 :ttags参数

并抑制警告。举例来说，你可以这样做：

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

这似乎有点小题大做 - 为什么你会想从这本书允许任何信任标签，当你知道它只需oslib，quicklisp和quicklisp.osicat？相反，只允许您知道您需要的少数信任标签会更安全吗？

问题是：即使oslib/top book只需要这三个标签今天，可能有人会在将来以某种方式扩展它，这将需要额外的信任标签。如果发生这种情况，您必须更新每您已将此信息标签包含在该受限制的一组信任标签中。把这个数字乘以许多书籍，你的手上就会陷入一片混乱。

无论如何，如果你真的想限制信任标签的使用，最好将这些限制放在你的cert.acl2文件的cert-flags部分，以便你可以控制它们的目录粒度，而不是个人包括。有关详细信息，请参阅custom certify-book commands。