• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
          • World
          • Io
          • Wormhole
          • Programming-with-state
            • Error-triple
            • Cbd
              • State-global-let*
              • Last-prover-steps
              • @
              • Assign
              • Read-run-time
              • Canonical-pathname
              • F-put-global
              • Unsound-eval
              • Setenv$
              • Er-progn
              • Read-ACL2-oracle
              • With-live-state
              • F-get-global
              • Getenv$
              • Pprogn
              • Get-real-time
              • Makunbound-global
              • Get-cpu-time
              • F-boundp-global
              • Probe-file
            • W
            • Set-state-ok
            • Random$
          • Mutual-recursion
          • Memoize
          • Mbe
          • Io
          • Defpkg
          • Apply$
          • Loop$
          • Programming-with-state
            • Error-triple
            • Cbd
              • State-global-let*
              • Last-prover-steps
              • @
              • Assign
              • Read-run-time
              • Canonical-pathname
              • F-put-global
              • Unsound-eval
              • Setenv$
              • Er-progn
              • Read-ACL2-oracle
              • With-live-state
              • F-get-global
              • Getenv$
              • Pprogn
              • Get-real-time
              • Makunbound-global
              • Get-cpu-time
              • F-boundp-global
              • Probe-file
            • Arrays
            • Characters
            • Time$
            • Defmacro
            • Loop$-primer
            • Fast-alists
            • Defconst
            • Evaluation
            • Guard
            • Equality-variants
            • Compilation
            • Hons
            • ACL2-built-ins
            • Developers-guide
            • System-attachments
            • Advanced-features
            • Set-check-invariant-risk
            • Numbers
            • Efficiency
            • Irrelevant-formals
            • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
            • Redefining-programs
            • Lists
            • Invariant-risk
            • Errors
            • Defabbrev
            • Conses
            • Alists
            • Set-register-invariant-risk
            • Strings
            • Program-wrapper
            • Get-internal-time
            • Basics
            • Packages
            • Oracle-eval
            • Defmacro-untouchable
            • <<
            • Primitive
            • Revert-world
            • Unmemoize
            • Set-duplicate-keys-action
            • Symbols
            • Def-list-constructor
            • Easy-simplify-term
            • Defiteration
            • Fake-oracle-eval
            • Defopen
            • Sleep
          • Operational-semantics
          • Real
          • Start-here
          • Debugging
          • Miscellaneous
          • Output-controls
          • Macros
          • Interfacing-tools
        • Interfacing-tools
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Books-reference
      • Programming-with-state
      • ACL2-built-ins

      Cbd

      Connected book directory string

      Example:
      ACL2 !>:cbd
      "/usr/home/smith/"

      The connected book directory (``cbd'') is a string ending with the / character that specifies a directory as an absolute pathname. (See pathname for a discussion of file naming conventions.) When utilities that take a filename argument, such as include-book, are given a relative pathname, it is elaborated into an absolute pathname, essentially by appending the connected book directory string to the left and ".lisp" to the right. (This absolute pathname is actually canonical when elaborating book names. For more details on book names, see book-name and also see full-book-name.) Furthermore, include-book and ld temporarily set the connected book directory to the directory string of the resulting full pathname so that references to files in the same directory may omit the directory. See set-cbd for how to set the connected book directory string.

      Note that the cbd is used for elaborating every pathname argument, not just a pathname that represents a book. (Technical remark: Some utilities, such as open-input-channel, use the cbd indirectly as follows. That utility uses the Common Lisp utility, open, which knows nothing about the cbd. However, ACL2 arranges that the Lisp global *default-pathname-defaults* always has the cbd as its value, and Lisp uses that global to elaborate relative pathnames much as ACL2 uses the cbd.)

      General Form:
      (cbd)

      This is a macro that expands into a term involving the single free variable state. It returns the connected book directory string.

      For example, if the cbd is "/usr/home/smith/" then the book-name "project/task-1/arith" is elaborated using the cbd to the full-book-name "/usr/home/smith/project/task-1/arith.lisp", which is what include-book opens to read the source text for the book.

      The cbd may be changed using set-cbd.

      As noted above, during the processing of the events in a book, include-book sets the cbd to be the directory string of the full-book-name of the book; similarly for ld. Thus, if the cbd is "/usr/home/smith/" then during the processing of events by

      (include-book "project/task-1/arith")

      the cbd will be set to "/usr/home/smith/project/task-1/". Note that if "arith" recursively includes a sub-book, say "naturals", that resides on the same directory, the include-book event for it may omit the specification of that directory. For example, "arith" might contain the event

      (include-book "naturals").

      In general, suppose we have a superior book and several inferior books which are included by events in the superior book. Any inferior book residing on the same directory as the superior book may be referenced in the superior without specification of the directory.

      We call this a ``relative'' as opposed to ``absolute'' naming. The use of relative naming is preferred because it permits books (and their accompanying inferiors) to be moved between directories while maintaining their certificates and utility. Certified books that reference inferiors by absolute file names are unusable (and rendered uncertified) if the inferiors are moved to new directories.