		Search-engine friendly clone of the ACL2 documentation.

Oslib

Copy!

Copy files or directories, or cause a hard error.

Signature
(copy! from to &key (recursive 'nil) (overwrite 'nil) (limit '1000) (state 'state)) → state
Arguments: from — Path to copy from (ordinary file or directory).
Guard (stringp from).; to — Path to copy to (ordinary file or directory).
Guard (stringp to).; recursive — Allow copying directories like cp -r?.
Guard (booleanp recursive).; overwrite — Should we overwrite files/directories that already exist? Only matters when copying individual files, not directories.
Guard (booleanp overwrite).; limit — Directly depth recursion limit (in case of symlink loops). Only matters when copying directories, not files.
Guard (natp limit).
Returns: state — Type (state-p1 state), given (force (state-p1 state)).

This is identical to copy except that we raise a hard error if anything goes wrong.

Definitions and Theorems

Function: copy!-fn

(defun copy!-fn
       (from to recursive overwrite limit state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard (and (stringp from)
                                   (stringp to)
                                   (booleanp recursive)
                                   (booleanp overwrite)
                                   (natp limit))))
       (let ((__function__ 'copy!))
            (declare (ignorable __function__))
            (b* (((mv err state)
                  (copy from to
                        :recursive recursive
                        :overwrite overwrite
                        :limit limit))
                 ((when err) (raise "~@0" err) state))
                state)))

Theorem: state-p1-of-copy!

(defthm
    state-p1-of-copy!
    (implies
         (force (state-p1 state))
         (b* ((state (copy!-fn from
                               to recursive overwrite limit state)))
             (state-p1 state)))
    :rule-classes :rewrite)