• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
      • Gentle-introduction-to-ACL2-programming
      • ACL2-tutorial
        • Introduction-to-the-theorem-prover
        • Pages Written Especially for the Tours
        • The-method
        • Advanced-features
        • Interesting-applications
        • Tips
        • Alternative-introduction
        • Tidbits
        • Annotated-ACL2-scripts
        • Startup
        • ACL2-as-standalone-program
        • ACL2-sedan
        • Talks
        • Nqthm-to-ACL2
        • Emacs
      • About-ACL2
    • Real
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• ACL2-tutorial

Emacs

Emacs support for ACL2

Many successful users of ACL2 take advantage of the Emacs editor, for example by running ACL2 in an Emacs shell buffer. If you do so, then you may wish to load the distributed file emacs-acl2.el from one of two directories under the main ACL2 directory: books/emacs/ if you use a recent version of Emacs, or emacs/ if you use Emacs 24. An easy way to arrange this is to put the load form into your .emacs file; here, DIR denotes your main ACL2 directory.

(load "DIR/books/emacs/emacs-acl2.el") ; for recent Emacs versions

-OR-

(load "DIR/emacs/emacs-acl2.el") ; for Emacs 24

The file begins with considerable comments describing what it offers.

In particular, the above file provides the ACL2-Doc browser, a convenient tool for viewing, in Emacs, documentation for both the ACL2 system and the documented community books, as well as custom manuals. See ACL2-Doc.

If you are not comfortable with Emacs, you may prefer to use an Eclipse-based interface; see ACL2-sedan.