(include-book "foo" :dir :system) fails due to wrong path in :system

[Mark Reitblatt]

Binary package hint: acl2

ACL2 !>(in-package "ACL2")
 "ACL2"
ACL2 !>(include-book "arithmetic-3/extra/top-ext" :dir :system)

ACL2 Error in ( INCLUDE-BOOK "arithmetic-3/extra/top-ext" ...): There
is no file named
"/build/buildd/acl2-3.1/books/arithmetic-3/extra/top-ext.lisp" that
can be opened for input.

Summary
Form: ( INCLUDE-BOOK "arithmetic-3/extra/top-ext" ...)
Rules: NIL
Warnings: None
Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)

******** FAILED ******** See :DOC failure ******** FAILED ********
ACL2 !>

[Mark Reitblatt (mark-reitblatt)]

Workaround: set env variable ACL2_SYSTEM_BOOKS="/usr/share/acl2-3.1/books"

[Barry deFreese (bddebian)]

Even setting that variable doesn't work for me, nor do I see a top-ext.lisp file installed anywhere?? Thanks.

[wolfger (wolfger)]

5 months without a response. We are closing this bug report because it lacks the information we need to investigate the problem, as described in the previous comments. Please reopen it if you can give us the missing information, and don't hesitate to submit bug reports in the future. To reopen the bug report you can click on the current status, under the Status column, and change the Status back to "New". Thanks again!