		Search-engine friendly clone of the ACL2 documentation.

Oslib

Mkdir

Make new directories if they don't already exist, like mkdir -p, and return a success indicator so you can recover from errors.

Signature
(mkdir dir &optional (state 'state)) → (mv successp state)
Arguments: dir — The path that you want to create, e.g., ./foo/bar.
Guard (stringp dir).
Returns: successp — Success indicator. We might fail due to file system permissions, illegal file names, etc.
Type (booleanp successp).; state — Type (state-p1 state), given (force (state-p1 state)).

In the logic this function reads from the ACL2 oracle to determine if it succeeds. In the execution, we attempt to create directories using the Common Lisp function ensure-directories-exist, and capture any errors.

Definitions and Theorems

Function: mkdir-fn

(defun mkdir-fn (dir state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard (stringp dir)))
       (let ((__function__ 'mkdir))
            (declare (ignorable __function__))
            (b* ((- (raise "Raw Lisp definition not installed?"))
                 ((mv err val state)
                  (read-acl2-oracle state))
                 (okp (and (not err) (booleanp val) val)))
                (mv okp state))))

Theorem: booleanp-of-mkdir.successp

(defthm booleanp-of-mkdir.successp
        (b* (((mv ?successp acl2::?state)
              (mkdir-fn dir state)))
            (booleanp successp))
        :rule-classes :type-prescription)

Theorem: state-p1-of-mkdir.state

(defthm state-p1-of-mkdir.state
        (implies (force (state-p1 state))
                 (b* (((mv ?successp acl2::?state)
                       (mkdir-fn dir state)))
                     (state-p1 state)))
        :rule-classes :rewrite)