		Search-engine friendly clone of the ACL2 documentation.

Oslib

Lisp-version

Get a host-Lisp specific string describing the version number for this Common Lisp implementation.

Signature
(lisp-version &optional (state 'state)) → (mv description state)
Returns: description — E.g., "Version 1.9-r15996 (LinuxX8664)".
Type (stringp description).; state — Type (state-p1 state), given (force (state-p1 state)).

In the logic this function reads from the ACL2 oracle. In the execution, we call the Common Lisp function lisp-implementation-version, and return the string it produces.

Note that the Common Lisp lisp-implementation-type function is technically allowed to return nil; in this case we return the empty string.

Definitions and Theorems

Function: lisp-version-fn

(defun lisp-version-fn (state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard t))
  (let ((__function__ 'lisp-version))
    (declare (ignorable __function__))
    (b* (((mv err val state)
          (read-acl2-oracle state))
         (description (if (and (not err) (stringp val))
                          val
                        "")))
      (mv description state))))

Theorem: stringp-of-lisp-version.description

(defthm stringp-of-lisp-version.description
  (b* (((mv ?description acl2::?state)
        (lisp-version-fn state)))
    (stringp description))
  :rule-classes :type-prescription)

Theorem: state-p1-of-lisp-version.state

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