0

我正在尝试理解错误消息，以便我可以考虑修复它。解决以下错误的正确方法是什么？我应该去添加: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 !>
4

2 回答 2

1

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

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

这可能看起来有点过头了——当你知道本书只需要、和时，为什么还要允许这本书中的任何信任标签？只允许您知道自己需要的少数信任标签不是更安全吗？oslibquicklispquicklisp.osicat

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

无论如何，如果您真的想限制信任标签的使用，最好将这些限制放在文件的各个cert-flags部分中cert.acl2，这样您就可以在目录的粒度而不是单个包含中控制它们。有关详细信息，请参阅自定义 certify-book 命令。

于 2014-11-24T01:50:04.023 回答
0

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

(include-book "oslib/top" :dir :system :ttags ((oslib) (quicklisp)
  (quicklisp.osicat)))
于 2014-09-23T20:36:22.243 回答