Other Requirements

ACL2 is distributed on the Web without fee.

There is a License agreement, which is available via the ACL2 Home Page link below.

ACL2 currently runs on Unix, Linux, Windows, and Macintosh OS X operating systems.

It can be built in any of the following Common Lisps:

  * Allegro Common Lisp,
  * CCL (formerly OpenMCL)
  * CLISP,
  * CMU Common Lisp,
  * GCL (Gnu Common Lisp),
  * LispWorks, and
  * SBCL (Steel Bank Common Lisp)