[acl2/acl2] d92ba4: FGL: add a stack debugging function

[solswords]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: d92ba452b772593246eefce3d7a648b720ee67fc
https://github.com/acl2/acl2/commit/d92ba452b772593246eefce3d7a648b720ee67fc
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-02-20 (Fri, 20 Feb 2026)

Changed paths:
M books/centaur/fgl/annotation.lisp

Log Message:
-----------
FGL: add a stack debugging function


Commit: 4804d9fdba765738a47cc0ee2d27235fb510b458
https://github.com/acl2/acl2/commit/4804d9fdba765738a47cc0ee2d27235fb510b458
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-02-20 (Fri, 20 Feb 2026)

Changed paths:
M books/centaur/fgl/annotation.lisp
M books/centaur/fgl/constraint-db.lisp
M books/centaur/fgl/fgl-object.lisp
M books/centaur/fgl/interp.lisp
M books/centaur/meta/bindinglist.lisp
A books/centaur/meta/fnsymlist.lisp
M books/centaur/meta/package.lsp
M books/centaur/meta/subst-vars.lisp
M books/centaur/meta/subst.lisp
M books/centaur/meta/term-vars.lisp

Log Message:
-----------
FGL: add an annotation feature to help fix a rewrite loop


Commit: 4e110f572cd1a19bb002ef8d0cb0974ac5b9eede
https://github.com/acl2/acl2/commit/4e110f572cd1a19bb002ef8d0cb0974ac5b9eede
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-02-23 (Mon, 23 Feb 2026)

Changed paths:
M books/centaur/fgl/annotation.lisp
M books/centaur/fgl/congruence-rules.lisp
M books/centaur/fgl/congruence.lisp
M books/centaur/fgl/interp.lisp
M books/centaur/meta/congruence.lisp

Log Message:
-----------
FGL: broaden identity congruences to allow multiarg functions


Commit: 00d89ca8be12e05a169d5905ca8edf42ac2c123d
https://github.com/acl2/acl2/commit/00d89ca8be12e05a169d5905ca8edf42ac2c123d
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-02-23 (Mon, 23 Feb 2026)

Changed paths:
M books/centaur/fgl/binder-rules.lisp
M books/centaur/fgl/congruence.lisp
M books/centaur/fgl/contexts.lisp
M books/centaur/fgl/interp.lisp
M books/centaur/fgl/rules.lisp
M books/centaur/gl/gl-generic-clause-proc.lisp
M books/centaur/gl/gl-generic-interp-defs.lisp
M books/centaur/gl/gl-generic-interp.lisp
M books/centaur/gl/glcp-rewrite-tables.lisp
M books/centaur/gl/rewrite-tables.lisp
M books/centaur/gl/run-gified-cp.lisp
M books/centaur/glmc/glmc-generic-proof.lisp
M books/centaur/glmc/glmc.lisp
M books/centaur/meta/congruence.lisp
M books/centaur/meta/equivalence.lisp
M books/centaur/meta/pseudo-rewrite-rule.lisp
M books/centaur/meta/urewrite.lisp
M books/centaur/misc/context-rw.lisp
M books/centaur/misc/defapply.lisp
M books/centaur/misc/interp-function-lookup.lisp
M books/clause-processors/ev-theoremp.lisp
M books/clause-processors/just-expand.lisp
M books/clause-processors/meta-extract-user.lisp
M books/clause-processors/witness-cp.lisp

Log Message:
-----------
Metareasoning: at long last make <eval>-theoremp a function rather than a macro


Commit: 7da450d8c28483ffb01f3eec5857424743cc5287
https://github.com/acl2/acl2/commit/7da450d8c28483ffb01f3eec5857424743cc5287
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-02-23 (Mon, 23 Feb 2026)

