You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
It took me a while to get up and running with J-Bob using the Dracula package. In particular:
I didn't realize that I had to install ACL2 separately.
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.
The text was updated successfully, but these errors were encountered:
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.
It took me a while to get up and running with J-Bob using the Dracula package. In particular:
When trying to use the "include-book" command in the Dr. Racket REPL, I'd get an error:
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.
The text was updated successfully, but these errors were encountered: