J-Bob from the Little Prover

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:

1. Install Racket.
2. Install the Dracula package for Racket. On macOS, I did:

   cd /Applications/Racket\ v6.10.1/bin
   sudo ./raco pkg install dracula

3. 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/
4. Unzip the ACL2 tarball somewhere, I put it in my home directory, so it ended up as ~/acl2-image-7.1-macosx.x86_64
5. Launch the DrRacket IDE
6. Menu: Language -> Choose Language -> Other Languages -> Dracula -> ACL2
7. Menu: Dracula -> Change ACL2 Executable Path… -> Point it at the run_acl2 binary in the directory where you installed ACL2.
8. 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.

9. 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)))