Changed paths:
M books/centaur/fgl/binder-rules.lisp
M books/centaur/fgl/congruence.lisp
M books/centaur/fgl/contexts.lisp
M books/centaur/fgl/interp.lisp
M books/centaur/fgl/rules.lisp
M books/centaur/gl/gl-generic-clause-proc.lisp
M books/centaur/gl/gl-generic-interp-defs.lisp
M books/centaur/gl/gl-generic-interp.lisp
M books/centaur/gl/glcp-rewrite-tables.lisp
M books/centaur/gl/rewrite-tables.lisp
M books/centaur/gl/run-gified-cp.lisp
M books/centaur/glmc/glmc-generic-proof.lisp
M books/centaur/glmc/glmc.lisp
M books/centaur/meta/congruence.lisp
M books/centaur/meta/equivalence.lisp
M books/centaur/meta/pseudo-rewrite-rule.lisp
M books/centaur/meta/urewrite.lisp
M books/centaur/misc/context-rw.lisp
M books/centaur/misc/defapply.lisp
M books/centaur/misc/interp-function-lookup.lisp
M books/clause-processors/ev-theoremp.lisp
M books/clause-processors/just-expand.lisp
M books/clause-processors/meta-extract-user.lisp
M books/clause-processors/witness-cp.lisp

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


Commit: 4c3244b554cd923ba23193d3841ba8ad37fdaa87
https://github.com/acl2/acl2/commit/4c3244b554cd923ba23193d3841ba8ad37fdaa87
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-02-25 (Wed, 25 Feb 2026)

Changed paths:
M books/centaur/fgl/congruence-rules.lisp
M books/centaur/fgl/congruence.lisp
M books/centaur/fgl/fgl-primitive-congruences.lisp

Log Message:
-----------
FGL: make identity congruences more general


Commit: 8cb9e5334ab11641815ac21218597ccd65c7d007
https://github.com/acl2/acl2/commit/8cb9e5334ab11641815ac21218597ccd65c7d007
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
A books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe] Split out print-as-term-or-dag.


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: e1d0a0a27075df29e2f4f40d1c4102a8b24dcd6a
https://github.com/acl2/acl2/commit/e1d0a0a27075df29e2f4f40d1c4102a8b24dcd6a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-02 (Mon, 02 Mar 2026)

Changed paths:
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp

Log Message:
-----------
[axe] Improve and localize implementation rules.


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


Commit: 8c74b41b232be665d13fe68b08def77ef4504109
https://github.com/acl2/acl2/commit/8c74b41b232be665d13fe68b08def77ef4504109
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
A books/projects/x86isa/machine/instructions/logical.lisp
A books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp

Log Message:
-----------
Merge commit '85ac411190522bbc64f5163eb5559b69e6184a23' into HEAD


Commit: 6816d7e63c828d90dc4b565051d3bbf1180278a3
https://github.com/acl2/acl2/commit/6816d7e63c828d90dc4b565051d3bbf1180278a3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/kestrel/axe/dag-exprs.lisp

Log Message:
-----------
[axe] Improve implementation rules.


Commit: 97c61ed56c2f5b12a4da2611d08a693a81d336a4
https://github.com/acl2/acl2/commit/97c61ed56c2f5b12a4da2611d08a693a81d336a4
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe/x86] Add warning.


Commit: d11d37f135688869d9e75c7ab16694d961366a2a
https://github.com/acl2/acl2/commit/d11d37f135688869d9e75c7ab16694d961366a2a
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/kestrel/axe/dag-exprs.lisp
A books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/dag-to-term.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
Merge commit '97c61ed56c2f5b12a4da2611d08a693a81d336a4' into HEAD


Commit: cb229f33d563776cb22c2ed429809b017358b661
https://github.com/acl2/acl2/commit/cb229f33d563776cb22c2ed429809b017358b661
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/centaur/fgl/syntax-bind.lisp
M books/centaur/fgl/trace.lisp
M books/doc/relnotes.lisp

Log Message:
-----------
Doc fixes and release notes


