		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)