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. DrRacket is a graphical programming environment for Racket, Scheme, ACL2, and other programming languages. This page provides instructions for downloading the software, working in Racket'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.
planetin all instructions.
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 Racket is installed; on Mac or Unix, it is in the
bin subdirectory. To install Dracula using this utility, execute:
raco planet install cce dracula.plt 8 23
If the Planet server is unavailable, the current version of Dracula can be downloaded via this link. To install this package manually, download it and execute the following from the directory it is saved in:
raco planet fileinject cce dracula.plt 8 23
Read the Guide. To find it, start Help Desk via DrRacket's Help menu. The section titled "Other Languages in the Racket Environment" will include links to "Dracula: A Guide to ACL2 Theorem Proving in DrRacket" and "Dracula: Reference Manual".
If the Dracula language or its documentation does not get installed correctly, try running the following command to fix it:
If that does not work, you can uninstall Dracula using the instructions below and try to reinstall. Alternately, feel free to inquire on the Racket User's mailing list, file a bug report via DrRacket's Help menu, or contact the author.
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 DrRacket'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. DrRacket 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
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.
You should see output similar to the following:
raco planet show
The two numbers after
cce dracula.plt 8 23
schematics random.plt 1 0
cce dracula.pltare Dracula's version number. In the output above, Dracula version 8.23 is installed.
raco planet remove cce dracula.plt 8 23
Remember to replace
raco planet remove cce dracula.plt 7 1
planetwhen using DrScheme instead of DrRacket.
Thanks to Rex Page for the inspiration for this project and Dale Vaillancourt for the initial implementation. Thanks to Zoe Zhang, 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.