[acl2/acl2] d3d0e0: [axe] Add comment.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: d3d0e0c2ff496e6516e361c81445f3e29ddb7dfc
https://github.com/acl2/acl2/commit/d3d0e0c2ff496e6516e361c81445f3e29ddb7dfc
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/axe/rules3.lisp

Log Message:
-----------
[axe] Add comment.


Commit: 79280215d45c627fe422669582d7524b626a9b0d
https://github.com/acl2/acl2/commit/79280215d45c627fe422669582d7524b626a9b0d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
A books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/x86/package.lsp

Log Message:
-----------
[axe] Pull out common lists of imported symbols.


Commit: 2e3b4d982d3b24adb2c9313b3c331c742ac5ad2f
https://github.com/acl2/acl2/commit/2e3b4d982d3b24adb2c9313b3c331c742ac5ad2f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/x86/package.lsp

Log Message:
-----------
[axe] Continue improving packages.


Commit: 238b8848f159ba0de72d656b9613279c964ddb36
https://github.com/acl2/acl2/commit/238b8848f159ba0de72d656b9613279c964ddb36
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/doc/practices.lisp
M books/quicklisp/top.lisp

Log Message:
-----------
Merge.


Commit: aba164d76db88e385ad7bd646f2236c408b18fbb
https://github.com/acl2/acl2/commit/aba164d76db88e385ad7bd646f2236c408b18fbb
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/axe/rules3.lisp
M books/kestrel/bv/bvuminus.lisp

Log Message:
-----------
[bv] Add some rules.

These include commutativity rules for bvplus that treat bvuminus as invisible, and other related rules.


Commit: 602526fe68856bd4f48ab56577fcd0e3efd95817
https://github.com/acl2/acl2/commit/602526fe68856bd4f48ab56577fcd0e3efd95817
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/axe/axe-rules-mixed.lisp

Log Message:
-----------
[axe] Tweak hints.


Commit: 10ecd0cefc427785d8a96940b26e63c31c8ab2bd
https://github.com/acl2/acl2/commit/10ecd0cefc427785d8a96940b26e63c31c8ab2bd
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/x86/tools/lifter-support.lisp

Log Message:
-----------
Merge.


Compare: https://github.com/acl2/acl2/compare/cebe6962b86c...10ecd0cefc42

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

[Eric W. Smith]

Branch: refs/heads/master

[Eric W. Smith]

Branch: refs/heads/testing

[MattKaufmann]

Branch: refs/heads/testing-acl2s

Home: https://github.com/acl2/acl2
Commit: d3d0e0c2ff496e6516e361c81445f3e29ddb7dfc
https://github.com/acl2/acl2/commit/d3d0e0c2ff496e6516e361c81445f3e29ddb7dfc
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/axe/rules3.lisp

Log Message:
-----------
[axe] Add comment.


Commit: 79280215d45c627fe422669582d7524b626a9b0d
https://github.com/acl2/acl2/commit/79280215d45c627fe422669582d7524b626a9b0d
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
A books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/x86/package.lsp

Log Message:
-----------
[axe] Pull out common lists of imported symbols.

Commit: c5df6ce95d51ae90561aa961118a0420bfcb61b3
https://github.com/acl2/acl2/commit/c5df6ce95d51ae90561aa961118a0420bfcb61b3
Author: Grant Jurgensen <gr...@jurgensen.dev>

Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
[doc] Update best-practices advice on predicates

Provide more concrete advice on naming predicates.


Commit: cd539c07efb92686f81e0b63618ff5599fc7b04c
https://github.com/acl2/acl2/commit/cd539c07efb92686f81e0b63618ff5599fc7b04c
Author: Grant Jurgensen <gr...@jurgensen.dev>

Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:

M books/quicklisp/top.lisp

Log Message:
-----------
[doc] Update osicat build failure advice

Replace advice with a more succinct command.

Commit: 2e3b4d982d3b24adb2c9313b3c331c742ac5ad2f
https://github.com/acl2/acl2/commit/2e3b4d982d3b24adb2c9313b3c331c742ac5ad2f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/package.lsp
M books/kestrel/x86/package.lsp

Log Message:
-----------
[axe] Continue improving packages.


Commit: 238b8848f159ba0de72d656b9613279c964ddb36
https://github.com/acl2/acl2/commit/238b8848f159ba0de72d656b9613279c964ddb36
Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/doc/practices.lisp
M books/quicklisp/top.lisp

Log Message:
-----------
Merge.

Commit: cebe6962b86cd850f0a82bf18362b1f64d8f8723
https://github.com/acl2/acl2/commit/cebe6962b86cd850f0a82bf18362b1f64d8f8723

Author: Eric Smith <ews...@gmail.com>
Date: 2025-11-24 (Mon, 24 Nov 2025)

Changed paths:
M books/kestrel/x86/tools/lifter-support.lisp

Log Message:
-----------

[axe/x86] Improve lifter.

Support :rip as the output-indicator, to allow extracting the final program counter.

Commit: 0d043185a65ccbb79c20458d9d64c22754f23b3f
https://github.com/acl2/acl2/commit/0d043185a65ccbb79c20458d9d64c22754f23b3f
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2025-11-25 (Tue, 25 Nov 2025)

Changed paths:
M axioms.lisp
M books/system/doc/acl2-doc.lisp
M defthm.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M rewrite.lisp

Log Message:
-----------
Fixed bugs involving large arrays not created by defstobj due to :non-executable t and in :pr.

Quoting :DOC note-8-7:

Fixed a bug that was causing errors for [stobj]s introduced with
[defstobj] keyword argument :non-executable t in the presence of
large arrays. This should not have caused an error, since that
keyword argument prevents attempts at contructing the stobj (with
its arrays).

Fixed a bug in :[pr] to work on function symbols introduced by
[defstobj] (GitHub Issue 1851). Thanks to David Taylor for
reporting this bug.

Quoting an implementation-level comment in (defxdoc note-8-7 ...):

; Fixed function find-rules-of-rune to work on runes introduced by defstobj.
; This is related to the fix for :pr: both use a new function,
; world-to-next-non-deeper-event, in place of world-to-next-event.


Compare: https://github.com/acl2/acl2/compare/7fc5284692f8...0d043185a65c