Major Section: SWITCHES-PARAMETERS-AND-MODES
ACL2 provides a mechanism to load automatically a so-called ``ACL2
customization file,'' via
ld, the first time
lp is called in an
ACL2 session. ACL2 looks for this file as follows.
o If the host Lisp reads a non-empty value for the system's environment variable
ACL2-CUSTOMIZATION, then that string value is used for the customization file name. In this case, if the file does not exist or if the string is "NONE" then there is no customization file. Notes. (1) If the customization file name is a relative pathname (see pathname), then the pathname is considered relative to the connected book directory (see cbd). (2) If this variable is not already defined, then its value is set to
NONEwhen the ACL2 makefile system is invoked (specifically,
o Otherwise (empty environment variable value), file
"acl2-customization.lisp"on the connected book directory (see cbd), generally the current directory, is the customization file if it exists.
o Otherwise file
"acl2-customization.lisp"on your home directory is the customization file, if it exists (except, this case is skipped on Windows operating systems.
Except for the fact that this
ld command is not typed explicitly by
you, it is a standard
ld command, with one exception: any settings of
ld specials are remembered once this call of
ld has completed.
For example, suppose that you start your customization file with
(set-ld-skip-proofsp t state), so that proofs are skipped as it is loaded
ld. Then the
ld-skip-proofsp will remain
t after the
ld has completed, causing proofs to be skipped in your
ACL2 session, unless your customization file sets this variable back to
nil, say with
(set-ld-skip-proofsp nil state).
If the customization file exists, it is loaded with
ld using the
usual default values for the
ld specials (see ld). Thus, if an
error is encountered, no subsequent forms in the file will be
To create a customization file it is recommended that you first give it a
name other than
"acl2-customization.lisp" so that ACL2 does not try to
include it prematurely when you next enter
lp. Then, while in the
lp, explicitly invoke
ld on your evolving
(but renamed) customization file until all forms are successfully evaluated.
The same procedure is recommended if for some reason ACL2 cannot successfully
evaluate all forms in your customization file: temporarily rename your
customization file so that ACL2 does not try to
ld it automatically and
then debug the new file by explicit calls to
WARNING! If you certify a book after the (automatic) loading of a
customization file, the forms in that file will be part of the
portcullis of the books you certify! That is, the forms in your
customization file at certification time will be loaded whenever anybody uses
the books you are certifying. Since customization files generally
contain idiosyncratic commands, you may not want yours to be part of the
books you create for others. Thus, if you have a customization file
then you may want to invoke
1 before certifying any
books; alternatively, see certify-book! for automatic invocation of
On the other hand, if you wish to prevent undoing commands from the customization file, see reset-prehistory.
Finally, we note that except on Windows-based systems, if there is a file
acl2-init.lsp in your home directory, then it will be loaded into raw
Lisp when ACL2 is invoked.