Понимание ошибки тегов

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 :all на включенных книгах, или просто опуская :ttags спор целиком и подавление предупреждений. Например, вы можете сделать:

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

Это может показаться излишним - почему вы хотите разрешить любые теги доверия из этой книги, когда вы знаете, что это нужно только oslib, quicklisp, а также quicklisp.osicat? Разве не безопаснее разрешить только те несколько доверительных тегов, которые вам нужны?

Проблема заключается в том, что, хотя для oslib/top book сегодня требуются только эти три тега, возможно, что в будущем кто-то каким-то образом расширит его, что потребует дополнительных тегов доверия. Если и когда это произойдет, вам придется обновлять каждое место, в которое вы включили его, с помощью этого ограниченного набора тегов доверия. Умножьте это на множество книг, и у вас будет большой беспорядок.

В любом случае, если вы действительно хотите ограничить использование тегов доверия, гораздо лучше поместить эти ограничения в cert-flags разделы вашего cert.acl2 файлы, так что вы можете контролировать их на уровне детализации каталогов, а не отдельных включений. См. Пользовательские команды certify-book для деталей.

Answer 2

Чтобы разрешить в самих книгах включать теги, поместите теги в скобки следующим образом:

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