read an environment variable
Major Section:  ACL2-BUILT-INS

(Getenv$ str state), where str is a string, reads the value of environment variable str, returning a value of nil if none is found or if the read fails. The logical story is that getenv$ reads its value from the oracle field of the ACL2 state. The return value is thus a triple of the form (mv erp val state), where erp will always be nil in practice, and logically, val is the top of the acl2-oracle field of the state and the returned state has the updated (popped) acl2-oracle.

(getenv$ "PWD" state) ==> (mv nil "/u/joe/work" state)
Also see setenv$.