Little Prover's J-Bob problems with set up

[Javier Soto]

Trying to set up J-Bob according to https://github.com/the-little-prover/j-bob there seems to be 2 available ways:

1. Dracula for Racket seems to already include J-Bob. Follow the Installation and Tutorial they provide.

raco pkg install dracula

You also need ACL2 version 3.1. To be downloaded and installed from the ACL2 site at UT, Austin.

ACL2 is not available in homebrew, and seems that we need to make it. Nevertheless, Dracula + ACL2 seem to provide some visual tools to Racket.

2. Manually

- copy the Little-Prover/J-Bob files from the Scheme folder and place them in your directory. These are j-bob.scm, j-bob-lang.scm and little-prover.scm

- open a file and add the code (from Little-Prover/J-Bob README):

;; Load the J-Bob language:
(load "j-bob-lang.scm")
;; Load J-Bob, our little proof assistant:
(load "j-bob.scm")

(J-Bob/step (prelude)

            '(car (cons 'ham '(cheese)))

            '())

- Boom! We start failing at j-bob-lang.scm. Runing that single file in DrRacket it seems that:

• j-bob-lang needs a #lang at the start (i.e. #lang r5rs)
• seems that the file extension being .scm or .rkt doesn't matter.
• There is a conflict between (define s.car car) and (define (car x) (if (pair? x) (s.car x) '())) below. Ryan was trying to circumvent the second define with a set!

And that is where I am so far...

One last thought, Scott thinks that we could also racketify j-bob's syntax code so, for example, we use #f instead of 'nil and #t instead of 't.

[ahmad seleem]

You're faster than me :-) I just found it, too. and was gonna mention it...