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

 

Advertisements
This entry was posted in Uncategorized and tagged , , , . Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s