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.
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)))
