[acl2/acl2] dc5394: [X86ISA] Improve some code indentation.

0 views
Skip to first unread message

Alessandro Coglio

unread,
May 6, 2026, 2:27:58 PM (2 days ago) May 6
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: dc53949d71a5c255309271464c0d916c31b5a52c
https://github.com/acl2/acl2/commit/dc53949d71a5c255309271464c0d916c31b5a52c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Improve some code indentation.

This was excessively indented.


Commit: 64809bf0bbf3190d475e7c7915a58e2a13345d21
https://github.com/acl2/acl2/commit/64809bf0bbf3190d475e7c7915a58e2a13345d21
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/projects/x86isa/utils/fp-structures.lisp

Log Message:
-----------
[X86ISA] Avoid boldface `:short`.


Commit: 248c5efda4fdca7bf24b00049368b017a9c6a701
https://github.com/acl2/acl2/commit/248c5efda4fdca7bf24b00049368b017a9c6a701
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/projects/x86isa/utils/fp-structures.lisp

Log Message:
-----------
[X86ISA] Update some references.


Commit: ff22975f08bf441d74d269bd888b4c7bba5e0ab5
https://github.com/acl2/acl2/commit/ff22975f08bf441d74d269bd888b4c7bba5e0ab5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Expand some doc.


Commit: 751f2d40012eaf0416617ee5bf954f560ecc58dc
https://github.com/acl2/acl2/commit/751f2d40012eaf0416617ee5bf954f560ecc58dc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Improve doc and code clarity.


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

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

Log Message:
-----------
[doc] Drop some incorrect links.


Commit: 182eccea0dead425cb42849851481e79c8442063
https://github.com/acl2/acl2/commit/182eccea0dead425cb42849851481e79c8442063
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/c/language/decimal-0-to-octal-0.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/rename.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/fty/deffold-map-doc.lisp
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/dynamic-semantics.lisp
M books/kestrel/remora/grammar.abnf
A books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/printer.lisp
M books/kestrel/remora/static-semantics.lisp
M books/kestrel/remora/syntax-abstraction.lisp
M books/kestrel/remora/top.lisp
A books/kestrel/remora/values.lisp
M books/kestrel/x86/package.lsp

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


Commit: 6f90216c4225aa05b7fb9ada98bec61ce01825aa
https://github.com/acl2/acl2/commit/6f90216c4225aa05b7fb9ada98bec61ce01825aa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Fix and improve CMPS/CMPSB/CMPSW/CMPSD/CMPSQ.

The treatment of repetition prefixes was incorrect.

Add some documentation.

Improve code clarity and consistency.


Commit: 7a8f2ca68e4785dd7fe2b2831b115a4ee349bdc2
https://github.com/acl2/acl2/commit/7a8f2ca68e4785dd7fe2b2831b115a4ee349bdc2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Reorder items.


Commit: 3b24a5e318e704ab48530dc862da69b92a010059
https://github.com/acl2/acl2/commit/3b24a5e318e704ab48530dc862da69b92a010059
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/projects/x86isa/machine/decoding-and-spec-utils.lisp

Log Message:
-----------
[X86ISA] Add a theorem.


Commit: 241bac177676872bc17ae76215f9aa18498c05d3
https://github.com/acl2/acl2/commit/241bac177676872bc17ae76215f9aa18498c05d3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Speed up some proofs significantly.


Commit: 6706250e5fa8a56c190f10e8c5a5d12e14972819
https://github.com/acl2/acl2/commit/6706250e5fa8a56c190f10e8c5a5d12e14972819
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Add SCAS/SCASB/SCASW/SCASD/SCASQ.


Commit: e700b4e95d78e32d78338a329653c6d0f57a5381
https://github.com/acl2/acl2/commit/e700b4e95d78e32d78338a329653c6d0f57a5381
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Improve code and doc of STOS/STOSB/STOSW/STOSD/STOSQ.


Commit: df3ae5e511d514f6262aca3d709a021081e78c2c
https://github.com/acl2/acl2/commit/df3ae5e511d514f6262aca3d709a021081e78c2c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Improve some variable names.

In CMPS, there is no source and destination, but rather source 1 and source 2.


