• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
    • Io
    • Defttag
    • Sys-call
    • Save-exec
    • Quicklisp
    • Oslib
      • File-types
      • Get-decoded-time$
      • Argv
      • Copy
      • Catpath
      • Ls
      • Universal-time
      • Tempfile
      • Basename
      • Dirname
      • Copy!
      • Ls-files
      • Mkdir
      • Date
      • Rmtree
      • Lisp-version
      • Lisp-type
      • Ls-subdirs
      • Getpid
      • Dirnames
      • Basenames
      • Basename!
      • Ls-subdirs!
      • Ls-files!
      • Dirname!
      • Ls!
      • Catpaths
      • Mkdir!
      • Rmtree!
      • Remove-nonstrings
    • Std/io
    • Bridge
    • Clex
    • Tshell
    • Unsound-eval
    • Hacker
    • ACL2s-interface
    • Startup-banner
    • Command-line
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Oslib

Date

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

Signature

(date &optional (state 'state) &key (zone 'nil)) 
  → 
(mv datestamp state)

Returns

datestamp — Type (stringp datestamp).

state — Type (state-p1 state), given (force (state-p1 state)).

The datestamp string is constructed from the values returned by get-decoded-time$. Optionally, specify :zone t to include a time zone abbreviation in the datestamp. (The default is no time zone.)

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

Definitions and Theorems

Function: date-fn

(defun date-fn (state zone)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'date))
  (declare (ignorable __function__))
  (mv-let (second minute hour date month
                  year day daylight-p zone-code state)
          (get-decoded-time$ state)
   (declare (ignore day))
   (let
    ((month
          (nth (- month 1)
               '("January" "February" "March" "April"
                           "May" "June" "July" "August" "September"
                           "October" "November" "December")))
     (year (natstr (if (<= 0 year) year 0)))
     (date (natstr date))
     (hour (if (< hour 10)
               (cat "0" (natstr hour))
             (natstr hour)))
     (minute (if (< minute 10)
                 (cat "0" (natstr minute))
               (natstr minute)))
     (second (if (< second 10)
                 (cat "0" (natstr second))
               (natstr second))))
    (mv
     (cat
        month " " date
        ", " year " " hour ":" minute ":" second
        (if zone (cat " "
                      (time-zone-abbreviation zone-code daylight-p))
          ""))
     state)))))

Theorem: stringp-of-date.datestamp

(defthm stringp-of-date.datestamp
  (b* (((mv ?datestamp acl2::?state)
        (date-fn state zone)))
    (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 zone)))
             (state-p1 state)))
  :rule-classes :rewrite)