[acl2/acl2] 7667d3: Fixed a proof-builder bug that could occasionally ...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 7667d34215afee3991c6bbe4ed13a8f8cc11c064
https://github.com/acl2/acl2/commit/7667d34215afee3991c6bbe4ed13a8f8cc11c064
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M proof-builder-a.lisp

Log Message:
-----------
Fixed a proof-builder bug that could occasionally cause two goals to exist with the same name.

Quoting :DOC note-8-7:

Fixed a [proof-builder] bug that could occasionally cause two goals
to exist with the same name.



To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[MattKaufmann]

Branch: refs/heads/testing

[MattKaufmann]

Branch: refs/heads/testing-acl2s

Home: https://github.com/acl2/acl2
Commit: 7667d34215afee3991c6bbe4ed13a8f8cc11c064
https://github.com/acl2/acl2/commit/7667d34215afee3991c6bbe4ed13a8f8cc11c064
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M proof-builder-a.lisp

Log Message:
-----------
Fixed a proof-builder bug that could occasionally cause two goals to exist with the same name.

Quoting :DOC note-8-7:

Fixed a [proof-builder] bug that could occasionally cause two goals
to exist with the same name.

Commit: 32ecc9827d6e0a77147cff19893593ee4134f683
https://github.com/acl2/acl2/commit/32ecc9827d6e0a77147cff19893593ee4134f683

Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-30 (Sun, 30 Nov 2025)

Changed paths:
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt

M other-events.lisp

Log Message:
-----------
Fixed SBCL handling of the :native option of trace! and trace$.

Quoting :DOC note-8-7:

The :native option of [trace!] and [trace$] did not work as one would
reasonably expect when SBCL is the host Lisp; now it does.

Also updated :DOC trace$ and :DOC trace!.


Compare: https://github.com/acl2/acl2/compare/2e73b6035784...32ecc9827d6e