search

the-little-prover / j-bob

BSD 2-Clause "Simplified" License
420 stars 63 forks source link

Readme doesn't have enough detail to get started #8

Open lorin opened 7 years ago

lorin commented 7 years ago

It took me a while to get up and running with J-Bob using the Dracula package. In particular:

  1. I didn't realize that I had to install ACL2 separately.
  2. I couldn't get J-Bob to load by typing commands in the REPL.

When trying to use the "include-book" command in the Dr. Racket REPL, I'd get an error:

> (include-book "j-bob-lang" :dir :teachpacks)
 Library/Racket/6.10.1/pkgs/dracula/lang/do-check.rkt:92:34: rename-below: defined outside of begin-below in: here

Eventually, I figured out how to do it, and I even wrote up a blog post. I recommend adding more detail to the README to make it easier on new users. I'm happy to submit a PR updating the README with the additional details.

RickMoynihan commented 7 years ago

Totally agree that getting j-bob installed could be made much easier with better instructions.

@lorin Thanks for posting here and your blog post it really helped me get going. One small thing that tripped me up with your instructions was finding the binary downloads on the ACL2 site.

For future travellers, I downloaded the binaries from here: http://acl2s.ccs.neu.edu/acl2s/src/acl2/

anthonyquizon commented 5 years ago

This seemed to work for me (not using drracket): raco pkg install dracula

#lang dracula
(include-book "j-bob-lang" :dir :teachpacks) 
(include-book "j-bob" :dir :teachpacks) 

;;first example using J-Bob
(J-bob/step (prelude)
    '(car (cons 'ham '(cheese))) 
    '((() (car/cons 'ham '(cheese)))))