The Little Prover book references a companion proof assistant tool called J-Bob. I had a hard time getting it running using Racket’s Dracula package, here’s how to do it:
- Install Racket.
- Install the Dracula package for Racket. On macOS, I did:
cd /Applications/Racket\ v6.10.1/bin sudo ./raco pkg install dracula
- Download ACL2. I ended up grabbing a pre-built binary gzipped tarball which was for 7.1, but the latest is 7.4 if you want to build from source. You can get the binaries at http://acl2s.ccs.neu.edu/acl2s/src/acl2/
- Unzip the ACL2 tarball somewhere, I put it in my home directory, so it ended up as ~/acl2-image-7.1-macosx.x86_64
- Launch the DrRacket IDE
- Menu: Language -> Choose Language -> Other Languages -> Dracula -> ACL2
- Menu: Dracula -> Change ACL2 Executable Path… -> Point it at the run_acl2 binary in the directory where you installed ACL2.
- In the top-left window, paste the following:
(include-book "j-bob-lang" :dir :teachpacks) (include-book "j-bob" :dir :teachpacks) (include-book "little-prover" :dir :teachpacks)
Note: Running these commands in the REPL in the bottom-left window didn’t work for me.
- Click the “Run” button at the top-right of the Dr. Racket window.
You’re now set up to use J-Bob. Verify it worked by typing the following in the interpreter in the bottom-left window of Dr. Racket.
(J-Bob/step (prelude) '(car (cons 'ham '(cheese))) '())
The output should be:
(car (cons 'ham '(cheese)))