Commit: e6d54faae5365d6cf2b391d12620f02178a9db8b
https://github.com/acl2/acl2/commit/e6d54faae5365d6cf2b391d12620f02178a9db8b
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M README.md
M acl2-init.lisp
M all-files.txt
M books/GNUmakefile
M books/doc/more-topics.lisp
M books/doc/publications.acl2
M books/doc/relnotes.lisp
A books/kestrel/air/acl2-customization.lsp
A books/kestrel/air/cert.acl2
A books/kestrel/air/model-0/acl2-customization.lsp
A books/kestrel/air/model-0/air/acl2-customization.lsp
A books/kestrel/air/model-0/air/correctness.lisp
A books/kestrel/air/model-0/air/example.lisp
A books/kestrel/air/model-0/air/field-encoding.lisp
A books/kestrel/air/model-0/air/field.lisp
A books/kestrel/air/model-0/air/pfcs-constraints.lisp
A books/kestrel/air/model-0/air/pfcs-lifting.lisp
A books/kestrel/air/model-0/air/traces.lisp
A books/kestrel/air/model-0/cert.acl2
A books/kestrel/air/model-0/language/abstract-syntax.lisp
A books/kestrel/air/model-0/language/acl2-customization.lsp
A books/kestrel/air/model-0/language/dynamic-semantics.lisp
A books/kestrel/air/model-0/language/example.lisp
A books/kestrel/air/model-0/language/input-output-semantics.lisp
A books/kestrel/air/model-0/language/static-semantics.lisp
A books/kestrel/air/model-0/library-extensions.lisp
A books/kestrel/air/model-0/package.lsp
A books/kestrel/air/model-0/portcullis.acl2
A books/kestrel/air/model-0/portcullis.lisp
A books/kestrel/air/model-0/top.lisp
A books/kestrel/air/package.lsp
A books/kestrel/air/portcullis.acl2
A books/kestrel/air/portcullis.lisp
A books/kestrel/air/top.lisp
M books/kestrel/arm/def-inst.lisp
M books/kestrel/arm/doc.lisp
M books/kestrel/arm/encodings.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/arm/tests/simple.lisp
M books/kestrel/auto-termination/README
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
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/arm/axe-rules.lisp
M books/kestrel/axe/arm/examples/add/add.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/support.lisp
M books/kestrel/axe/arm/syntaxp-evaluator.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/axe-bind-free-evaluator-basic.lisp
M books/kestrel/axe/axe-rules.lisp
M books/kestrel/axe/axe-syntax-functions-bv.lisp
M books/kestrel/axe/axe-syntax-functions.lisp
M books/kestrel/axe/axe-syntaxp-evaluator-basic.lisp
M books/kestrel/axe/bounded-dag-exprs.lisp
M books/kestrel/axe/bounded-darg-listp.lisp
M books/kestrel/axe/bv-rules-axe.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
A books/kestrel/axe/dag-printing.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/imported-symbols.lisp
M books/kestrel/axe/make-axe-bind-free-evaluator.lisp
M books/kestrel/axe/make-axe-syntaxp-evaluator-tests.lisp
M books/kestrel/axe/make-axe-syntaxp-evaluator.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/r1cs/axe-syntaxp-evaluator-r1cs.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/x86/bind-free-evaluator-x86.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp
M books/kestrel/bv/bvnot.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/logext.lisp
M books/kestrel/bv/overflow-and-underflow.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/sbvlt.lisp
A books/kestrel/c/language/decimal-0-to-octal-0.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/syntax/.sys/preproces...@useless-runes.lsp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/concrete-syntax.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/all.abnf
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-files.lisp
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/preservable-inclusions.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/printing.lisp
M books/kestrel/c/syntax/tests/.gitignore
M books/kestrel/c/syntax/tests/preproc-example1/.gitignore
M books/kestrel/c/syntax/tests/preproc-example2/.gitignore
M books/kestrel/c/syntax/tests/preproc-example3/.gitignore
M books/kestrel/c/syntax/tests/preproc-example4/.gitignore
M books/kestrel/c/syntax/tests/preproc-example5/.gitignore
M books/kestrel/c/syntax/tests/preproc-example6/.gitignore
A books/kestrel/c/syntax/tests/preproc-example7/.gitignore
A books/kestrel/c/syntax/tests/preproc-example7/f.c
A books/kestrel/c/syntax/tests/preproc-example7/g.c
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/kestrel/c/syntax/top.lisp
A books/kestrel/c/syntax/unicode-characters.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/transformation/utilities/free-vars.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/crypto/primes/koala-bear.lisp
M books/kestrel/ethereum/rlp/top.lisp
M books/kestrel/fty/defmake-self.lisp
M books/kestrel/risc-v/executable/execution-executable.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
M books/kestrel/utilities/defstobj-plus-tests.lisp
M books/kestrel/utilities/ensure-rules-known.lisp
M books/misc/check-acl2-exports.lisp
M books/projects/abnf/parsing-tools/defdefparse.lisp
M books/projects/acl2-in-hol/tests/inputs/PKGS.lsp
M books/projects/acl2-in-hol/tests/inputs/PKGS.sml
M books/projects/aleo/leo/early-version/definition/concrete-syntax.lisp
M books/projects/aleo/leo/early-version/definition/format-strings.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-and.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-all.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-true.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-if.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-nand.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-nor.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-not.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-or.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-xor.lisp
M books/projects/aleo/vm/circuits/pfcs/field-add.lisp
M books/projects/aleo/vm/circuits/pfcs/field-assert-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-assert-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-checked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-flagged.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-unchecked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-double.lisp
M books/projects/aleo/vm/circuits/pfcs/field-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-if.lisp
M books/projects/aleo/vm/circuits/pfcs/field-inv-checked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-inv-flagged.lisp
M books/projects/aleo/vm/circuits/pfcs/field-mul.lisp
M books/projects/aleo/vm/circuits/pfcs/field-neg.lisp
M books/projects/aleo/vm/circuits/pfcs/field-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-square.lisp
M books/projects/aleo/vm/circuits/pfcs/field-sub.lisp
M books/projects/aleo/vm/circuits/top.lisp
M books/projects/aleo/vm/language/grammar.lisp
M books/projects/hol-in-acl2/acl2/hol.lisp
M books/projects/hol-in-acl2/acl2/hpp-set.lisp
M books/projects/hol-in-acl2/acl2/lemmas.lisp
R books/projects/hol-in-acl2/acl2/type-match.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/pfcs/.sys/le...@useless-runes.lsp
M books/projects/pfcs/.sys/par...@useless-runes.lsp
M books/projects/pfcs/.sys/syntax-ab...@useless-runes.lsp
M books/projects/pfcs/abstract-syntax-operations.lisp
M books/projects/pfcs/abstract-syntax-trees.lisp
M books/projects/pfcs/abstract-syntax.lisp
M books/projects/pfcs/convenience-constructors.lisp
M books/projects/pfcs/grammar.lisp
M books/projects/pfcs/lexer.lisp
M books/projects/pfcs/parser.lisp
M books/projects/pfcs/syntax-abstraction.lisp
M books/projects/pfcs/tokenizer.lisp
M books/projects/pfcs/well-formedness.lisp
M books/projects/python/embedding/types.lisp
M books/projects/set-theory/foldr.lisp
M books/projects/set-theory/ordinals.lisp
M books/projects/set-theory/restrict.lisp
M books/projects/set-theory/set-algebra.lisp
A books/projects/set-theory/skolem.lisp
M books/projects/set-theory/top.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
A books/projects/x86isa/machine/instructions/logical.lisp
A books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
A books/projects/x86isa/machine/instructions/pmadd.lisp
A books/projects/x86isa/machine/instructions/pmul.lisp
A books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/std/obags/core.lisp
M books/std/obags/tests.lisp
M books/system/apply/apply-prim.lisp
M books/system/check-system-guards.lisp
M books/system/doc/acl2-doc.lisp
M books/system/pseudo-good-worldp.lisp
M books/system/to-do.txt
M books/workshops/2025/kwan/rv-state.lisp
M books/workshops/2025/manjrekar/examples/imul64/imul64-proof.lisp
M books/workshops/2025/manjrekar/examples/imul8/imul8-proof.lisp
M defpkgs.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp
M other-events.lisp

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


