		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)