ACL2-CUSTOMIZATION

customizing ACL2 for a particular user
Major Section:  MISCELLANEOUS

The file "acl2-customization.lisp" is automatically loaded, via ld, the first time lp is called in an ACL2 session, provided such a file exists on the current directory. 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 with ld. Then the ld special 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).

The customization file "acl2-customization.lisp" actually resides on the connected book directory; see cbd. Except, if that file does not exist, then ACL2 looks for "acl2-customization.lisp" on your home directory. If ACL2 does not find that file either, then no customization occurs and lp enters the standard ACL2 read-eval-print loop.

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

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 uncustomized 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: rename your customization file so that ACL2 does not try to ld it automatically and then debug the new file by explicit calls to ld.

When you have created a file that can be loaded with ld without error and that you wish to be your customization file, name it "acl2-customization.lisp" and put it on the current directory or in your home directory. The first time after starting up ACL2 that you invoke (lp), ACL2 will automatically load the "acl2-customization.lisp" file from the cbd (see cbd) if there is one, and otherwise will load it from your home directory.

Note that if you certify a book after the (automatic) loading of an acl2-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 :ubt 1 before certifying any books.

The conventions concerning ACL2 customization are liable to change as we get more experience with the interaction between customization, certification of books for others, and routine undoing. For example, at the moment it is regarded as a feature of customization that it can be undone but it might be regarded as a bug if you accidentally undo your customization.