Commit: fd511c5ea9fd3c342846e280a0f8fc58bd5ad0c8
https://github.com/acl2/acl2/commit/fd511c5ea9fd3c342846e280a0f8fc58bd5ad0c8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/projects/x86isa/machine/syscalls.lisp

Log Message:
-----------
[X86ISA] Fix X86ISA_EXEC=t build.

Also fix a comment.


Commit: 84997a36af3965c9a6e11ef75fb31e199071cff2
https://github.com/acl2/acl2/commit/84997a36af3965c9a6e11ef75fb31e199071cff2
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
doc fix


Commit: a2ae43c81c9e349928d182571228492a1ae80045
https://github.com/acl2/acl2/commit/a2ae43c81c9e349928d182571228492a1ae80045
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/projects/x86isa/machine/syscalls.lisp

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


Compare: https://github.com/acl2/acl2/compare/85ac41119052...a2ae43c81c9e

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

[solswords]

Branch: refs/heads/master

Commit: 84997a36af3965c9a6e11ef75fb31e199071cff2
https://github.com/acl2/acl2/commit/84997a36af3965c9a6e11ef75fb31e199071cff2
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/doc/relnotes.lisp

Log Message:
-----------
doc fix


Commit: a2ae43c81c9e349928d182571228492a1ae80045
https://github.com/acl2/acl2/commit/a2ae43c81c9e349928d182571228492a1ae80045
Author: Sol Swords <sol.s...@arm.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/projects/x86isa/machine/syscalls.lisp

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

