• Top
    • Documentation
    • Books
      • Cert.pl
      • Community-books
      • Project-dir-alist
      • Bookdata
      • Book-hash
      • Uncertified-books
      • Sysfile
      • Show-books
      • Best-practices
      • Books-reference
        • Include-book
        • Certify-book
        • Cbd
        • Set-write-ACL2x
        • Book-compiled-file
        • Add-include-book-dir
        • Pathname
        • Add-include-book-dir!
        • Full-book-name
        • Delete-include-book-dir
        • With-cbd
        • Delete-include-book-dir!
        • Set-cbd
          • Certify-book-debug
        • Where-do-i-place-my-book
        • Books-tour
      • Recursion-and-induction
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Books-reference

    Set-cbd

    To set the connected book directory

    Example Forms:
    ACL2 !>:set-cbd "/usr/home/smith/"
    ACL2 !>:set-cbd "my-acl2/books"

    See cbd for a description of the connected book directory.

    General Form:
    (set-cbd str)

    where str evaluates to a nonempty string that represents the desired directory (see pathname). This command sets the connected book directory according to that string; see cbd. Thus, this command may determine which files are processed by include-book, certify-book, and ld commands, as well as by file operations such as open-input-channel.

    IMPORTANT: Pathnames in ACL2 are in the Unix (trademark of AT&T) style. That is, the character ``/'' separates directory components of a pathname, and pathnames are absolute when they start with this character, and relative otherwise. See pathname.