Comments (7)
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.
from j-bob.
it is fine for me to run J-bob in racket's interpreter.
is DrRacket (the IDE) different from racket on this redefining matter ?
from j-bob.
That may be the issue. I suspect it may work in the interactions window but not the definitions window.
from j-bob.
Aha, I've found out how you can make it work in DrRacket in the R5RS language.
- Select the "Language" menu and the "Choose Language ..." option. This should bring up a dialog box.
- Select "Other Languages", and under "Legacy Languages" choose "R5RS". You had probably already gotten this far, but these instructions might help someone else.
- Select "Show Details" if there is not already a menu on the right side of the dialog box.
- Under "Initial Bindings", UN-check the box "Disallow redefinition of initial bindings".
- 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.
from j-bob.
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 [email protected]
wrote:
Aha, I've found out how you can make it work in DrRacket in the R5RS
language.
- Select the "Language" menu and the "Choose Language ..." option.
This should bring up a dialog box.- Select "Other Languages", and under "Legacy Languages" choose
"R5RS". You had probably already gotten this far, but these instructions
might help someone else.- Select "Show Details" if there is not already a menu on the right
side of the dialog box.- Under "Initial Bindings", UN-check the box "Disallow redefinition
of initial bindings".- 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)
.
from j-bob.
try just do
(load "little-prover.scm")
(dethm.align/align)
please see issue: #2
for more information about this
from j-bob.
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.
from j-bob.
Related Issues (9)
- Error following README instructions for loading J-Bob into ACL2 HOT 2
- Error to `raco pkg install dracula` on win10 from racket8.8 HOT 2
- reloading source code in source code conflicts with the instructions in README HOT 5
- Does this work with guile? HOT 2
- Racket/Dracula
- Scheme J-Bob/step examples w/ non-null focus paths return incorrect results; ACL2 equivalents return correctly. HOT 2
- Readme doesn't have enough detail to get started HOT 2
- why make car and cdr total ?
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from j-bob.