		Search-engine friendly clone of the ACL2 documentation.

Oslib

Mkdir!

Make new directories if they don't already exist, like mkdir -p, or cause a hard error if there is any problem.

Signature
(mkdir! dir &optional (state 'state)) → state
Arguments: dir — The path that you want to create, e.g., ./foo/bar.
Guard (stringp dir).
Returns: state — Type (state-p1 state), given (force (state-p1 state)).

This is just a wrapper for mkdir that causes an error on any failure.

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* (((mv successp state) (mkdir dir state))
         ((unless successp)
          (raise "Failed to create ~s0." dir)
          state))
      state)))

Theorem: state-p1-of-mkdir!

(defthm state-p1-of-mkdir!
  (implies (force (state-p1 state))
           (b* ((state (mkdir!-fn dir state)))
             (state-p1 state)))
  :rule-classes :rewrite)