diff --git a/Makefile b/Makefile index 48ee94e0df..7ac05e6f2b 100644 --- a/Makefile +++ b/Makefile @@ -59,12 +59,13 @@ export SCHEME .PHONY: all idris2-exec libdocs testenv testenv-clean support clean-support clean FORCE -all: support ${TARGET} libs +all: ${TARGET} libs idris2-exec: ${TARGET} -${TARGET}: src/IdrisPaths.idr +${TARGET}: support src/IdrisPaths.idr ${IDRIS2_BOOT} --build ${IDRIS2_APP_IPKG} + cp ${IDRIS2_CURDIR}/support/c/${IDRIS2_SUPPORT} ${TARGETDIR}/${NAME}_app/${IDRIS2_SUPPORT} # We use FORCE to always rebuild IdrisPath so that the git SHA1 info is always up to date src/IdrisPaths.idr: FORCE diff --git a/idris2api.ipkg b/idris2api.ipkg index 81fef80e68..1724a33733 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -192,6 +192,7 @@ modules = Libraries.System.File, Libraries.System.File.Buffer, + Libraries.System.File.Meta, Libraries.System.Directory.Tree, Libraries.Text.Bounded, diff --git a/libs/base/System/File/Meta.idr b/libs/base/System/File/Meta.idr index a9578bc6b5..063f63fe4d 100644 --- a/libs/base/System/File/Meta.idr +++ b/libs/base/System/File/Meta.idr @@ -1,12 +1,20 @@ ||| Functions for accessing file metadata. module System.File.Meta +import Data.String + +import System.FFI + import System.File.Handle import System.File.Support import public System.File.Types %default total +||| Pointer to a structure holding File's time attributes +FileTimePtr : Type +FileTimePtr = AnyPtr + %foreign supportC "idris2_fileSize" "node:lambda:fp=>require('fs').fstatSync(fp.fd).size" prim__fileSize : FilePtr -> PrimIO Int @@ -14,15 +22,33 @@ prim__fileSize : FilePtr -> PrimIO Int %foreign supportC "idris2_fileSize" prim__fPoll : FilePtr -> PrimIO Int -%foreign supportC "idris2_fileAccessTime" -prim__fileAccessTime : FilePtr -> PrimIO Int +%foreign supportC "idris2_fileTime" + "node:support:filetime,support_system_file" +prim__fileTime : FilePtr -> PrimIO FileTimePtr + +%foreign supportC "idris2_filetimeAccessTimeSec" + "node:lambda:ft=>ft.atime_sec" +prim__filetimeAccessTimeSec : FileTimePtr -> PrimIO Int + +%foreign supportC "idris2_filetimeAccessTimeNsec" + "node:lambda:ft=>ft.atime_nsec" +prim__filetimeAccessTimeNsec : FileTimePtr -> PrimIO Int + +%foreign supportC "idris2_filetimeModifiedTimeSec" + "node:lambda:ft=>ft.mtime_sec" +prim__filetimeModifiedTimeSec : FileTimePtr -> PrimIO Int -%foreign supportC "idris2_fileModifiedTime" - "node:lambda:fp=>require('fs').fstatSync(fp.fd).mtimeMs / 1000" -prim__fileModifiedTime : FilePtr -> PrimIO Int +%foreign supportC "idris2_filetimeModifiedTimeNsec" + "node:lambda:ft=>ft.mtime_nsec" +prim__filetimeModifiedTimeNsec : FileTimePtr -> PrimIO Int -%foreign supportC "idris2_fileStatusTime" -prim__fileStatusTime : FilePtr -> PrimIO Int +%foreign supportC "idris2_filetimeStatusTimeSec" + "node:lambda:ft=>ft.ctime_sec" +prim__filetimeStatusTimeSec : FileTimePtr -> PrimIO Int + +%foreign supportC "idris2_filetimeStatusTimeNsec" + "node:lambda:ft=>ft.ctime_nsec" +prim__filetimeStatusTimeNsec : FileTimePtr -> PrimIO Int %foreign supportC "idris2_fileIsTTY" "node:lambda:fp=>Number(require('tty').isatty(fp.fd))" @@ -43,32 +69,70 @@ firstExists : HasIO io => List String -> io (Maybe String) firstExists [] = pure Nothing firstExists (x :: xs) = if !(exists x) then pure (Just x) else firstExists xs +||| Record that holds timestamps with nanosecond precision +public export +record Timestamp where + constructor MkTimestamp + sec : Int + nsec : Int + +export +Eq Timestamp where + t == t' = (t.sec == t'.sec) && (t.nsec == t'.nsec) + +export +Ord Timestamp where + t < t' = (t.sec < t'.sec) || (t.sec == t'.sec && t.nsec < t'.nsec) + +export +Show Timestamp where + show t = "\{show t.sec}.\{padLeft 9 '0' $ show t.nsec}" + +||| Record that holds file's time attributes +public export +record FileTime where + constructor MkFileTime + atime : Timestamp + mtime : Timestamp + ctime : Timestamp + +||| Get File's time attributes +export +fileTime : HasIO io => (h : File) -> io (Either FileError FileTime) +fileTime (FHandle f) + = do res <- primIO (prim__fileTime f) + ft <- parseFileTime res + free res + if ft.atime.sec > 0 + then ok ft + else returnError + where + parseFileTime : FileTimePtr -> io FileTime + parseFileTime ft = pure $ MkFileTime { atime = MkTimestamp { sec = !(primIO (prim__filetimeAccessTimeSec ft)) + , nsec = !(primIO (prim__filetimeAccessTimeNsec ft)) + } + , mtime = MkTimestamp { sec = !(primIO (prim__filetimeModifiedTimeSec ft)) + , nsec = !(primIO (prim__filetimeModifiedTimeNsec ft)) + } + , ctime = MkTimestamp { sec = !(primIO (prim__filetimeStatusTimeSec ft)) + , nsec = !(primIO (prim__filetimeStatusTimeNsec ft)) + } + } + ||| Get the File's atime. export fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int) -fileAccessTime (FHandle f) - = do res <- primIO (prim__fileAccessTime f) - if res > 0 - then ok res - else returnError +fileAccessTime h = (fileTime h <&> (.atime.sec)) @{Compose} ||| Get the File's mtime. export fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int) -fileModifiedTime (FHandle f) - = do res <- primIO (prim__fileModifiedTime f) - if res > 0 - then ok res - else returnError +fileModifiedTime h = (fileTime h <&> (.mtime.sec)) @{Compose} ||| Get the File's ctime. export fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int) -fileStatusTime (FHandle f) - = do res <- primIO (prim__fileStatusTime f) - if res > 0 - then ok res - else returnError +fileStatusTime h = (fileTime h <&> (.ctime.sec)) @{Compose} ||| Get the File's size. export diff --git a/src/Core/Binary/Prims.idr b/src/Core/Binary/Prims.idr index 1be07ed533..adb22d210b 100644 --- a/src/Core/Binary/Prims.idr +++ b/src/Core/Binary/Prims.idr @@ -12,6 +12,7 @@ import Data.String import Data.Vect import Libraries.Data.PosMap +import public Libraries.System.File.Meta as L -- Remove after release 0.7.0 import public Libraries.Utils.Binary import public Libraries.Utils.String @@ -441,15 +442,15 @@ TTC Nat where ||| Get a file's modified time. If it doesn't exist, return 0 (UNIX Epoch) export -modTime : String -> Core Int +modTime : String -> Core L.Timestamp modTime fname = do Right f <- coreLift $ openFile fname Read - | Left err => pure 0 -- Beginning of Time :) - Right t <- coreLift $ fileModifiedTime f + | Left err => pure $ MkTimestamp 0 0 -- Beginning of Time :) + Right t <- coreLift $ L.fileTime f | Left err => do coreLift $ closeFile f - pure 0 + pure $ MkTimestamp 0 0 coreLift $ closeFile f - pure t + pure $ t.mtime export hashFileWith : Maybe String -> String -> Core (Maybe String) diff --git a/src/Libraries/System/File/Meta.idr b/src/Libraries/System/File/Meta.idr new file mode 100644 index 0000000000..a1fe07cdc3 --- /dev/null +++ b/src/Libraries/System/File/Meta.idr @@ -0,0 +1,110 @@ +module Libraries.System.File.Meta + +import Data.String + +import System.FFI + +import System.File.Handle +import System.File.Support +import public System.File.Types + +%default total + +||| Pointer to a structure holding File's time attributes +FileTimePtr : Type +FileTimePtr = AnyPtr + +%foreign supportC "idris2_fileTime" + "node:support:filetime,support_system_file" +prim__fileTime : FilePtr -> PrimIO FileTimePtr + +%foreign supportC "idris2_filetimeAccessTimeSec" + "node:lambda:ft=>ft.atime_sec" +prim__filetimeAccessTimeSec : FileTimePtr -> PrimIO Int + +%foreign supportC "idris2_filetimeAccessTimeNsec" + "node:lambda:ft=>ft.atime_nsec" +prim__filetimeAccessTimeNsec : FileTimePtr -> PrimIO Int + +%foreign supportC "idris2_filetimeModifiedTimeSec" + "node:lambda:ft=>ft.mtime_sec" +prim__filetimeModifiedTimeSec : FileTimePtr -> PrimIO Int + +%foreign supportC "idris2_filetimeModifiedTimeNsec" + "node:lambda:ft=>ft.mtime_nsec" +prim__filetimeModifiedTimeNsec : FileTimePtr -> PrimIO Int + +%foreign supportC "idris2_filetimeStatusTimeSec" + "node:lambda:ft=>ft.ctime_sec" +prim__filetimeStatusTimeSec : FileTimePtr -> PrimIO Int + +%foreign supportC "idris2_filetimeStatusTimeNsec" + "node:lambda:ft=>ft.ctime_nsec" +prim__filetimeStatusTimeNsec : FileTimePtr -> PrimIO Int + +||| Record that holds timestamps with nanosecond precision +public export +record Timestamp where + constructor MkTimestamp + sec : Int + nsec : Int + +export +Eq Timestamp where + t == t' = (t.sec == t'.sec) && (t.nsec == t'.nsec) + +export +Ord Timestamp where + t < t' = (t.sec < t'.sec) || (t.sec == t'.sec && t.nsec < t'.nsec) + +export +Show Timestamp where + show t = "\{show t.sec}.\{padLeft 9 '0' $ show t.nsec}" + +||| Record that holds file's time attributes +public export +record FileTime where + constructor MkFileTime + atime : Timestamp + mtime : Timestamp + ctime : Timestamp + +||| Get File's time attributes +export +fileTime : HasIO io => (h : File) -> io (Either FileError FileTime) +fileTime (FHandle f) + = do res <- primIO (prim__fileTime f) + ft <- parseFileTime res + free res + if ft.atime.sec > 0 + then ok ft + else returnError + where + parseFileTime : FileTimePtr -> io FileTime + parseFileTime ft = pure $ MkFileTime { atime = MkTimestamp { sec = !(primIO (prim__filetimeAccessTimeSec ft)) + , nsec = !(primIO (prim__filetimeAccessTimeNsec ft)) + } + , mtime = MkTimestamp { sec = !(primIO (prim__filetimeModifiedTimeSec ft)) + , nsec = !(primIO (prim__filetimeModifiedTimeNsec ft)) + } + , ctime = MkTimestamp { sec = !(primIO (prim__filetimeStatusTimeSec ft)) + , nsec = !(primIO (prim__filetimeStatusTimeNsec ft)) + } + } + +||| Get the File's atime. +export +fileAccessTime : HasIO io => (h : File) -> io (Either FileError Int) +fileAccessTime h = (fileTime h <&> (.atime.sec)) @{Compose} + +||| Get the File's mtime. +export +fileModifiedTime : HasIO io => (h : File) -> io (Either FileError Int) +fileModifiedTime h = (fileTime h <&> (.mtime.sec)) @{Compose} + +||| Get the File's ctime. +export +fileStatusTime : HasIO io => (h : File) -> io (Either FileError Int) +fileStatusTime h = (fileTime h <&> (.ctime.sec)) @{Compose} + + diff --git a/support/c/idris_file.c b/support/c/idris_file.c index 7fe3ef6812..5817f619e7 100644 --- a/support/c/idris_file.c +++ b/support/c/idris_file.c @@ -177,15 +177,55 @@ size_t idris2_writeBufferData(FILE *h, const char *buffer, size_t loc, int idris2_eof(FILE *f) { return feof(f); } -int idris2_fileAccessTime(FILE *f) { +struct filetime { + int atime_sec; + int atime_nsec; + int mtime_sec; + int mtime_nsec; + int ctime_sec; + int ctime_nsec; +}; + +struct filetime *idris2_fileTime(FILE *f) { + struct filetime *ft = malloc(sizeof(*ft)); + +#ifdef _WIN32 + if (win32_getFileTime(f, &ft->atime_sec, &ft->atime_nsec, &ft->mtime_sec, + &ft->mtime_nsec, &ft->ctime_sec, &ft->ctime_nsec)) { + ft->atime_sec = -1; + return ft; + } + + return ft; +#else int fd = idris2_getFileNo(f); struct stat buf; - if (fstat(fd, &buf) == 0) { - return buf.st_atime; - } else { - return -1; + if (fstat(fd, &buf)) { + ft->atime_sec = -1; + return ft; } + + ft->atime_sec = buf.st_atime; + ft->mtime_sec = buf.st_mtime; + ft->ctime_sec = buf.st_ctime; + +#if defined(__MACH__) || defined(__APPLE__) + ft->atime_nsec = buf.st_atimespec.tv_nsec; + ft->mtime_nsec = buf.st_mtimespec.tv_nsec; + ft->ctime_nsec = buf.st_ctimespec.tv_nsec; +#elif (_POSIX_VERSION >= 200809L) || defined(__FreeBSD__) + ft->atime_nsec = buf.st_atim.tv_nsec; + ft->mtime_nsec = buf.st_mtim.tv_nsec; + ft->ctime_nsec = buf.st_ctim.tv_nsec; +#else + ft->atime_nsec = 0; + ft->mtime_nsec = 0; + ft->ctime_nsec = 0; +#endif + + return ft; +#endif } int idris2_fileModifiedTime(FILE *f) { @@ -199,15 +239,24 @@ int idris2_fileModifiedTime(FILE *f) { } } -int idris2_fileStatusTime(FILE *f) { - int fd = idris2_getFileNo(f); +int idris2_filetimeAccessTimeSec(struct filetime *ft) { return ft->atime_sec; } - struct stat buf; - if (fstat(fd, &buf) == 0) { - return buf.st_ctime; - } else { - return -1; - } +int idris2_filetimeAccessTimeNsec(struct filetime *ft) { + return ft->atime_nsec; +} + +int idris2_filetimeModifiedTimeSec(struct filetime *ft) { + return ft->mtime_sec; +} + +int idris2_filetimeModifiedTimeNsec(struct filetime *ft) { + return ft->mtime_nsec; +} + +int idris2_filetimeStatusTimeSec(struct filetime *ft) { return ft->ctime_sec; } + +int idris2_filetimeStatusTimeNsec(struct filetime *ft) { + return ft->ctime_nsec; } int idris2_fileIsTTY(FILE *f) { diff --git a/support/c/idris_file.h b/support/c/idris_file.h index e3b1eed17a..2e9e4d70fd 100644 --- a/support/c/idris_file.h +++ b/support/c/idris_file.h @@ -39,10 +39,18 @@ size_t idris2_writeBufferData(FILE *h, const char *buffer, size_t loc, size_t len); int idris2_eof(FILE *f); -int idris2_fileAccessTime(FILE *f); + +struct filetime; + +struct filetime *idris2_fileTime(FILE *f); int idris2_fileModifiedTime(FILE *f); -int idris2_fileStatusTime(FILE *f); -int idris2_fileIsTTY(FILE *f); + +int idris2_filetimeAccessTimeSec(struct filetime *f); +int idris2_filetimeAccessTimeNsec(struct filetime *f); +int idris2_filetimeModifiedTimeSec(struct filetime *f); +int idris2_filetimeModifiedTimeNsec(struct filetime *f); +int idris2_filetimeStatusTimeSec(struct filetime *f); +int idris2_filetimeStatusTimeNsec(struct filetime *f); FILE *idris2_stdin(); FILE *idris2_stdout(); diff --git a/support/c/windows/win_utils.c b/support/c/windows/win_utils.c index ceffc8e30e..d5e9ad85df 100644 --- a/support/c/windows/win_utils.c +++ b/support/c/windows/win_utils.c @@ -165,4 +165,41 @@ long win32_getNProcessors() { int win32_getFileNo(FILE *f) { return _fileno(f); } +int win32_getFileTime(FILE *f, int *atime_sec, int *atime_nsec, int *mtime_sec, + int *mtime_nsec, int *ctime_sec, int *ctime_nsec) { + HANDLE wh = (HANDLE)_get_osfhandle(_fileno(f)); + if (wh == INVALID_HANDLE_VALUE) { + return -1; + } + + FILETIME atime, mtime, ctime; + + if (GetFileTime(wh, &ctime, &atime, &mtime)) { + ULARGE_INTEGER at, mt, ct; + + at.HighPart = atime.dwHighDateTime; + at.LowPart = atime.dwLowDateTime; + mt.HighPart = mtime.dwHighDateTime; + mt.LowPart = mtime.dwLowDateTime; + ct.HighPart = ctime.dwHighDateTime; + ct.LowPart = ctime.dwLowDateTime; + + *atime_sec = at.QuadPart / 10000000; + *atime_sec -= 11644473600; + *atime_nsec = (at.QuadPart % 10000000) * 100; + + *mtime_sec = mt.QuadPart / 10000000; + *mtime_sec -= 11644473600; + *mtime_nsec = (mt.QuadPart % 10000000) * 100; + + *ctime_sec = ct.QuadPart / 10000000; + *ctime_sec -= 11644473600; + *ctime_nsec = (ct.QuadPart % 10000000) * 100; + + return 0; + } else { + return -1; + } +} + int win32_isTTY(int fd) { return _isatty(fd); } diff --git a/support/c/windows/win_utils.h b/support/c/windows/win_utils.h index c84066f3b4..b2074e1624 100644 --- a/support/c/windows/win_utils.h +++ b/support/c/windows/win_utils.h @@ -16,4 +16,6 @@ int win32_getPID(); long win32_getNProcessors(); int win32_getFileNo(FILE *); +int win32_getFileTime(FILE *f, int *atime_sec, int *atime_nsec, int *mtime_sec, + int *mtime_nsec, int *ctime_sec, int *ctime_nsec); int win32_isTTY(int fd); diff --git a/support/js/support_system_file.js b/support/js/support_system_file.js index 9118cb4413..0436959667 100644 --- a/support/js/support_system_file.js +++ b/support/js/support_system_file.js @@ -167,3 +167,17 @@ function support_system_file_pclose (file_ptr) { support_system_file_removeFile(name) return exit_code } + +function support_system_file_filetime(file_ptr) { + const {fd, name, exit_code} = file_ptr + const st = support_system_file_fs.fstatSync(fd) + const ft = { + atime_sec : _truncInt32(Math.trunc(st.atimeMs / 1000)), + atime_nsec : st.atimeMs * 1000000 % 1000000000, + mtime_sec : _truncInt32(Math.trunc(st.mtimeMs / 1000)), + mtime_nsec : st.mtimeMs * 1000000 % 1000000000, + ctime_sec : _truncInt32(Math.trunc(st.ctimeMs / 1000)), + ctime_nsec : st.mtimeMs * 1000000 % 1000000000 + }; + return ft +} diff --git a/tests/Main.idr b/tests/Main.idr index 078ca1a0ef..10fa4f05ab 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -43,6 +43,7 @@ idrisTestsBasic = MkTestPool "Fundamental language features" [] Nothing "basic056", "basic057", "basic058", "basic059", "basic060", "basic061", "basic062", "basic063", "basic064", "basic065", "basic066", "basic067", "basic068", "basic069", "basic070", + "basic071", "idiom001", "literals001", "dotted001", diff --git a/tests/idris2/basic071/A.idr b/tests/idris2/basic071/A.idr new file mode 100644 index 0000000000..8e84a04337 --- /dev/null +++ b/tests/idris2/basic071/A.idr @@ -0,0 +1,5 @@ +module A + +export +x : Nat +x = 5 diff --git a/tests/idris2/basic071/B.idr b/tests/idris2/basic071/B.idr new file mode 100644 index 0000000000..61b75f7109 --- /dev/null +++ b/tests/idris2/basic071/B.idr @@ -0,0 +1,6 @@ +module B + +import A + +y : Nat +y = x diff --git a/tests/idris2/basic071/expected b/tests/idris2/basic071/expected new file mode 100644 index 0000000000..42c8107f4f --- /dev/null +++ b/tests/idris2/basic071/expected @@ -0,0 +1,3 @@ +1/2: Building A (A.idr) +2/2: Building B (B.idr) +-- this should be the last line of output -- diff --git a/tests/idris2/basic071/run b/tests/idris2/basic071/run new file mode 100755 index 0000000000..d2f5648f3f --- /dev/null +++ b/tests/idris2/basic071/run @@ -0,0 +1,16 @@ +rm -rf build +$1 --no-color --console-width 0 --no-banner --check B.idr + +# Set very close time for A and B TTC files +touch A.idr +sync A.idr +touch B.idr +sync B.idr +touch build/ttc/*/A.tt* +sync build/ttc/*/A.tt* +touch build/ttc/*/B.tt* +sync build/ttc/*/B.tt* + +echo "-- this should be the last line of output --" + +$1 --no-color --console-width 0 --no-banner --check B.idr