So you are interested in proof assistants and you got your paws on the newly published The Little Prover, the latest book of the series you've heard much good about, which includes:
And maybe you've never really been into Scheme, and now you have to figure out which of the many Scheme implementation available is the one you want to get, in order to get the book examples running.
I'll save you that effort in this guide.
Get a scheme
There many choices for a Scheme implementation, as you may have noticed.
They all have their merits, but if you're not completely against IDEs, probably the most convenient one is DrRacket.
DrRacket is an IDE geared geared towards people reading How to Design Programs, SICP and other famous books.
It's used in education, notably by Shriram Krishnamurthi at Brown, and it's very convenient to use, as it includes many different versions of Scheme in a neat package, with package management, many libraries and a lot of documentation.
Visit the DrRacket website and get the installer, run it, and you should be all set.
If you like to have command line control (like me) you'll want to get raco.
You have to run DrRacket and click Help -> Configure command line for Racket ...
That will ask for admin confirmation and install raco.
It points automatically
/Applications/Racket v<version>/bin so you should have
raco available if you restart your shell.
Dracula is a set of ACL2 theorem prover tools in DrRacket, which also includes J-Bob.
If you have raco you can install it with
raco pkg install dracula
or you can install through the UI, File -> Package Manager -> Available from Catalog -> search for Dracula, select it and press Install.
Now you should have Dracula and you'll be able to choose ACL2 as a language to use in DrRacket.
Get the book's code
The book's github repository contains all the code, it's best to have it as a reference, even if Dracula includes J-Bob.
Clone the repository to a directory on your machine:
git clone https://github.com/the-little-prover/j-bob ~/j-bob
j-bob-lang.scmthe J-bob language
little-prover.scmthe transcript of the book's proofs
in ACL2 and in Scheme R5S5 versions:
- for ACL2 under
- for Scheme R5RS under
You can run any of them in DrRacket, by switching the current language, or as a third option just load the version of J-Bob already included in Dracula.
- To switch to the ACL2 language/Dracula choose Language -> Choose Language Pack -> Other Languages -> Dracula -> ACL2.
- To switch to Scheme R5RS choose Language -> Choose Language Pack -> Legacy Languages -> R5RS, you also have to press Show Details and make sure that
Disallow redefinition of initial bindingsis not checked.
Then you load the version of
j-bob-lang.scm for the language you chose fist, then
j-bob.scm and then
little-pover.scm if you want to be able to access each proof from the start.
This will load all the files, including all the proofs
(include-book "j-bob-lang" :dir :teachpacks) (include-book "j-bob" :dir :teachpacks) (include-book "little-prover" :dir :teachpacks)
To run all the proofs up to align/align (might take a lot of cpu/RAM)
The equivalent commands in the other versions:
(load "j-bob-lang.scm") (load "j-bob.scm") (load "little-prover.scm") (dethm.align/align)
(include-book "j-bob-lang") (include-book "j-bob") (include-book "little-prover") (dethm.align/align)
If you're opening them manually using a menu DrRacket will attempt to guess their language and you'll see a yellow message "Determine language from source", you'll have to force the language to be the one you chose again.
Follow the book
The Racket IDE is divided in two spaces, in the upper one you can write all the code you want and then press Run to execute. It's called the definitions area.
The interactions area is just below and works like a REPL, you can write the code and as soon as you press Return it will execute.
If you keep one of the
little-prover.scm versions open while you read you'll be able to check the actual code needed to run the proofs one by one without typing them, though I do recommend typing, in order to learn better.
> (chapter1.example1) 'ham > (chapter2.example1) (if (if (equal a 't) 't (equal 'or '(black coffee))) c c)
You should be ready to get started now, have fun!