		Search-engine friendly clone of the ACL2 documentation.

Oslib

Rmtree

Recursively delete files, like the shell command rm -rf, and return a success indicator so you can recover from errors.

Signature
(rmtree dir &optional (state 'state)) → (mv successp state)
Arguments: dir — The path that you want to remove, 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 delete the requested path, and detect errors.

Definitions and Theorems

Function: rmtree-fn

(defun rmtree-fn (dir state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard (stringp dir)))
       (let ((__function__ 'rmtree))
            (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-rmtree.successp

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

Theorem: state-p1-of-rmtree.state

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