		Search-engine friendly clone of the ACL2 documentation.

Projects

Sidekick

The ACL2 Sidekick is a graphical add-on for ACL2. It extends your ACL2 session with a web server so that you can interact with ACL2 through your browser. You use the Sidekick along with—not instead of—Emacs or your favorite ACL2 development environment.

Note: the Sidekick is highly experimental software and at this point is mostly a proof of concept.

Screenshots:

Basic Setup

The Sidekick has been tested on CCL on Linux with Firefox or Chromium as the browser. It might possibly work on other Lisps, most likely SBCL and LispWorks.

To build the Sidekick, build ACL2 as usual and then certify at least the basic and ACL2::quicklisp books, e.g.,

$ cd acl2
$ make LISP=ccl
$ cd acl2/books
$ make USE_QUICKLISP=1 basic quicklisp

Then certify the sidekick books:

$ cd acl2/books/projects/sidekick
$ cert.pl top     # should produce top.cert

The Sidekick should now be ready. To try it out, go to the projects/sidekick/demo directory and follow along with demo.lsp.

Sidekick Images

For instant startup times, you can build an ACL2 image with the Sidekick built in.

$ cd acl2/books/projects/sidekick
$ make           # should produce a 'sidekick' executable
$ ./sidekick

You can then use this sidekick executable instead of invoking your normal saved_acl2 image when doing interactive development.

Browser Launching

You can tell the Sidekick to automatically launch a web browser when it boots up by setting the SIDEKICK_BROWSER environment variable. For instance:

$ export SIDEKICK_BROWSER="firefox"

Whatever command you supply will simply be invoked, in the background, with the argument http://localhost:9000/ (or similar).

Other Ports

The Sidekick will try to listen on port 9000 by default, but this can be adjusted using SIDEKICK_PORT. For instance:

$ export SIDEKICK_PORT=9001

You can also explicitly start the sidekick on a different port by using, e.g., (sidekick::start 9001).

Subtopics

Start: Start the ACL2 sidekick web server.
Stop: Stop the ACL2 sidekick web server.
With-sidekick-lock: Special macro that should be used to ensure thread-safety when accessing sidekick state.