[acl2/acl2] 73c11c: [X86ISA] Remove unnecessary :ttags.

[Eric W. Smith]

Branch: refs/heads/x86isa-ttags
Home: https://github.com/acl2/acl2
Commit: 73c11c7416fd42229824a44e3b5b8569b8bd3813
https://github.com/acl2/acl2/commit/73c11c7416fd42229824a44e3b5b8569b8bd3813
Author: Eric Smith <ews...@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/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/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.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/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] Remove unnecessary :ttags.

Remove many unnecessary items in the :ttags arguments given to include-book and certify-book. Some of the remaining ones are only needed when X86ISA_EXEC=t.


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

Changed paths:
M books/projects/x86isa/machine/environment.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/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/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/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/pio.lisp
M books/projects/x86isa/machine/instructions/pmadd.lisp
M books/projects/x86isa/machine/instructions/pmul.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.lisp
M books/projects/x86isa/machine/segmentation.lisp
M books/projects/x86isa/machine/x86.lisp
M books/projects/x86isa/tools/execution/init-state.lisp

Log Message:
-----------
[X86ISA] Remove empty :ttags args.

Since these include-book events worked with :ttags (), no ttags are actually involved, so we can drop the :ttags arguments.


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

Changed paths:
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/syscalls.lisp

Log Message:
-----------
[X86ISA] Drop more unneeded :ttags.


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

Changed paths:
M books/projects/x86isa/machine/instructions/logical.lisp
M books/projects/x86isa/machine/instructions/pcmp.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/syscalls.lisp

Log Message:
-----------
[X86ISA] Remove newly empty :ttags args.


Compare: https://github.com/acl2/acl2/compare/73c11c7416fd%5E...b41dd570710d

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

[Eric W. Smith]

Branch: refs/heads/testing-kestrel

Commit: 8b28e0802ddc57f10a057d8e7a3651d559128f04
https://github.com/acl2/acl2/commit/8b28e0802ddc57f10a057d8e7a3651d559128f04
Author: Eric W. Smith <48038799+eri...@users.noreply.github.com>

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/syscalls.lisp

Merge pull request #1910 from acl2/x86isa-ttags

Remove many unneeded ttags from x86isa books


Compare: https://github.com/acl2/acl2/compare/5d759a50c4b5...8b28e0802ddc

[acl2buildserver]

Branch: refs/heads/master

Commit: 4504aa5816fd0e17342528bbd2653c7d57f868cf
https://github.com/acl2/acl2/commit/4504aa5816fd0e17342528bbd2653c7d57f868cf
Author: ACL2 Build Server <acl2bui...@gmail.com>

Merge commit '8b28e0802ddc57f10a057d8e7a3651d559128f04' into HEAD


Compare: https://github.com/acl2/acl2/compare/c3eee0b1e5fa...4504aa5816fd

[acl2buildserver]

Branch: refs/heads/testing