4.5.1 Unix and Mac OS Paths🔗ℹ

A path on Unix or Mac OS is natively a byte string. For presentation to users and for other string-based operations, a path is converted to/from a string using the current locale’s encoding with ? (encoding) or Char"\uFFFD" (decoding) in place of errors. Beware that the encoding may not accommodate all possible paths as distinct strings.

A / separates elements of a Unix or Mac OS path, . as a path element always means the directory indicated by preceding path, and .. as a path element always means the parent of the directory indicated by the preceding path. A leading ~ in a path is not treated specially, but filesystem.expand_user_path can be used to convert a leading ~ element to a user-specific directory. No other character or byte has a special meaning within a path. Multiple adjacent / are equivalent to a single / (i.e., they act as a single path separator).

A path root is always /. A path starting with / is an absolute, complete path, and a path starting with any other character is a relative path.

Any pathname that ends with a / syntactically refers to a directory, as does any path whose last element is . or ...

A Unix or Mac OS path is cleansed by replacing multiple adjacent /s with a single /.

For the Path.Element constructor, the given byte string must not contain any /, otherwise the Exn.Fail.Annot exception is thrown. The result of Path.Element.bytes or Path.Element.string is always the same as the result of Path.bytes and Path.string. Since that is not the case for other platforms, however, Path.Element.bytes and Path.Element.string should be used when converting individual path elements.