• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
    • Miscellaneous
    • Output-controls
    • Bdd
    • Macros
    • Installation
      • Obtaining-common-lisp
      • Installation-instructions
      • Using-ACL2
      • Installation-support
        • Creating-executable
        • Windows-installation
        • Summary-of-ACL2-system-distribution
        • Running-ACL2-without-executable
    • Mailing-lists
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Installation-support

Summary-of-ACL2-system-distribution

Summary of ACL2 system distribution

This topic discusses a distribution that includes only the ACL2 system, without the community-books.

See installation-instructions for how to obtain a gzipped tarfile that contains both the ACL2 sources and community books. Below we describe the ACL2 distribution only (without the community books). Its files are available by obtaining a gzipped tarfile, acl2.tar.gz. If you download this file and extract it with

tar xfz acl2.tar.gz

then you will create a subdirectory, acl2-sources, which is approximately the usual ACL2 distribution (see installation-instructions) without the books subdirectory. Among its contents, in addition to the ACL2 source files, are the following.

LICENSE       ; ACL2 license file
GNUmakefile   ; For use with GNU make
TAGS          ; Handy for looking at source files with emacs
TAGS-acl2-doc ; Handy for finding code in books, e.g., with the acl2-doc browser
acl2-customization-files/ ; Useful for certifying books, e.g., with ACL2(p)
bin/          ; Contains an executable script, bin/acl2, which invokes ACL2
doc/          ; ACL2 documentation
emacs/        ; Some helpful emacs utilities

Also available are images/, which may contain executables; see images/Readme.html

GitHub Distributions

We strongly recommend that ACL2 users update their local copies of the system and community-books every time there is an ACL2 release. While that should suffice for many ACL2 users, nevertheless for those who prefer to obtain the latest developments, the ACL2 source code and community books are available between ACL2 releases, by way of revision control using git. See the GitHub ACL2 project website for more information.