		Search-engine friendly clone of the ACL2 documentation.

Oslib

Universal-time

Get the current timestamp as a natural number, specifically the number of seconds since 00:00 January 1, 1900 GMT. Note well that this is not the Unix epoch.

Signature
(universal-time &optional (state 'state)) → (mv seconds state)
Returns: seconds — Type (natp seconds).; state — Type (state-p1 state), given (force (state-p1 state)).

In the logic this function reads from the ACL2 oracle, so there is no logical guarantee that it will return successive times. (Indeed, the user could likely change their computer's clock so that it would report earlier times.)

In the execution, we use Common Lisp's get-universal-time function to figure out the current time in seconds since the start of 1900.

This is, for whatever reason, a different starting date than the Unix epoch (which records time since the start of 1970). You should therefore be careful if you need to compare this timestamp against those produced by external tools.

Definitions and Theorems

Function: universal-time-fn

(defun universal-time-fn (state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'universal-time))
    (declare (ignorable __function__))
    (b* ((- (raise "Raw Lisp definition not installed?"))
         ((mv err val state)
          (read-acl2-oracle state)))
      (if (and (not err) (natp val))
          (mv val state)
        (mv 0 state)))))

Theorem: natp-of-universal-time.seconds

(defthm natp-of-universal-time.seconds
  (b* (((mv ?seconds acl2::?state)
        (universal-time-fn state)))
    (natp seconds))
  :rule-classes :type-prescription)

Theorem: state-p1-of-universal-time.state

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