Hello! I've started reading The Little Prover and I installed ACL2 for the first time. I get errors about books not being "certified" when I try to follow the instructions in the README though. I am wondering if the error is something that I need to troubleshoot on my side or if it's a bug in this repo?

Here's the transcript running ACL2 on NixOS Linux and the latest version from this repo:

luke@thinky:~/git/j-bob/acl2]$ acl2
This is SBCL 2.0.8.nixos, an implementation of ANSI Common Lisp.
More information about SBCL is available at <http://www.sbcl.org/>.

SBCL is free software, provided as is, with absolutely no warranty.
It is mostly in the public domain; some portions are provided under
BSD-style licenses.  See the CREDITS and COPYING files in the
distribution for more information.

 ACL2 Version 8.3 built February 12, 2021  13:57:32.
 Copyright (C) 2020, Regents of the University of Texas
 ACL2 comes with ABSOLUTELY NO WARRANTY.  This is free software and you
 are welcome to redistribute it under certain conditions.  For details,
 see the LICENSE file distributed with ACL2.

 Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
 See the documentation topic note-8-3 for recent changes.
 Note: We have modified the prompt in some underlying Lisps to further
 distinguish it from the ACL2 prompt.

ACL2 Version 8.3.  Level 1.  Cbd "/home/luke/git/j-bob/acl2/".
System books directory 
"/nix/store/nhq9v7x3a2d01cx0fbcmjna04fp8xhjg-acl2-8.3/share/acl2/books/".
Type :help for help.
Type (good-bye) to quit completely out of ACL2.

ACL2 !>(include-book "j-bob-lang")

ACL2 Warning [Compiled file] in ( INCLUDE-BOOK "j-bob-lang" ...): 
Unable to load compiled file for book
  /home/luke/git/j-bob/acl2/j-bob-lang.lisp
because that book is not certified.  See :DOC include-book.  No load
was in progress for any parent book.


ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "j-bob-lang" ...):  There
is no certificate on file for "/home/luke/git/j-bob/acl2/j-bob-lang.lisp".


Summary
Form:  ( INCLUDE-BOOK "j-bob-lang" ...)
Rules: NIL
Warnings:  Uncertified and Compiled file
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
 "/home/luke/git/j-bob/acl2/j-bob-lang.lisp"
ACL2 !>(include-book "j-bob")

ACL2 Warning [Compiled file] in ( INCLUDE-BOOK "j-bob" ...):  Unable
to load compiled file for book
  /home/luke/git/j-bob/acl2/j-bob.lisp
because that book is not certified.  See :DOC include-book.  No load
was in progress for any parent book.


ACL2 Warning [Uncertified] in ( INCLUDE-BOOK "j-bob" ...):  There is
no certificate on file for "/home/luke/git/j-bob/acl2/j-bob.lisp".



ACL2 Error in ( DEFUN REWRITE/DEFINE+ ...):  It is illegal to supply
a measure for a non-recursive function, as has been done for REWRITE/DEFINE+.
To avoid this error, see :DOC set-bogus-measure-ok.


ACL2 Warning in ( INCLUDE-BOOK "j-bob" ...):  The error reported above
indicates that this book is incompatible with the current logical world.
The attempted INCLUDE-BOOK has failed.


Summary
Form:  ( INCLUDE-BOOK "j-bob" ...)
Rules: NIL
Warnings:  Uncertified and Compiled file
Time:  0.11 seconds (prove: 0.00, print: 0.00, other: 0.11)

ACL2 Error in ( INCLUDE-BOOK "j-bob" ...):  See :DOC failure.

******** FAILED ********

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?

I was going through the Recess section on J-Bob, starting on page 164, when I noticed that some of the Scheme examples in little-prover.scm give incorrect results when run in MITScheme/DrRacket, but their ACL2 equivalents in little-prover.lisp give correct results when run in ACL2/DrRacket. I ran the first five Chapter 1 examples in both MIT/GNU Scheme and Dr Racket using R5RS (as described in the README) - the REPL dialogue in both interpreters proceeded as follows:

