Set an environment variable
(Setenv$ str val), where str and val are strings,
sets the environment variable str to have value val, for subsequent
read by getenv$ (see getenv$), and returns nil. Or, if this
operation is not implemented for the host Common Lisp, an error will
(setenv$ "FOO" "BAR")
It may be surprising that setenv$ returns nil; indeed, it neither
takes nor returns the ACL2 state. The reason is that getenv$
takes responsibility for trafficking in state; it is defined in the
logic using the function read-ACL2-oracle, which (again, in the logic)
does modify state, by popping an entry from its acl2-oracle field. See getenv$.
As suggested above, a call of getenv$ takes into account the most
recent call of setenv$ on the same environment variable. It may also be
the case that setenv$ modifies the environment of the underlying process;
for example, we think this is probably the case for most invocations of ACL2
built on a host Lisp that is CCL, SBCL, or CMUCL, as well as others perhaps.
If you want to rely on such behavior, however, we advise you to look at source
(defun setenv$ (str val)
(declare (xargs :guard (and (stringp str) (stringp val))))
(declare (ignore str val))
- A version of setenv$ that is an event.