[acl2/acl2] cb2364: [risc-v] Reorder args of read-bytes.

Eric W. Smith

unread,

Sep 22, 2025, 6:39:11 PM (3 days ago) Sep 22

to acl2-...@googlegroups.com

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: cb2364de8ce09f51375cc39a0faae1ba5e9670cd
https://github.com/acl2/acl2/commit/cb2364de8ce09f51375cc39a0faae1ba5e9670cd
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-20 (Sat, 20 Sep 2025)

Changed paths:
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/unroll.lisp

Log Message:
-----------
[risc-v] Reorder args of read-bytes.

Put the length arg first, like we do for other operations (it is often a small constant).

Commit: ce6aa62778deda868d0421a65a163ce7e96e76e0
https://github.com/acl2/acl2/commit/ce6aa62778deda868d0421a65a163ce7e96e76e0
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-21 (Sun, 21 Sep 2025)

Changed paths:
A books/kestrel/c/syntax/lexer.lisp
A books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
A books/kestrel/c/syntax/reader.lisp
A books/kestrel/c/syntax/tests/lexer.lisp
A books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/parser.lisp
A books/kestrel/c/syntax/tests/reader.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/validation-information.lisp
A books/kestrel/c/syntax/validation.lisp
M books/kestrel/c/syntax/validator.lisp

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

Commit: 91980452a648405f516ccb59731c1be4499209d7
https://github.com/acl2/acl2/commit/91980452a648405f516ccb59731c1be4499209d7
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-21 (Sun, 21 Sep 2025)

Changed paths:
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions64.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-bytes-and-write-bytes.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/zmm.lisp

Log Message:
-----------
[x86] Reorder args of read-bytes.

Put the length arg first, like we do for other operations (it is often a small constant).

Commit: eccf065335462eda39313d27c29160d7c32e775a
https://github.com/acl2/acl2/commit/eccf065335462eda39313d27c29160d7c32e775a
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-21 (Sun, 21 Sep 2025)

Changed paths:
M books/kestrel/x86/read-bytes-and-write-bytes.lisp

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

Commit: da7e7524e4e8608918ebe49c8c08d6189441b2b3
https://github.com/acl2/acl2/commit/da7e7524e4e8608918ebe49c8c08d6189441b2b3
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/merge-nodes-into-dag-array.lisp
M books/kestrel/axe/risc-v/run-until-return.lisp
M books/kestrel/axe/utilities.lisp

Log Message:
-----------
[axe] Tweaks.

Commit: 08c2859498c9a616bb18df2a39ac8529ea0f518b
https://github.com/acl2/acl2/commit/08c2859498c9a616bb18df2a39ac8529ea0f518b
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/apt/schemalg-doc.lisp

Log Message:
-----------
[APT] Add missing space in doc.

Commit: ab1e22f863544cd34861807f1e5d0073355a6647
https://github.com/acl2/acl2/commit/ab1e22f863544cd34861807f1e5d0073355a6647
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/bv-lists/bv-array-conversions2.lisp

Log Message:
-----------
[bv-lists] Tweak.

Commit: effb7ebee3cfa6191134a5a043e9711d8922c3de
https://github.com/acl2/acl2/commit/effb7ebee3cfa6191134a5a043e9711d8922c3de
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/xml/xml-parser.lisp

Log Message:
-----------
[xml] Slightly improve xml parser.

Get lemma from library. Avoid a different include.

Commit: 926856f533c99375c94f5a401766f9e461b39179
https://github.com/acl2/acl2/commit/926856f533c99375c94f5a401766f9e461b39179
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/xml/xml-parser.lisp

Log Message:
-----------
[xml] Work on termination and guards.

Commit: b81dce91ce43680f6010d3fbaf9d57fddde839e7
https://github.com/acl2/acl2/commit/b81dce91ce43680f6010d3fbaf9d57fddde839e7
Author: Eric Smith <ews...@gmail.com>
Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
A books/kestrel/xml/build-book-for-xml-file.lisp
M books/kestrel/xml/xml-parser.lisp

Log Message:
-----------
[xml] Split out build-book-for-xml-file.

Compare: https://github.com/acl2/acl2/compare/6ee695d0f4e8...b81dce91ce43

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

acl2buildserver

unread,

Sep 22, 2025, 9:33:11 PM (3 days ago) Sep 22

to acl2-...@googlegroups.com

Branch: refs/heads/master

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

Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/apt/schemalg-doc.lisp

M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/merge-nodes-into-dag-array.lisp

M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/run-until-return.lisp
M books/kestrel/axe/risc-v/unroll.lisp
M books/kestrel/axe/utilities.lisp
M books/kestrel/bv-lists/bv-array-conversions2.lisp

M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions64.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-bytes-and-write-bytes.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/zmm.lisp

A books/kestrel/xml/build-book-for-xml-file.lisp
M books/kestrel/xml/xml-parser.lisp

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

Merge.

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

Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:
M books/kestrel/apt/schemalg-doc.lisp

M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/merge-nodes-into-dag-array.lisp

M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/risc-v/run-until-return.lisp
M books/kestrel/axe/risc-v/unroll.lisp
M books/kestrel/axe/utilities.lisp
M books/kestrel/bv-lists/bv-array-conversions2.lisp