$ (load "j-bob/scheme/j-bob-lang.scm")
$ (load "j-bob/scheme/j-bob.scm")
$ (load "j-bob/scheme/little-prover.scm")
$ (chapter1.example1) ;;
-> (car (cons 'ham '(eggs))) ;; INCORRECT; should be 'ham
$ (chapter1.example2)
-> 't ;; CORRECT
$ (chapter1.example3)
-> (atom (cons 'ham '(eggs))) ;; INCORRECT; should be 'nil
$ (chapter1.example4)
-> 'nil ;; CORRECT
$ (chapter1.example5)
-> (equal 'flapjack (atom (cons a b))) ;; INCORRECT; should be 'nil

I noticed that the correct and incorrect examples differ in one key respect: the correct examples have no path to the focus (i.e., the focus is the entire expression) in their definitions, whereas the incorrect examples have at least one step with a path to the focus. Here's the same Chapter 1 examples, run with the ACL2 Dracula package in Dr Racket, showing correct output for all examples:

$ (include-book "j-bob-lang" :dir :teachpacks)
$ (include-book "j-bob" :dir :teachpacks)
$ (include-book "little-prover" :dir :teachpacks)
$ (chapter1.example1)
-> 'ham ;; CORRECT
$ (chapter1.example2)
-> 't ;; CORRECT
$ (chapter1.example3)
-> 'nil ;; CORRECT
$ (chapter1.example4)
-> 'nil ;; CORRECT
$ (chapter1.example5)
-> 'nil ;; CORRECT

Diagnosing why this is occurring is beyond my abilities at this point - can one of the authors, or someone who is more well-versed in Scheme/LISP than I am, explain what's going on here?

It took me a while to get up and running with J-Bob using the Dracula package. In particular:

1. I didn't realize that I had to install ACL2 separately.
2. 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.

I was wondering if there's a way to use DrRacket + Dracula integration to use J-Bob as an interactive assistant. There's seems to be a panel to the right that indicates it could show me the state of the proof à-là Coq.

My typical mistakes are in the number of arguments or substituting a 't for a '? or that some variable isn't in scope (something a basic type-checker would point out ;-) ) which takes a while to find and all I have to troubleshoot is whether the theorem was accepted or not.

When i install dracula package by raco, it tells me that it needs to install dependency planet-schematics-random1, then it log cannot open module file \n module path: test-engine/scheme-gui, like this:

open-input-file: cannot open module file
  module path: test-engine/scheme-gui
  path: C:\Program Files\Racket\share\pkgs\htdp-lib\test-engine\scheme-gui.rkt
  system error: no such file or directory; rkt_err=3
  compilation context...:
   C:\Users\31090\AppData\Roaming\Racket\8.8\pkgs\dracula\private\scheme\test\test-drscheme.rkt
  context...:
   C:\Program Files\Racket\collects\racket\require-transform.rkt:266:2: expand-import
   C:\Program Files\Racket\collects\racket\private\reqprov.rkt:498:5
...

There are a lot of error messages like the following at the end of the output

raco setup: error: during making for <pkgs>/dracula/drscheme
raco setup:   open-input-file: cannot open module file
raco setup:     module path: test-engine/scheme-gui
raco setup:     path: C:\Program Files\Racket\share\pkgs\htdp-lib\test-engine\scheme-gui.rkt
raco setup:     system error: no such file or directory; rkt_err=3
raco setup:     compiling: <pkgs>/dracula/private/scheme/drscheme.rkt

I tried to find the reason of the error, dracula shows on racket package webpage that the dependency it needs to install , called planet-schematics-random1.plt doesn't exist.

I geuss that's why the installation failed.

is it for to make the implementation simple [about error handling] ?
or it is essential to the implementation of j-bob ?

With guile, I get

% guile
GNU Guile 2.0.11
Copyright (C) 1995-2014 Free Software Foundation, Inc.

Guile comes with ABSOLUTELY NO WARRANTY; for details type `,show w'.
This program is free software, and you are welcome to redistribute it
under certain conditions; type `,show c' for details.

Enter `,help' for help.
scheme@(guile-user)> (load "j-bob-lang.scm")
scheme@(guile-user)> (load "j-bob.scm")
scheme@(guile-user)> (load "little-prover.scm")
scheme@(guile-user)> (chapter1.example1)
$1 = (car (cons (quote ham) (quote (eggs))))

I thought the result was supposed to be 'ham.

hi Carl

it is about the scheme version of j-bob

in j-bob.scm
I see you are using (load "j-bob-lang.scm")

and
in little-prover.scm
you are using (load "j-bob.scm")

and in README.md
you said

;; 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)

note that
function redefinition is side effect

thus
this will redefine a lots of primitive functions multiple times
and use these multiple redefined functions to redefine other functions

this hurts performance

as a result
when I follow the instructions in README.md
my scheme interpreter will eat up all the memory of my machine [about 2G of memory]

you can fix this in many ways
my advice is to keep the README.md as it is
and do not use (load) in source code