read an environment variable
Major Section:  PROGRAMMING

(Getenv$ str), where str is a string, reads the value of environment variable str, returning nil if none is found or if the read fails. The formal 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, val is the value that has been read, and state is the new state, which is obtained by popping val from the top of the state's oracle.

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