		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)