Commit: 57d2e3a71f8a8a6a39a642d6769ec91e83b81c59
https://github.com/acl2/acl2/commit/57d2e3a71f8a8a6a39a642d6769ec91e83b81c59

Author: Sol Swords <sol.s...@arm.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:

M books/clause-processors/induction.lisp
M books/clause-processors/replace-equalities.lisp

Log Message:
-----------
more ev-theoremp fallout


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

Author: Sol Swords <sol.s...@arm.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:

M books/kestrel/axe/x86/rule-lists.acl2
M books/kestrel/axe/x86/tester-rules.acl2
M books/kestrel/axe/x86/x86-rules.acl2
M books/kestrel/x86/assumptions-new.acl2
M books/kestrel/x86/assumptions32.acl2
M books/kestrel/x86/assumptions64.acl2
M books/kestrel/x86/bytes-loadedp.acl2
M books/kestrel/x86/canonical.acl2
M books/kestrel/x86/conditions.acl2
M books/kestrel/x86/floats.acl2
M books/kestrel/x86/if-lowering.acl2
M books/kestrel/x86/linear-memory.acl2
M books/kestrel/x86/memory32.acl2
M books/kestrel/x86/read-and-write.acl2
M books/kestrel/x86/read-and-write2.acl2
M books/kestrel/x86/read-bytes-and-write-bytes.acl2
M books/kestrel/x86/read-over-write-rules.acl2
M books/kestrel/x86/read-over-write-rules32.acl2
M books/kestrel/x86/read-over-write-rules64.acl2
M books/kestrel/x86/register-readers-and-writers32.acl2
M books/kestrel/x86/register-readers-and-writers64.acl2
M books/kestrel/x86/rflags2.acl2
M books/kestrel/x86/run-until-return.acl2
M books/kestrel/x86/run-until-return2.acl2
M books/kestrel/x86/run-until-return3.acl2
M books/kestrel/x86/run-until-return4.acl2
M books/kestrel/x86/support-x86.acl2
M books/kestrel/x86/support.acl2
M books/kestrel/x86/support2.acl2
M books/kestrel/x86/support32.acl2
M books/kestrel/x86/tools/lifter-support.acl2
M books/kestrel/x86/tools/top.acl2
M books/kestrel/x86/tools/unroll-x86-code-old.acl2
M books/kestrel/x86/top.acl2
M books/kestrel/x86/write-over-write-rules.acl2
M books/kestrel/x86/write-over-write-rules32.acl2
M books/kestrel/x86/write-over-write-rules64.acl2
M books/kestrel/x86/zmm.acl2

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


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

Author: Sol Swords <sol.s...@arm.com>
Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:
M books/centaur/fgl/syntax-bind.lisp

Log Message:
-----------
one more doc fix


Compare: https://github.com/acl2/acl2/compare/5d759a50c4b5...c3eee0b1e5fa

[solswords]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

Commit: b9c4908d3c7c61e3ca669c33d0fed02aea22cfb1
https://github.com/acl2/acl2/commit/b9c4908d3c7c61e3ca669c33d0fed02aea22cfb1
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp

Log Message:
-----------
[X86ISA] Add MMX packed shift instructions.


Commit: 4f78af8932fda7682f26eef606274897760f8e2e
https://github.com/acl2/acl2/commit/4f78af8932fda7682f26eef606274897760f8e2e
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/instructions/move-mmx.lisp

Log Message:
-----------
[X86ISA] Add forgotten MMX FP updates.


Commit: 2cbe4a8bbcbd1be74a87db1fe14d967f4bb7c3cf
https://github.com/acl2/acl2/commit/2cbe4a8bbcbd1be74a87db1fe14d967f4bb7c3cf
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/instructions/punpck.lisp

