Error following README instructions for loading J-Bob into ACL2

[lukego]

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 ********

[lukego]

I asked about this on the #acl2 IRC channel and got some feedback that I post here in case it is useful to anyone else.

[carl-eastlund]

Sorry for the delay in addressing this. I've just merged @ericwhitmansmith's fix. Thanks for the patch, Eric.