Trouble getting this to work in Racket

[Engelberg]

Under the R5RS language in DrRacket, I get the error:

define-values: assignment disallowed;
 cannot change constant
  constant: car

which presumably means that car can't be redefined.

What version of Scheme has this been tested on? Any tips to getting it to work in DrRacket?

[carl-eastlund]

I tested the Scheme mode most recently using Petite Chez Scheme, but I thought I had tried Racket's R5RS mode, too. I guess not recently enough. You can use J-Bob in DrRacket using the Dracula package, or through Petite Chez Scheme, for now. I'll see what I can do for more general Racket compatibility shortly. Sorry for the difficulty.

[xieyuheng]

it is fine for me to run J-bob in racket's interpreter.
is DrRacket (the IDE) different from racket on this redefining matter ?

[carl-eastlund]

That may be the issue. I suspect it may work in the interactions window but not the definitions window.

[carl-eastlund]

Aha, I've found out how you can make it work in DrRacket in the R5RS language.

1. Select the "Language" menu and the "Choose Language ..." option. This should bring up a dialog box.
2. Select "Other Languages", and under "Legacy Languages" choose "R5RS". You had probably already gotten this far, but these instructions might help someone else.
3. Select "Show Details" if there is not already a menu on the right side of the dialog box.
4. Under "Initial Bindings", UN-check the box "Disallow redefinition of initial bindings".
5. Click "OK".

With that box unclicked, you should be able to run the J-Bob code in DrRacket. That option catches some potential errors, but isn't technically R5RS-compliant, so for the language-defining tricks we use in "j-bob-lang.scm", the option needs to be off.

I hope this helps, let me know if you have any more trouble.

[Engelberg]

Following these directions allowed me to run the program without the
redefinitions error:

;; Load the J-Bob language:
(load "j-bob-lang.scm")
;; Load J-Bob, our little proof assistant:
(load "j-bob.scm")
;; Load the transcript of all proofs in the book:
(load "little-prover.scm")
;; Run every proof in the book, up to and including the proof of
align/align:
(dethm.align/align)

but after running for a few seconds, the program quickly ate up all
available memory and returned an error asking me to double the amount of
allocated memory, which I did, and then same error, so I doubled it again
(now to 1gb), at which point it ran until the program hung.

This is on the newest version of Racket (6.2.1) on Windows.

I haven't tried the ACL flavor of J-bob because installing ACL on Windows
is rather complex, so am still hoping to get this working in Racket.

On Thu, Aug 13, 2015 at 7:32 PM, Carl Eastlund notifications@github.com
wrote:

Aha, I've found out how you can make it work in DrRacket in the R5RS
language.

1. Select the "Language" menu and the "Choose Language ..." option.
   This should bring up a dialog box.
2. Select "Other Languages", and under "Legacy Languages" choose
   "R5RS". You had probably already gotten this far, but these instructions
   might help someone else.
3. Select "Show Details" if there is not already a menu on the right
   side of the dialog box.
4. Under "Initial Bindings", UN-check the box "Disallow redefinition
   of initial bindings".
5. Click "OK".

With that box unclicked, you should be able to run the J-Bob code in
DrRacket. That option catches some potential errors, but isn't technically
R5RS-compliant, so for the language-defining tricks we use in
"j-bob-lang.scm", the option needs to be off.

I hope this helps, let me know if you have any more trouble.

—
Reply to this email directly or view it on GitHub
#1 (comment)
.

[xieyuheng]

---

try just do

(load "little-prover.scm")
(dethm.align/align)

---

please see issue: #2
for more information about this

---

[carl-eastlund]

I've updated the Scheme files so that they don't load each other any more, and the README example now works as-is inside DrRacket. Sorry for all the difficulties, and thanks for your patience.