		Search-engine friendly clone of the ACL2 documentation.

Copy

Copy-file

Copy a single file. (low level)

Signature
(copy-file from to &key (overwrite 'nil) (state 'state)) → (mv error state)
Arguments: from — Path to copy from, should be an ordinary file.
Guard (stringp from).; to — Path to copy to, should not be a directory.
Guard (stringp to).; overwrite — Should we overwrite to, if it exists?.
Guard (booleanp overwrite).
Returns: error — NIL on success, or an error msg on failure.; state — Type (state-p1 state), given (force (state-p1 state)).

This is a low level function for copying files. See copy for a higher-level alternative that can, e.g., copy directories.

In the logic this function reads from the ACL2 oracle. In the execution we use raw Lisp functions to attempt to copy the indicated file. This can fail for many reasons, e.g., from might not exist or we might not have permission to copy it.

Some typical examples of how to use this command correctly would be:

(copy-file "original.txt" "backup.txt")

(copy-file "/home/jared/original.txt"
           "/home/jared/my-backups/today/original.txt"
           :overwrite t)

The following example is not correct and will fail because the destination is a directory:

(copy-file "original.txt" "/home/jared/") ;; wrong, fails

Probably what was intended is instead:

(copy-file "original.txt"              ;; correct: specify full
           "/home/jared/original.txt") ;; destination path

Definitions and Theorems

Function: copy-file-fn

(defun copy-file-fn (from to overwrite state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (stringp from)
                              (stringp to)
                              (booleanp overwrite))))
  (declare (ignorable from to overwrite))
  (let ((__function__ 'copy-file))
    (declare (ignorable __function__))
    (b* ((- (raise "Raw Lisp definition not installed?"))
         ((mv ?err val state)
          (read-acl2-oracle state)))
      (mv val state))))

Theorem: state-p1-of-copy-file.state

(defthm state-p1-of-copy-file.state
  (implies (force (state-p1 state))
           (b* (((mv common-lisp::?error acl2::?state)
                 (copy-file-fn from to overwrite state)))
             (state-p1 state)))
  :rule-classes :rewrite)