		Search-engine friendly clone of the ACL2 documentation.

Cert.pl

Ifdef-define

Define an environment variable for use with ifdef and ifndef.

This is simply a macro defined as follows:

Macro: ifdef-define

(defmacro ifdef-define (x)
          (cons 'value-triple
                (cons (cons 'setenv$ (cons x '("1")))
                      'nil)))

When this form is loaded, it will set the given environment variable to "1", affecting subsequent uses of ifdef and ifndef. The cert.pl build system tracks uses of this macro in order to determine which forms in the file are really used, so as to correctly compute the dependencies between files. In order to be correctly scannable by the build system, the ifdef-define form must occur all on one line:

(ifdef-define "FOO")

(acl2::ifdef-define "FOO")

Note that the effects of this form are local to the current book; see ifdef-define! for a version that persists across include-books. Also see ifdef-undefine and ifdef-undefine!.