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.1+ for the latest release of Dracula. Download and install from the PLT Scheme site.
• You also need ACL2 version 3.1+. Download and install from the ACL2 site at UT, Austin.

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 8 1

• NOTE: There is a known bug in PLT Scheme that may cause an error message like the following when you install Dracula:

  require: unknown module: 'program
setup-plt: error: during Building docs for <PATH TO DRSCHEME CONFIGURATION>/PLT Scheme/planet/300/4.1.3/cache/cce/scheme.plt/2/0/manual.scrbl
setup-plt: require: unknown module: 'program

  You may safely ignore this error message, as it only indicates a problem with documentation for an internal support library.

  Alternately, you can install the library before Dracula:

  planet install cce scheme.plt 2 0

  This will avoid the error message.

• Read the Guide. To find it, start Help Desk via DrScheme's Help menu. The Getting Started section at the top of the page will include a link to Dracula: A Guide to ACL2 in DrScheme.

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

Dracula versions below 6.0 are 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.

Running Dracula

• Start DrScheme.

• Select ACL2 in the Dracula category as your Language Level.

• You now see a Definitions Window, an Interactions Window, a Run button, and a Stop button (plus a few others). The right side of the screen shows a Proof Summary Window, proof control buttons including Start, Admit, and Undo, and a Proof Output Window.

• 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 and use the Admit and/or 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 (which replaces Start while ACL2 is running). 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 8 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.