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

• ACL2-tutorial

Emacs

Emacs support for ACL2

Many successful users of ACL2 run it in a shell under the Emacs editor. If you do so, then you may wish to load the distributed file emacs/emacs-acl2.el. 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.