• 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
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
      • Term
      • Ld
      • Hints
      • Type-set
      • Ordinals
      • Clause
      • ACL2-customization
      • With-prover-step-limit
      • Set-prover-step-limit
      • With-prover-time-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Gcl
      • Oracle-timelimit
      • Thm
      • Defopener
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
      • Ttags-seen
      • Adviser
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Def::doc
      • Syntax
      • Subversive-inductions
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Miscellaneous

ACL2-customization

File of initial commands for ACL2 to run at startup

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.

1. 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:
   • If the customization file name is a relative pathname (see pathname), then the pathname is considered relative to the connected book directory (see cbd).
   • If this variable is not already defined, then its value is set to NONE when books are certified using build::cert.pl or other, legacy Make-based certification tools.
2. Otherwise (empty environment variable value), file "acl2-customization.lsp" or "acl2-customization.lisp" on the connected book directory (see cbd), generally the current directory, is the customization file (in that order) if either exists.
3. Otherwise file "acl2-customization.lsp" or "acl2-customization.lisp" on your home directory is the customization file (in that order), if either 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 except that any settings of ld specials are remembered once this call of ld has completed other than ld-error-action, which will always be :command-conventions after that call of ld completes. 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).

If the customization file exists, it is loaded with ld using the usual default values for the ld specials (see ld) except that :ld-error-action is :error. If an error is encountered, then no subsequent forms in the file will be evaluated and ACL2 will quit immediately.

To create a customization file it is recommended that you first give it a name other than "acl2-customization.lsp" or "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: 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 ld.

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 :ubt 1 before certifying any books; alternatively, see certify-book! for automatic invocation of ubt.

On the other hand, if you wish to prevent undoing commands from the customization file, see reset-prehistory.

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.

Silent loading of ACL2 customization files

When the environment variable ACL2_CUSTOMIZATION_QUIET is set and not "", there will generally be no output from ACL2 customization. A special value of "all" for this variable will cause continued minimal output after startup, as explained in the following remark.

Technical Remark. For quiet loading of acl2-customization files, ld specials are bound to the following values.

ld-verbose = nil
ld-pre-eval-print = :never
ld-post-eval-print = nil
ld-prompt = nil

These ld specials are returned to their normal values after loading an ACL2 customization file, with one exception: if ACL2_CUSTOMIZATION_QUIET has value "ALL" (or "all"; the case is irrelevant), then those values are retained in the ACL2 loop even after customization completes.