• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
      • Fmt
      • Msg
      • Cw
      • Set-evisc-tuple
      • Set-iprint
      • Print-control
      • Read-file-into-string
      • Msgp
      • Std/io
      • Printing-to-strings
      • Evisc-tuple
      • Output-controls
      • Observation
      • *standard-co*
      • Pp-special-syms
      • Standard-oi
      • Without-evisc
      • Standard-co
      • Serialize
      • Output-to-file
      • Fmt-to-comment-window
      • Character-encoding
      • Princ$
      • Open-output-channel!
      • Cw-print-base-radix
      • Set-print-case
      • Set-print-base
      • Print-object$
      • Fmx-cw
      • Print-object$+
      • Set-print-radix
      • Extend-pathname
      • Set-fmt-hard-right-margin
      • Proofs-co
      • File-write-date$
      • Set-print-base-radix
      • Print-base-p
      • *standard-oi*
      • Wof
      • File-length$
      • Fms!-lst
      • *standard-ci*
      • Write-list
      • Fmt!
      • Fms
      • Delete-file$
      • 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
      • Cw!+
      • Newline
      • Fmx
      • Cw+
      • Read-object-from-file
      • Set-fmt-soft-right-margin
      • Read-objects-from-file
      • Read-file-into-byte-list
      • Read-file-into-character-list
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
    • Std/io
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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 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 non-empty string, representing a directory's pathname, 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 flesh out 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)
; assumes that the current working directory is "/home/joe"
"/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.