Log Message:
-----------
[X86ISA] Stylistic consistency (in preparation for extensions).

Commit: bb9f8e801e60efa43548e5b54e4c22dab7452847
https://github.com/acl2/acl2/commit/bb9f8e801e60efa43548e5b54e4c22dab7452847
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp

Log Message:
-----------
[X86ISA] Add PUNPCKLBW/WD/DQ (MMX variants).


Commit: c47df101ef57d6ed449f3247092022921b640f67
https://github.com/acl2/acl2/commit/c47df101ef57d6ed449f3247092022921b640f67
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp

Log Message:
-----------
[X86ISA] Add PUNPCKHBW/WD/DQ (MMX variants).


Commit: 6e686a9de6e218f55eea39555b27ba1111e4893c
https://github.com/acl2/acl2/commit/6e686a9de6e218f55eea39555b27ba1111e4893c
Author: Alessandro Coglio <em...@alessandrocoglio.info>

M books/projects/x86isa/machine/syscalls.lisp

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

Merge.


Commit: 3b4e78e14baf4edfe2243b186aaed7f5c06e9c6a
https://github.com/acl2/acl2/commit/3b4e78e14baf4edfe2243b186aaed7f5c06e9c6a
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
A books/projects/x86isa/machine/instructions/pack.lisp
M books/projects/x86isa/machine/instructions/top.lisp

Log Message:
-----------
[X86ISA] Refactor some code.

Put the PACKUSWB instruction into a new file, for the family of PACK*
instructions.


Commit: 4504aa5816fd0e17342528bbd2653c7d57f868cf
https://github.com/acl2/acl2/commit/4504aa5816fd0e17342528bbd2653c7d57f868cf

Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:

M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/syscalls.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.lisp

Log Message:
-----------
Merge commit '8b28e0802ddc57f10a057d8e7a3651d559128f04' into HEAD


Commit: 6058c11300781c743c50b40560d0cef8142218f7
https://github.com/acl2/acl2/commit/6058c11300781c743c50b40560d0cef8142218f7
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2026-03-03 (Tue, 03 Mar 2026)

Changed paths:

M books/centaur/fgl/annotation.lisp
M books/centaur/fgl/binder-rules.lisp
M books/centaur/fgl/congruence-rules.lisp
M books/centaur/fgl/congruence.lisp
M books/centaur/fgl/constraint-db.lisp
M books/centaur/fgl/contexts.lisp
M books/centaur/fgl/fgl-object.lisp
M books/centaur/fgl/fgl-primitive-congruences.lisp
M books/centaur/fgl/interp.lisp
M books/centaur/fgl/rules.lisp
M books/centaur/fgl/syntax-bind.lisp
M books/centaur/fgl/trace.lisp

M books/centaur/gl/gl-generic-clause-proc.lisp
M books/centaur/gl/gl-generic-interp-defs.lisp
M books/centaur/gl/gl-generic-interp.lisp
M books/centaur/gl/glcp-rewrite-tables.lisp
M books/centaur/gl/rewrite-tables.lisp
M books/centaur/gl/run-gified-cp.lisp
M books/centaur/glmc/glmc-generic-proof.lisp
M books/centaur/glmc/glmc.lisp

M books/centaur/meta/bindinglist.lisp
M books/centaur/meta/congruence.lisp
M books/centaur/meta/equivalence.lisp
A books/centaur/meta/fnsymlist.lisp
M books/centaur/meta/package.lsp
M books/centaur/meta/pseudo-rewrite-rule.lisp

M books/centaur/meta/subst-vars.lisp
M books/centaur/meta/subst.lisp
M books/centaur/meta/term-vars.lisp

M books/centaur/meta/urewrite.lisp
M books/centaur/misc/context-rw.lisp
M books/centaur/misc/defapply.lisp
M books/centaur/misc/interp-function-lookup.lisp
M books/clause-processors/ev-theoremp.lisp

