DrACuLa

The objective of the "Dracula" project is to provide a programming environment for the ACL2 language and theorem prover. ACL2, short for A Computational Logic for Applicative Common Lisp, is a programming language and theorem prover. DrScheme is a graphical programming environment for Scheme, Lisp, and other programming languages. This page provides instructions for downloading the software, working in DrScheme's ACL2 language, writing interactive graphical programs, and for reporting bugs.

Keep reading below for installation instructions, and check out the links on the left for tutorials, examples, and bug report instructions.

Dracula has been used to teach a first-year undergraduate logic course at Northeastern University. A report on this course was presented at the ACL2 Workshop in 2007, and can be found here.

Installation

Prerequisites:

• You need DrScheme version 4.0 for the latest release of Dracula. Download and install from the PLT Scheme site.
• You also need ACL2 version 3.1 to 3.3. Download and install from the ACL2 site at UT, Austin.
• Dracula is sensitive to which Common Lisp your ACL2 is built from. The table below lists compatible configurations with links in each cell to the Common Lisp distribution.

Installing Dracula:

• Dracula is available as a Planet package. It can be installed using the planet command line utility. On Windows, this utility is in the directory where PLT Scheme is installed; on Mac or Unix, it is in the bin subdirectory. To install Dracula using this utility, execute:

  planet install cce dracula.plt 3 1

• Read the manual. To find it, start Help Desk via DrScheme's Help menu and follow the manuals link under the Software bullet. Scroll all the way to the bottom and follow the Dracula link.

Legacy version (DrScheme 371-372):

If you have DrScheme 371-372 you can still use Dracula. Simply run the following at the command line:

planet -i cce dracula.plt 2 9

Running Dracula

• Start DrScheme.

• Select Dracula v3.1 as your Language Level.

• You now see a Definitions Window, an Interactions Window, a Run button, a Stop button, and a Start ACL2 button (plus a few others).

• To define and edit functions, use the Definitions window.

• To run your program, click on Run. This adds the content of the Definitions Window to DrScheme's "knowledge base". Now you can evaluate expressions in the Interactions Window that refer to the definitions in the Definitions Window.

  You may also copy and paste such expressions into the Definitions Window. DrScheme will then evaluate them next time you click Run.

  You may also enter definitions into the Interactions Window (if you want to test something on the fly). We don't recommend this, but it is not an uncommon practice for Lisp development.

• To prove theorems, click on Start ACL2 and use the Admit Next and/or Admit All buttons to send the expressions in the definitions window to ACL2. Admitted expressions will be highlighted green, and rejected expressions will be highlighted red.

• To quit the theorem prover, click Stop Prover. You then have a chance to save a transcript of your ACL2 (theorem prover) interactions in a file. You may now restart ACL2 if desired.

Upgrading or Uninstalling

• To uninstall Dracula, run the following at the command line:

  planet remove cce dracula.plt 3 1

• For other versions of Dracula, change the major and minor version numbers. For DrScheme versions 372 and before, change the remove flag to -r:

  planet -r cce dracula.plt 2 9

• To upgrade, remove the old Dracula as shown here. Then follow the installation instructions above.

Acknowledgements

Thanks to Rex Page for the inspiration for this project and Dale Vaillancourt for the initial implementation. Thanks to Carter Schonwald and Ken McGrady for their contributions to Dracula. Thanks to J Moore, Matt Kaufmann, Pete Manolios, Ruben Gamboa, and the rest of the ACL2 community for their support and constructive suggestions.