ACL2 does not build on SBCL 2.4.2

[mister-walter]

ACL2 does not build on SBCL 2.4.2

[MattKaufmann]

Thanks. This is actually horrifying, because ACL2 can prove
(thm (booleanp (standard-char-p x))).
Im aware of the "generalized boolean" issue but this is the first time it's bitten us.
I'll pursue this further later....

[MattKaufmann]

SBCL no longer has this issue (as of its commit 780ec048d0 yesterday). This morning I cloned the latest SBCL, built ACL2 on it, and ran a successful "regression-everything". I might (soon-ish) add a little to the error message for SBCL 2.4.2 users, suggesting use of either SBCL 2.4.1 or the latest github version of SBCL.

[MattKaufmann]

That's seems strange to me, since I get the following with SBCL 2.4.1 on Linux.

ACL2 !>(standard-char-p (code-char 10))
T
ACL2 !>

But maybe this has something to do with multiple characters, as you note.
I'll look into it soon, probably later today. Thanks for the report.

[mister-walter]

I didn't dig into this enough - it seems like it might be a bug, as standard-character-p is not returning a Boolean on SBCL 2.4.2 in this case:

# SBCL 2.4.1
* (standard-char-p (code-char 10))
T

# SBCL 2.4.2
* (standard-char-p (code-char 10))
#\Newline

acl2-check.lisp relies on the result being a Boolean.

[mister-walter]

Actually this seems to be allowed behavior by SBCL according to the HyperSpec, as standard-character-p is specified as returning a generalized boolean.

I think that replacing the form starting on line 267 of acl2-check.lisp with the following should resolve the immediate problem. Running the below form on SBCL 2.4.2 does not result in an error, while running the original form does.

(dotimes (i 256)
         (let ((ch (code-char i)))
           (or (equal (not (null (standard-char-p ch)))
                      (or #+(and mcl (not ccl))
                          (= i 13)
                          #-(and mcl (not ccl))
                          (= i 10)
                          (and (>= i 32)
                               (<= i 126))))
               (error "This Common Lisp is unsuitable for ACL2 because the ~
                       character~%with char-code ~d ~a standard in this ~
                       Common Lisp but should~%~abe."
                      i
                      (if (standard-char-p ch) "is" "is not")
                      (if (standard-char-p ch) "not " "")))))

I can submit a PR for this change if you would like.

[MattKaufmann]

I see what's going on. Common Lisp specifies that a predicate can
return a "generalized Boolean", which is actually anything at all --
nil represents false, and everything else represents true. However,
SBCL 2.4.2 is the first time we've seen this, over more than 30 years
of ACL2 development with multiple Lisps hosting the system (currently,
six of them). In case anyone is interested, here is the relevant
definition from file src/code/target-char.lisp of the SBCL 2.4.2
source distribution.

(defun standard-char-p (char)
  "The argument must be a character object. STANDARD-CHAR-P returns true if the
argument is a standard character -- one of the 95 ASCII printing characters or
<return>."
  (let ((n (char-code char)))
    ;; returning CHAR for true is fine, and it's already in a register,
    ;; but the compiler can't infer BASE-CHAR from the constraint on N,
    ;; so we have to force it.
    (if (std-char-code-p n) (truly-the base-char char) nil)))

So apparently standard-char-p is the identity function on standard
characters.

My plan is to email the sbcl-help list tomorrow to see if maybe this
wasn't really intended and might be "fixed" in the next SBCL release.
I'm guessing that the answer will be "no" (explicitly or implicitly).
In that case, our plan is to replace standard-char-p by a new function,
standard-char-p$, whose definition matches what's currently in the
ACL2 logic for standard-char-p (hence, returns a Boolean). I'll make
that replacement in the community books as well.

I suppose we could redefine standard-char-p in raw Lisp, though I
don't like that idea since maybe SBCL depends on the new definition
somehow. For what it's worth, I'll also note that same SBCL source
file declares standard-char-p to be inline (with a suitable declaim
form).

By the way, I don't want to redefine standard-char-p, in part because
it's apparently inlined.

[xgqt]

I might (soon-ish) add a little to the error message for SBCL 2.4.2 users, suggesting use of either SBCL 2.4.1 or the latest github version of SBCL.

Please do so, we ran into this in Gentoo: https://bugs.gentoo.org/926360

[MattKaufmann]

@xgqt Sorry about the inconvenience. I've added such an error message (github master commit 2f29000). I think this issue can be closed.

[mister-walter]

Thanks so much Matt!

[xgqt]

@xgqt Sorry about the inconvenience. I've added such an error message (github master commit 2f29000). I think this issue can be closed.

No need to be sorry :D I dont think anybody knew we could run into this. Thanks a lot for the fix.