		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)