[acl2/acl2] c1b77f: Tweaked set-theory and hol-in-acl2 libraries. Twe...

[MattKaufmann]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: c1b77f47710a91a9209afd13f344fabd86a6d9c2
https://github.com/acl2/acl2/commit/c1b77f47710a91a9209afd13f344fabd86a6d9c2
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/GNUmakefile
M books/kestrel/auto-termination/README
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
M books/projects/acl2-in-hol/tests/inputs/PKGS.lsp
M books/projects/acl2-in-hol/tests/inputs/PKGS.sml
M books/projects/hol-in-acl2/acl2/hol.lisp
M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/milawa/ACL2/bootstrap/level11/waterfall-steps.lisp
M books/projects/milawa/ACL2/bootstrap/level5/update-clause-bldr.lisp
M books/projects/milawa/ACL2/bootstrap/level9/add-equality.lisp
M books/projects/milawa/ACL2/bootstrap/level9/eqdatabasep.lisp
M books/projects/milawa/ACL2/bootstrap/logic/disjoin-formulas.lisp
M books/projects/milawa/ACL2/bootstrap/logic/proofp-3-provablep.lisp
M books/projects/milawa/ACL2/interface/pcert.lisp
M books/projects/set-theory/foldr.lisp
M books/projects/set-theory/ordinals.lisp
M books/system/check-system-guards.lisp
M books/system/pseudo-good-worldp.lisp

Log Message:
-----------
Tweaked set-theory and hol-in-acl2 libraries. Tweaked a comment in books/system/check-system-guards.lisp. Updated termination database (specifically, *td-candidates*). Fixed a bug in the pseudo-good-worldp check (evaluator-check-inputs is not a global-value), and removed some ttags books from that check. Fixed Milawa issues.

One Milawa issue was a minor bug: fms! was called on an :object
channel, which needed to be a :character channel (and it now is). The
other Milawa issues had to do with violations of redundancy, and I
just hacked my way past them with a sequence of "make" commands with
target milawa-test-extended (in the books/ direcotry), until the last
one concluded successfully.


Commit: 5bc88b3ddafd7f98d05952234f038ea234a38a77
https://github.com/acl2/acl2/commit/5bc88b3ddafd7f98d05952234f038ea234a38a77
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/arm/doc.lisp
M books/kestrel/utilities/defstobj-plus-tests.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/std/obags/core.lisp
M books/std/obags/tests.lisp

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


Commit: 92345c45e845b2a727f9cf8c622577448f4f1070
https://github.com/acl2/acl2/commit/92345c45e845b2a727f9cf8c622577448f4f1070
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/.sys/add-bvxor-nest-to-...@useless-runes.lsp
M books/kestrel/axe/.sys/add-bvxor-nes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-tes...@useless-runes.lsp
M books/kestrel/axe/.sys/evaluate-...@useless-runes.lsp
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-exprs.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-array.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/dargp.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-term-into-dag-array-basic.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/x86/unroller.lisp

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


Compare: https://github.com/acl2/acl2/compare/d9151ad52212...92345c45e845

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

[acl2buildserver]

Branch: refs/heads/testing