		Search-engine friendly clone of the ACL2 documentation.

Oslib

Date

Get the current datestamp, like "November 17, 2010 10:25:33".

Signature
(date &optional (state 'state)) → (mv datestamp state)
Returns: datestamp — Type (stringp datestamp).; state — Type (state-p1 state), given (force (state-p1 state)).

In the logic this function reads from the ACL2 oracle. In the execution we use Common Lisp's get-decoded-time function to figure out what the current date and time is. We think this should work on any Common Lisp system.

See also universal-time, which returns an integer representation of the current time.

Definitions and Theorems

Function: date-fn

(defun date-fn (state)
       (declare (xargs :stobjs (state)))
       (declare (xargs :guard t))
       (let ((__function__ 'date))
            (declare (ignorable __function__))
            (b* ((- (raise "Raw Lisp definition not installed?"))
                 ((mv err val state)
                  (read-acl2-oracle state)))
                (if (and (not err) (stringp val))
                    (mv val state)
                    (mv "Error reading date." state)))))

Theorem: stringp-of-date.datestamp

(defthm stringp-of-date.datestamp
        (b* (((mv ?datestamp acl2::?state)
              (date-fn state)))
            (stringp datestamp))
        :rule-classes :type-prescription)

Theorem: state-p1-of-date.state

(defthm state-p1-of-date.state
        (implies (force (state-p1 state))
                 (b* (((mv ?datestamp acl2::?state)
                       (date-fn state)))
                     (state-p1 state)))
        :rule-classes :rewrite)