0

エラーメッセージの意味を理解しようとしているので、修正することを検討してください。次のエラーを修正する正しい方法は何ですか? :oslib、:quicklisp、および:quicklisp.osicatを 内の include-books に追加する必要があり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 book が現在これら 3 つの ttag のみを必要としているとしても、将来、誰かが何らかの方法でそれを拡張し、追加の信頼タグが必要になる可能性があることです。これが発生した場合は、それを含めたすべての場所を、この制限された信頼タグのセットで更新する必要があります。これに多くの本を掛けると、手に大きな混乱が生じます。

とにかく、信頼タグの使用を本当に制限したい場合は、これらの制限をファイルのcert-flagsセクションにcert.acl2配置して、個々のインクルードではなくディレクトリの粒度で制御できるようにすることをお勧めします。詳細については、カスタム certify-book コマンドを参照してください。

于 2014-11-24T01:50:04.023 に答える
0

本に ttag 自体を含めることを許可するには、次のように ttag を括弧で囲みます。

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