diff --git a/libs/base/System/File.idr b/libs/base/System/File.idr index 8359de4768..e1200e91fb 100644 --- a/libs/base/System/File.idr +++ b/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) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index 5d9d16fddf..c1e6da4831 100644 --- a/src/Idris/Package.idr +++ b/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,7 +374,7 @@ 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 ] @@ -381,7 +382,7 @@ installFrom builddir destdir ns -- 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 ] diff --git a/tests/base/system_file_copyFile/CopyFile.idr b/tests/base/system_file_copyFile/CopyFile.idr new file mode 100644 index 0000000000..56ed1b6eb7 --- /dev/null +++ b/tests/base/system_file_copyFile/CopyFile.idr @@ -0,0 +1,4 @@ +import System.File + +main : IO () +main = copyFile "source.bin" "dest.bin" diff --git a/tests/base/system_file_copyFile/expected b/tests/base/system_file_copyFile/expected new file mode 100644 index 0000000000..efd35673a0 --- /dev/null +++ b/tests/base/system_file_copyFile/expected @@ -0,0 +1 @@ +AQIDBA== diff --git a/tests/base/system_file_copyFile/input b/tests/base/system_file_copyFile/input new file mode 100644 index 0000000000..fc5992c298 --- /dev/null +++ b/tests/base/system_file_copyFile/input @@ -0,0 +1,2 @@ +:exec main +:q diff --git a/tests/base/system_file_copyFile/run b/tests/base/system_file_copyFile/run new file mode 100644 index 0000000000..21c35763c3 --- /dev/null +++ b/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 diff --git a/tests/base/system_file_copyFile/source.bin b/tests/base/system_file_copyFile/source.bin new file mode 100644 index 0000000000..82090ee2cb --- /dev/null +++ b/tests/base/system_file_copyFile/source.bin @@ -0,0 +1 @@ + \ No newline at end of file