• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
          • World
          • Io
          • Wormhole
          • Programming-with-state
            • Error-triple
            • Cbd
            • State-global-let*
            • Last-prover-steps
            • @
            • Assign
            • Read-run-time
            • Canonical-pathname
            • F-put-global
            • Unsound-eval
            • Setenv$
              • Setenv$-event
            • Er-progn
            • Read-ACL2-oracle
            • With-live-state
            • F-get-global
            • Getenv$
            • Pprogn
            • Get-real-time
            • Makunbound-global
            • Get-cpu-time
            • F-boundp-global
            • Probe-file
          • W
          • Set-state-ok
          • Random$
        • Mutual-recursion
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Loop$
        • Programming-with-state
          • Error-triple
          • Cbd
          • State-global-let*
          • Last-prover-steps
          • @
          • Assign
          • Read-run-time
          • Canonical-pathname
          • F-put-global
          • Unsound-eval
          • Setenv$
            • Setenv$-event
          • Er-progn
          • Read-ACL2-oracle
          • With-live-state
          • F-get-global
          • Getenv$
          • Pprogn
          • Get-real-time
          • Makunbound-global
          • Get-cpu-time
          • F-boundp-global
          • Probe-file
        • Arrays
        • Characters
        • Time$
        • Defmacro
        • Loop$-primer
        • Fast-alists
        • Defconst
        • Evaluation
        • Guard
        • Equality-variants
        • Compilation
        • Hons
        • ACL2-built-ins
        • Developers-guide
        • System-attachments
        • Advanced-features
        • Set-check-invariant-risk
        • Numbers
        • Efficiency
        • Irrelevant-formals
        • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
        • Redefining-programs
        • Lists
        • Invariant-risk
        • Errors
        • Defabbrev
        • Conses
        • Alists
        • Set-register-invariant-risk
        • Strings
        • Program-wrapper
        • Get-internal-time
        • Basics
        • Packages
        • Oracle-eval
        • Defmacro-untouchable
        • <<
        • Primitive
        • Revert-world
        • Unmemoize
        • Set-duplicate-keys-action
        • Symbols
        • Def-list-constructor
        • Easy-simplify-term
        • Defiteration
        • Fake-oracle-eval
        • Defopen
        • Sleep
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Programming-with-state
  • ACL2-built-ins

Setenv$

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 occur.

Example:
(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 code.

Function: setenv$

(defun setenv$ (str val)
  (declare (xargs :guard (and (stringp str) (stringp val))))
  (declare (ignore str val))
  nil)

Subtopics

Setenv$-event
A version of setenv$ that is an event.