ACL2 books certification with SBCL on M1 Mac

[MattKaufmann]

There seem to be problems with recent versions of SBCL on M1 Macs. I don't have an M1 Mac, so I'm not planning to be involved here. But I think it's an important issue, and there seems to have been no recent movement on it; so I'm attaching the acl2-help email thread here:
sbcl-on-m1.txt

[MattKaufmann]

It would be a wonderful contribution to file an SBCL bug report, ideally with an example that doesn't involve ACL2. I think that can be done at https://bugs.launchpad.net/sbcl .

[catap]

Reported to SBCL as https://bugs.launchpad.net/sbcl/+bug/2033922 which was closed as invalid

[snuglas]

The SBCL bug is invalid because the ACL2 source file named 'memoize-raw.lisp' took great liberties with symbols in the SB-VM:: package, particularly READ-CYCLE-COUNTER. Apparently someone already worked around that, but the fix doesn't make a ton of sense. I suspect the SBCL bug was reported by someone who didn't have the aforementioned ACL2 change.
In terms of correctness, the fix is misleading, as it suggests that "some" ARM implementations do/don't have rdtsc.
In fact no release of SBCL has ever exposed rdtsc for ARM, though the CPU does have a cycle count register.

[catap]

@snuglas you're correct. I've reported the bug at SBCL and after that discovered this issue. And yes, the test was at version which doesn't include the commit. Thus, as far as github shows no one version is included it.

[MattKaufmann]

@snuglas Thanks for your comments. Regarding:

  In terms of correctness, the fix is misleading, as it suggests that
  "some" ARM implementations do/don't have rdtsc.

I'd like to clear up anything misleading that I've said about this. Are you referring to the following comment in memoize-raw.lisp?

; We have gotten a report of sb-impl::read-cycle-counter returning 0 as both
; values on an M1 Mac running SBCL.

If so, would it be reasonable for me to extend that comment by mentioning that no release of SBCL has ever exposed rdtsc for ARM?

Also, if you have any suggestions for what to use for SBCL on ARM as a replacement for rdtsc, I'd be interested.

[ericwhitmansmith]

There is at least one other problem with SBCL on ARM-based Macs. See: #1531

[MattKaufmann]

@ericwhitmansmith You say "one other problem" but as far as I know, the problem reported in the present Issue (1495) has been fixed. If that's not the case, please let me know.