Add System.File.copyFile

libs/base/System/File.idr

@@ -1,5 +1,7 @@
 module System.File
 
+import Data.Buffer
+
 import public System.File.Buffer
 import public System.File.Error
 import public System.File.Handle
@@ -10,3 +12,10 @@ import public System.File.Process
 import public System.File.ReadWrite
 import public System.File.Types
 import public System.File.Virtual
+
+export
+copyFile : String -> String -> IO (Either FileError ())
+copyFile src dest
+    = do Right buf <- createBufferFromFile src
+             | Left err => pure (Left err)
+         writeBufferToFile dest buf !(rawSize buf)

src/Idris/Package.idr

@@ -336,6 +336,7 @@ build pkg opts
          runScript (postbuild pkg)
          pure []
 
+-- This function is deprecated; to be removed after the next version bump
 copyFile : String -> String -> IO (Either FileError ())
 copyFile src dest
     = do Right buf <- readFromFile src
@@ -373,15 +374,15 @@ installFrom builddir destdir ns
                              [ "Can't make directories " ++ show modPath
                              , show err ]
          coreLift $ putStrLn $ "Installing " ++ ttcPath ++ " to " ++ destPath
-         Right _ <- coreLift $ copyFile ttcPath destFile
+         Right _ <- coreLift $ Package.copyFile ttcPath destFile
              | Left err => throw $ InternalError $ unlines
                              [ "Can't copy file " ++ ttcPath ++ " to " ++ destPath
                              , show err ]
          -- Copy object files, if any. They don't necessarily get created,
          -- since some modules don't generate any code themselves.
          traverse_ (\ (obj, dest) =>
                       do coreLift $ putStrLn $ "Installing " ++ obj ++ " to " ++ destPath
-                         ignore $ coreLift $ copyFile obj dest)
+                         ignore $ coreLift $ Package.copyFile obj dest)
                    objPaths
 
          pure ()
@@ -414,7 +415,7 @@ installSrcFrom wdir destdir (ns, srcRelPath)
              (MkPermissions [Read, Write] [Read, Write] [Read, Write])
              | Left err => throw $ UserError (show err)
            pure ()
-         Right _ <- coreLift $ copyFile srcPath destFile
+         Right _ <- coreLift $ Package.copyFile srcPath destFile
              | Left err => throw $ InternalError $ unlines
                              [ "Can't copy file " ++ srcPath ++ " to " ++ destPath
                              , show err ]

tests/base/system_file_copyFile/CopyFile.idr

@@ -0,0 +1,4 @@
+import System.File
+
+main : IO ()
+main = copyFile "source.bin" "dest.bin"

tests/base/system_file_copyFile/expected

@@ -0,0 +1 @@
+AQIDBA==

tests/base/system_file_copyFile/input

@@ -0,0 +1,2 @@
+:exec main
+:q

tests/base/system_file_copyFile/run

@@ -0,0 +1,6 @@
+rm -rf build
+
+$1 --no-color --console-width 0 --no-banner CopyFile.idr < input
+base64 dest.bin
+
+rm dest.bin

tests/base/system_file_copyFile/source.bin

@@ -0,0 +1 @@
+