• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Std/io
    • Oslib
      • File-types
      • Argv
      • Copy
        • Copy-file
      • Catpath
      • Ls
      • Universal-time
      • Tempfile
      • Basename
      • Dirname
      • Copy!
      • Ls-files
      • Mkdir
      • Rmtree
      • Lisp-version
      • Lisp-type
      • Ls-subdirs
      • Date
      • Getpid
      • Dirnames
      • Basenames
      • Basename!
      • Ls-subdirs!
      • Ls-files!
      • Dirname!
      • Ls!
      • Catpaths
      • Mkdir!
      • Rmtree!
      • Remove-nonstrings
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Oslib

Copy

Copy files or directories, with recoverable errors.

Signature

(copy from to &key (recursive 'nil) 
      (overwrite 'nil) 
      (limit '1000) 
      (state 'state)) 
 
  → 
(mv error 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

error — NIL on success, or an error msg on failure.

state — Type (state-p1 state), given (force (state-p1 state)).

This is a nice, higher-level wrapper around the low-level copy-file routine, which acts more like the unix cp shell command. It can (optionally) copy whole directories recursively, and more correctly handles copying individual files into an existing directory.

Copying files can fail for a variety of reasons. This function attempts to gracefully catch errors and return them in a form that you can recover from. See also copy!, an alternative that just causes a hard error if there is any problem.

Examples:

(oslib::copy "./hello.txt" "./hello-copy.txt")

copies hello.txt to hello-copy.txt

"safe", won't overwrite hello-copy.txt if it exists

(oslib::copy "./hello.txt" "./hello-copy.txt" :overwrite t)

copies hello.txt to hello-copy.txt

overwrites hello-copy.txt if it exists

won't overwrite directories, pipes, sockets, etc.

(oslib::copy "./hello.txt" "./foo/")

copies hello.txt to foo/hello.txt

won't overwrite foo/hello.txt if it exists

(oslib::copy "./foo/" "./bar/")

Recursively copy the directory foo to...

• If directory bar exists: bar/foo
• Otherwise, bar

Won't overwrite ./bar/foo if it already exists.

Won't overwrite ./bar if it is some non-directory file.

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 from-err from-kind state)
     (file-kind from))
    ((when from-err)
     (mv (msg "~s0: can't copy ~s1: ~@2" 'copy
              from from-err)
         state))
    ((unless from-kind)
     (mv (msg "~s0: no such file: ~s1" 'copy
              from)
         state))
    ((when (eq from-kind :regular-file))
     (nice-copy-single-file from to
                            :overwrite overwrite))
    ((when (eq from-kind :directory))
     (if
      (not recursive)
      (mv
       (msg "~s0: can't copy directory (in non-recursive mode): ~s1"
            'copy
            from)
       state)
      (nice-copy-single-directory from to
                                  :limit limit))))
   (mv (msg "~s0: unsupported file type ~s1: ~s2"
            'copy
            from-kind from)
       state))))

Theorem: state-p1-of-copy.state

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

Subtopics

Copy-file

Copy a single file. (low level)