M books/clause-processors/induction.lisp
M books/clause-processors/just-expand.lisp
M books/clause-processors/meta-extract-user.lisp
M books/clause-processors/replace-equalities.lisp
M books/clause-processors/witness-cp.lisp
M books/doc/relnotes.lisp
M books/projects/x86isa/machine/environment.lisp
M books/projects/x86isa/machine/evex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/instructions/add-spec.lisp
M books/projects/x86isa/machine/instructions/and-spec.lisp
M books/projects/x86isa/machine/instructions/arith-and-logic.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/cache.lisp
M books/projects/x86isa/machine/instructions/cert.acl2
M books/projects/x86isa/machine/instructions/conditional.lisp
M books/projects/x86isa/machine/instructions/cpuid.lisp
M books/projects/x86isa/machine/instructions/divide-spec.lisp
M books/projects/x86isa/machine/instructions/divide.lisp
M books/projects/x86isa/machine/instructions/endbranch.lisp
M books/projects/x86isa/machine/instructions/exchange.lisp
M books/projects/x86isa/machine/instructions/flags.lisp
M books/projects/x86isa/machine/instructions/fp/arithmetic.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/cert.acl2
M books/projects/x86isa/machine/instructions/fp/convert.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/fp/mxcsr.lisp
M books/projects/x86isa/machine/instructions/fp/non-arith.lisp
M books/projects/x86isa/machine/instructions/fp/shuffle-and-unpack.lisp
M books/projects/x86isa/machine/instructions/fp/simd-integer.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp
M books/projects/x86isa/machine/instructions/halt.lisp
M books/projects/x86isa/machine/instructions/interrupts.lisp
M books/projects/x86isa/machine/instructions/jump-and-loop.lisp
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/move-mmx.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/instructions/move.lisp
M books/projects/x86isa/machine/instructions/msrs.lisp
M books/projects/x86isa/machine/instructions/multiply-spec.lisp
M books/projects/x86isa/machine/instructions/multiply.lisp
M books/projects/x86isa/machine/instructions/or-spec.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/pshuf.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/punpck.lisp
M books/projects/x86isa/machine/instructions/push-and-pop.lisp
M books/projects/x86isa/machine/instructions/rand.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
M books/projects/x86isa/machine/instructions/segmentation.lisp
M books/projects/x86isa/machine/instructions/shifts-spec.lisp
M books/projects/x86isa/machine/instructions/signextend.lisp
M books/projects/x86isa/machine/instructions/string.lisp
M books/projects/x86isa/machine/instructions/sub-spec.lisp
M books/projects/x86isa/machine/instructions/subroutine.lisp
M books/projects/x86isa/machine/instructions/syscall.lisp
M books/projects/x86isa/machine/instructions/time.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/projects/x86isa/machine/instructions/x87.lisp
M books/projects/x86isa/machine/instructions/xor-spec.lisp
M books/projects/x86isa/machine/linear-memory.lisp
M books/projects/x86isa/machine/modes.lisp
M books/projects/x86isa/machine/new-decode.lisp
M books/projects/x86isa/machine/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/paging.lisp
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/syscalls.lisp
M books/projects/x86isa/machine/three-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/two-byte-opcodes-dispatch.lisp
M books/projects/x86isa/machine/vex-opcodes-dispatch.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/proofs/cert.acl2
M books/projects/x86isa/proofs/codewalker-examples/cert.acl2
M books/projects/x86isa/proofs/dataCopy/cert.acl2
M books/projects/x86isa/proofs/dissertation-examples/cert.acl2
M books/projects/x86isa/proofs/factorial/cert.acl2
M books/projects/x86isa/proofs/popcount/cert.acl2
M books/projects/x86isa/proofs/powOfTwo/cert.acl2
M books/projects/x86isa/proofs/utilities/app-view/cert.acl2
M books/projects/x86isa/proofs/utilities/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/cert.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/paging-basics.acl2
M books/projects/x86isa/proofs/utilities/sys-view/paging/top.acl2
M books/projects/x86isa/proofs/wordCount/cert.acl2
M books/projects/x86isa/proofs/wordCount/wc-addr-byte.acl2
M books/projects/x86isa/proofs/zeroCopy/marking-view/cert.acl2
M books/projects/x86isa/proofs/zeroCopy/non-marking-view/cert.acl2
M books/projects/x86isa/tools/execution/init-page-tables.lisp
M books/projects/x86isa/tools/execution/init-state.lisp
M books/projects/x86isa/tools/execution/instrument/top.lisp

Log Message:
-----------
[X86ISA] Merge and resolve conflicts.


Compare: https://github.com/acl2/acl2/compare/8b28e0802ddc...6058c1130078