• 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
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
        • Io
          • Fmt
          • Msg
          • Cw
          • Set-evisc-tuple
          • Set-iprint
          • Print-control
          • Read-file-into-string
          • Std/io
          • Msgp
          • Printing-to-strings
          • Evisc-tuple
          • Output-controls
          • Observation
          • *standard-co*
          • Ppr-special-syms
          • Standard-oi
          • Standard-co
          • Without-evisc
          • Serialize
          • Output-to-file
          • Fmt-to-comment-window
          • Princ$
          • Character-encoding
          • Open-output-channel!
          • Cw-print-base-radix
          • Set-print-case
          • Set-print-base
          • Print-object$
          • Extend-pathname
            • Print-object$+
            • Fmx-cw
            • Set-print-radix
            • Set-fmt-hard-right-margin
            • File-write-date$
            • Proofs-co
            • Set-print-base-radix
            • Print-base-p
            • *standard-oi*
            • Wof
            • File-length$
            • Fms!-lst
            • Delete-file$
            • *standard-ci*
            • Write-list
            • Trace-co
            • Fmt!
            • Fms
            • Cw!
            • Fmt-to-comment-window!
            • Fms!
            • Eviscerate-hide-terms
            • Fmt1!
            • Fmt-to-comment-window!+
            • Read-file-into-byte-array-stobj
            • Fmt1
            • Fmt-to-comment-window+
            • Cw-print-base-radix!
            • Read-file-into-character-array-stobj
            • Fmx
            • Cw!+
            • Read-objects-from-book
            • Newline
            • Cw+
            • Probe-file
            • Write-objects-to-file!
            • Write-objects-to-file
            • Read-objects-from-file
            • Read-object-from-file
            • Read-file-into-byte-list
            • Set-fmt-soft-right-margin
            • Read-file-into-character-list
            • Io-utilities
          • Defttag
          • Sys-call
          • Save-exec
          • Quicklisp
          • Std/io
          • Oslib
          • Bridge
          • Clex
          • Tshell
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
      • Interfacing-tools
        • Io
          • Fmt
          • Msg
          • Cw
          • Set-evisc-tuple
          • Set-iprint
          • Print-control
          • Read-file-into-string
          • Std/io
          • Msgp
          • Printing-to-strings
          • Evisc-tuple
          • Output-controls
          • Observation
          • *standard-co*
          • Ppr-special-syms
          • Standard-oi
          • Standard-co
          • Without-evisc
          • Serialize
          • Output-to-file
          • Fmt-to-comment-window
          • Princ$
          • Character-encoding
          • Open-output-channel!
          • Cw-print-base-radix
          • Set-print-case
          • Set-print-base
          • Print-object$
          • Extend-pathname
            • Print-object$+
            • Fmx-cw
            • Set-print-radix
            • Set-fmt-hard-right-margin
            • File-write-date$
            • Proofs-co
            • Set-print-base-radix
            • Print-base-p
            • *standard-oi*
            • Wof
            • File-length$
            • Fms!-lst
            • Delete-file$
            • *standard-ci*
            • Write-list
            • Trace-co
            • Fmt!
            • Fms
            • Cw!
            • Fmt-to-comment-window!
            • Fms!
            • Eviscerate-hide-terms
            • Fmt1!
            • Fmt-to-comment-window!+
            • Read-file-into-byte-array-stobj
            • Fmt1
            • Fmt-to-comment-window+
            • Cw-print-base-radix!
            • Read-file-into-character-array-stobj
            • Fmx
            • Cw!+
            • Read-objects-from-book
            • Newline
            • Cw+
            • Probe-file
            • Write-objects-to-file!
            • Write-objects-to-file
            • Read-objects-from-file
            • Read-object-from-file
            • Read-file-into-byte-list
            • Set-fmt-soft-right-margin
            • Read-file-into-character-list
            • Io-utilities
          • Defttag
          • Sys-call
          • Save-exec
          • Quicklisp
          • Std/io
          • Oslib
          • Bridge
          • Clex
          • Tshell
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Io
      • ACL2-built-ins

      Extend-pathname

      Extend a relative pathname to an absolute pathname

      Extend-pathname is a :program mode function that takes a directory name as specified below and a filename (a string), and returns a corresponding pathname for the given file that is relative to the specified directory. If the filename is already an absolute pathname then the return value is that filename, unchanged.

      General Form:
      
      (extend-pathname dir filename state)

      where dir is either a string, representing an absolute pathname for a directory, or a keyword, representing a project directory (see project-dir-alist); filename is a string representing a relative or absolute pathname; and state is the ACL2 state.

      The following examples illustrate the behavior of extend-pathname.

      Examples (comments added)
      
      ACL2 !>(extend-pathname "~/temp" "foo.lisp" state)
      ; where the user is "bubba" here and in the remaining examples
      "/home/bubba/temp/foo.lisp"
      ACL2 !>(extend-pathname "~/temp/" "foo.lisp" state)
      ; the final / is optional for the directory name
      "/home/bubba/temp/foo.lisp"
      ACL2 !>(extend-pathname "~/temp/" "no-such-file" state)
      ; name of non-existent file is still extended
      "/home/bubba/temp/no-such-file"
      ACL2 !>(extend-pathname "." "no-such-file" state)
      ; THIS IS NOT SUPPORTED, because the first argument is a relative pathname,
      ; not an absolute pathname; but in this case a reasonable answer happens to
      ; be provided.  See the next example for how to do this properly.
      ; Here we assume that the current working directory is "/home/joe"
      "/home/joe/no-such-file"
      ACL2 !>(extend-pathname (canonical-pathname "." t state) "no-such-file" state)
      ; As above, but the first argument is first turned into an absolute pathname,
      ; which makes the call a supported one.
      "/home/joe/no-such-file"
      ACL2 !>(extend-pathname (cbd) "no-such-file" state)
      ; assumes that the connected book directory (see :DOC cbd) is "/data/santa"
      "/data/santa/no-such-file"
      ACL2 !>(extend-pathname :system "no-such-file" state)
      ; assumes that system books directory is "/data/acl2/books"
      "/data/acl2/books/no-such-file"
      ACL2 !>(extend-pathname "/data/acl2" "~/temp/foo.lisp" state)
      ; directory is ignored when filename is already absolute
      "/home/bubba/temp/foo.lisp"
      ACL2 !>(extend-pathname :system "~/temp/foo.lisp" state)
      ; directory is ignored when filename is already absolute
      "/home/bubba/temp/foo.lisp"

      Note that when the indicated file exists, extend-pathname resolves symbolic links by using canonical-pathname. If you don't want symbolic links to be resolved there are simpler alternatives; for example, see oslib::catpath.