Commit: bc2e9c58ac4622fbce851904a02f124723e6a068
https://github.com/acl2/acl2/commit/bc2e9c58ac4622fbce851904a02f124723e6a068
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-05 (Tue, 05 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Fix swapped operands in CMPS.

This is clear from the Intel pseudocode and the prose in the Intel specification
of the instruction. It affects some of the flags. It is a bit counterintuitive
because of the source/destination connotation of rSI and rDI, given that CMP
instead compares by performing of subtraction of source from destination. In
CMPS, instead, the subtraction is of the rDI operand from the rSI operand.


Commit: 48f3f0d8bdb89893174ec46b435109125d9f4a3e
https://github.com/acl2/acl2/commit/48f3f0d8bdb89893174ec46b435109125d9f4a3e
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/encoding-prefixes.abnf
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/identifier-lists.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c17.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c23.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives.abnf
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce.lisp

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


Commit: 779e9e92772bd38d5ebaa7d0d9ef4d8f8a9cebf7
https://github.com/acl2/acl2/commit/779e9e92772bd38d5ebaa7d0d9ef4d8f8a9cebf7
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/system/doc/developers-guide.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Updated :DOC developers-guide-examples with example of stobj hash-table keys. Added mention of a private maintenance repo in :DOC developers-guide-releases. Synched doc.lisp etc.


Commit: b7eb843dbef4bd6be6b25e69a0421027cf1ae219
https://github.com/acl2/acl2/commit/b7eb843dbef4bd6be6b25e69a0421027cf1ae219
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Add LODS(B/W/D/Q).


Commit: 1d343c30d7960aa477d29537d4ccb307752e3e82
https://github.com/acl2/acl2/commit/1d343c30d7960aa477d29537d4ccb307752e3e82
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Reorder some MOVS(B/W/D/Q) code for clarity/readability.


Commit: 49fec0ea66ccd76a46c7530671f3659d3c9ee1cb
https://github.com/acl2/acl2/commit/49fec0ea66ccd76a46c7530671f3659d3c9ee1cb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Reorder some CMPS(B/W/D/Q) code for clarity/readability.


Commit: aad379f5c7c3f940a106ded242618cc11c23ffcc
https://github.com/acl2/acl2/commit/aad379f5c7c3f940a106ded242618cc11c23ffcc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Reorder some SCAS(B/W/D/Q) code for clarity/readability.


Commit: 45cffe55da0916aa36f805af36517a8d8262687b
https://github.com/acl2/acl2/commit/45cffe55da0916aa36f805af36517a8d8262687b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Reorder some STOS(B/W/D/Q) code for clarity/readability.


Commit: 2c81826d8afded5dc10e62164f1e127fcce526b8
https://github.com/acl2/acl2/commit/2c81826d8afded5dc10e62164f1e127fcce526b8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/string.lisp

Log Message:
-----------
[X86ISA] Reorder some LODS(B/W/D/Q) code for clarity/readability.


Commit: 7ffa9c4d7610b500f5974ace776997a7d156da87
https://github.com/acl2/acl2/commit/7ffa9c4d7610b500f5974ace776997a7d156da87
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/encoding-prefixes.abnf
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/identifier-lists.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c17.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives-c23.abnf
A books/kestrel/c/syntax/grammar/preprocessing-directives.abnf
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce.lisp
M books/system/doc/acl2-doc.lisp
M books/system/doc/developers-guide.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

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


Commit: 05c377b06c348d97648fdf498bce2ac0ba9bcba5
https://github.com/acl2/acl2/commit/05c377b06c348d97648fdf498bce2ac0ba9bcba5
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
[doc] Add link.


Commit: f67deb2d663edce0eb8f2efb4b76755f5e1f3af9
https://github.com/acl2/acl2/commit/f67deb2d663edce0eb8f2efb4b76755f5e1f3af9
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
Merge commit '05c377b06c348d97648fdf498bce2ac0ba9bcba5' into HEAD


Commit: 3b230b3cfd0042f6b44b3c025b7ce2dda82c33fb
https://github.com/acl2/acl2/commit/3b230b3cfd0042f6b44b3c025b7ce2dda82c33fb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/doc/practices.lisp

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


Compare: https://github.com/acl2/acl2/compare/c656640af155...3b230b3cfd00

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

Alessandro Coglio

unread,
May 6, 2026, 4:05:26 PM (2 days ago) May 6
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: 3b230b3cfd0042f6b44b3c025b7ce2dda82c33fb
https://github.com/acl2/acl2/commit/3b230b3cfd0042f6b44b3c025b7ce2dda82c33fb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/doc/practices.lisp

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


Compare: https://github.com/acl2/acl2/compare/f67deb2d663e...3b230b3cfd00

Alessandro Coglio

unread,
May 6, 2026, 4:06:38 PM (2 days ago) May 6
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
May 6, 2026, 4:30:05 PM (2 days ago) May 6
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Commit: 779e9e92772bd38d5ebaa7d0d9ef4d8f8a9cebf7
https://github.com/acl2/acl2/commit/779e9e92772bd38d5ebaa7d0d9ef4d8f8a9cebf7
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/system/doc/developers-guide.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Updated :DOC developers-guide-examples with example of stobj hash-table keys. Added mention of a private maintenance repo in :DOC developers-guide-releases. Synched doc.lisp etc.


Commit: f67deb2d663edce0eb8f2efb4b76755f5e1f3af9
https://github.com/acl2/acl2/commit/f67deb2d663edce0eb8f2efb4b76755f5e1f3af9
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/doc/practices.lisp

Log Message:
-----------
Merge commit '05c377b06c348d97648fdf498bce2ac0ba9bcba5' into HEAD


Commit: 3b230b3cfd0042f6b44b3c025b7ce2dda82c33fb
https://github.com/acl2/acl2/commit/3b230b3cfd0042f6b44b3c025b7ce2dda82c33fb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-06 (Wed, 06 May 2026)

Changed paths:
M books/doc/practices.lisp

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


Compare: https://github.com/acl2/acl2/compare/05c377b06c34...3b230b3cfd00
Reply all
Reply to author
Forward
0 new messages