M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions64.lisp
M books/kestrel/x86/read-and-write2.lisp
M books/kestrel/x86/read-bytes-and-write-bytes.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/zmm.lisp

A books/kestrel/xml/build-book-for-xml-file.lisp
M books/kestrel/xml/xml-parser.lisp

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

Merge commit '4aeac394cf784a1ccc1e3af7393fb7b70bfad79d' into HEAD

Compare: https://github.com/acl2/acl2/compare/45c9f854b72a...271ae997abda

acl2buildserver

unread,

Sep 22, 2025, 9:33:38 PM (3 days ago) Sep 22

to acl2-...@googlegroups.com

Branch: refs/heads/testing

Alessandro Coglio

unread,

Sep 22, 2025, 11:23:28 PM (3 days ago) Sep 22

to acl2-...@googlegroups.com

Branch: refs/heads/testing-user-01

Commit: fa403f852a82c7431c18bd376e66b682c56cc87b
https://github.com/acl2/acl2/commit/fa403f852a82c7431c18bd376e66b682c56cc87b
Author: David Taylor <jdavid...@outlook.com>

Date: 2025-09-21 (Sun, 21 Sep 2025)

Changed paths:

M books/system/doc/acl2-doc.lisp

Log Message:
-----------
Add LIST to TYPE-SPEC doc

Commit: c8695786778ecb09e156269814143ed8ec5ce6ec
https://github.com/acl2/acl2/commit/c8695786778ecb09e156269814143ed8ec5ce6ec
Author: David Taylor <jdavid...@outlook.com>

Date: 2025-09-21 (Sun, 21 Sep 2025)

Changed paths:

M books/projects/codewalker/basic-demo.lsp

Log Message:
-----------
Update Codewalker basic demo for filename adjustments

Commit: 14d7870960f0df892da4882c4f228d383b5dc8c5
https://github.com/acl2/acl2/commit/14d7870960f0df892da4882c4f228d383b5dc8c5
Author: MattKaufmann <kauf...@cs.utexas.edu>

Date: 2025-09-21 (Sun, 21 Sep 2025)

Changed paths:

M books/system/doc/acl2-doc.lisp

Log Message:
-----------
Merge pull request #1853 from copperteal/type-spec/add-list-to-doc

Add `LIST` to type table in `TYPE-SPEC` doc

Commit: 220687f7f583e7d4ce7e27d60ece39339ba30ba7
https://github.com/acl2/acl2/commit/220687f7f583e7d4ce7e27d60ece39339ba30ba7

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

Date: 2025-09-21 (Sun, 21 Sep 2025)

Changed paths:

M books/kestrel/c/syntax/reader.lisp

Log Message:
-----------
Merge commit '952144127257e953bfb84e27446c6cfe05af21d6' into HEAD

Commit: a8da967d3bf18ed0ae5adb943de8e728ba736587
https://github.com/acl2/acl2/commit/a8da967d3bf18ed0ae5adb943de8e728ba736587
Author: Matt Kaufmann <kauf...@cs.utexas.edu>

Date: 2025-09-21 (Sun, 21 Sep 2025)

Changed paths:

M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Synch doc.lisp etc.

Commit: b439ebe3e052f77d45930a2de28e049fd274210e
https://github.com/acl2/acl2/commit/b439ebe3e052f77d45930a2de28e049fd274210e
Author: MattKaufmann <kauf...@cs.utexas.edu>

Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:

M books/projects/codewalker/basic-demo.lsp

Log Message:
-----------
Merge pull request #1854 from copperteal/codewalker/demo-fix

Update Codewalker basic demo for filename adjustments

Commit: 95f8781ee227053c49ae00d04982e0959a3a2f85
https://github.com/acl2/acl2/commit/95f8781ee227053c49ae00d04982e0959a3a2f85
Author: Matt Kaufmann <matthew.j...@gmail.com>

Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:

M books/projects/hol-in-acl2/acl2/lemmas.lisp
M books/projects/hol-in-acl2/acl2/package.lsp
M books/projects/hol-in-acl2/acl2/theories.lisp
A books/projects/hol-in-acl2/acl2/typ.lisp
M books/projects/hol-in-acl2/examples/README
A books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
A books/projects/hol-in-acl2/examples/eval-poly-thy-alt.lisp
A books/projects/hol-in-acl2/to-do.txt

Log Message:
-----------
Add proof of a distributive law for a HOL expression evaluator, carried out by reducing it to a trivial proof of a corresponding theorem about an ACL2 expression evaluator.

See books/projects/hol-in-acl2/examples/eval-poly-proof.lisp. This
work takes advantage of the translation from HOL to ACL2 carried out
with Konrad Slind, by applying Konrad's translator and my defhol macro
to translate the desired HOL theorem into ACL2 as extended by the ZF
set theory books.

Commit: 45c9f854b72a1d67d02dbfdc5c3c3e576c65f9da
https://github.com/acl2/acl2/commit/45c9f854b72a1d67d02dbfdc5c3c3e576c65f9da
Author: Matt Kaufmann <matthew.j...@gmail.com>

Date: 2025-09-22 (Mon, 22 Sep 2025)

Changed paths:

M books/projects/hol-in-acl2/to-do.txt

Log Message:
-----------
Add a to-do item.

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