|
|
|---|
|
|
|
|---|
Run some events only if an environment variable is defined and nonempty, with build system support.
Ifdef and ifndef, defined in "books/build/ifdef.lisp", support conditionally running some events depending on the build environment. This works as follows:
(ifdef "MY_ENV_VAR" (defun foo (x) x) (include-book "bar") :endif)
produces the given defun and include-book events only if "MY_ENV_VAR" is defined in the environment and is not the empty string. Ifndef has the opposite behavior.
There is special support in the build::cert.pl build system for these constructs, so that if the environment in which the cert.pl scan is run matches the environment in which the ACL2 job is run, the build system will know the true dependencies of the file, taking ifdefs into account.
For this to work correctly, it is important to write the ifdef forms in a
standard manner, as shown above: the
(ifdef "USE_FOO" (include-book "foo") :endif)