File-write-date$
The write-date of a file as a natural number
This analogue of the Common Lisp function, file-write-date,
uses that function under the hood to compute the write date D as a
natural number if the write date can be determined, returning (mv D
state); otherwise it returns (mv nil state). That number is, quoting
the Common Lisp HyperSpec, the number of seconds ``measured as an offset from
the beginning of the year 1900 (ignoring leap seconds)''. The guard
of file-write-date$ requires that the first argument is a string; the
second argument is the ACL2 state. The logical definition does not
actually look at the file and hence is not useful for reasoning about the
write date.
This utility provides a reasonable way to determine whether a file exists,
like Common Lisp's probe-file, according to whether D is
non-nil in when (mv D state) is returned.
Function: file-write-date$
(defun file-write-date$ (file state)
(declare (xargs :guard (stringp file)
:stobjs state)
(ignorable file))
(mv-let (erp val state)
(read-acl2-oracle state)
(mv (and (null erp) (posp val) val)
state)))
