[acl2/acl2] 5da262: [axe/x86] Drop unneeded .acl2 files.

0 views

Skip to first unread message

Eric W. Smith

unread,

Feb 4, 2026, 6:14:53 AM (7 days ago) Feb 4

to acl2-...@googlegroups.com

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 5da2624e614d9ebb88aa2791497405ffec4c7e3c
https://github.com/acl2/acl2/commit/5da2624e614d9ebb88aa2791497405ffec4c7e3c
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-30 (Fri, 30 Jan 2026)

Changed paths:
R books/kestrel/axe/x86/evaluator-x86.acl2
M books/kestrel/axe/x86/evaluator-x86.lisp
R books/kestrel/x86/x86-changes.acl2
M books/kestrel/x86/x86-changes.lisp

Log Message:
-----------
[axe/x86] Drop unneeded .acl2 files.

Also update comments about ttags.

Commit: c5bd7804e30dd37a4d6f516335c792af219e52ed
https://github.com/acl2/acl2/commit/c5bd7804e30dd37a4d6f516335c792af219e52ed
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-30 (Fri, 30 Jan 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/c17-std-example5-6.10.3.5.c
M books/kestrel/c/syntax/tests/macros.c
M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/kestrel/c/syntax/token-concatenation.lisp

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

Commit: 8d555afe49c9e36fdc59077c77267fa653f509cb
https://github.com/acl2/acl2/commit/8d555afe49c9e36fdc59077c77267fa653f509cb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-01-30 (Fri, 30 Jan 2026)

Changed paths:
M books/projects/x86isa/machine/environment-and-syscalls-raw.lsp
M books/projects/x86isa/machine/other-non-det-raw.lsp
M books/projects/x86isa/machine/register-readers-and-writers-raw.lsp

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

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

Changed paths:
M books/doc/relnotes.lisp
M books/kestrel/arm/def-inst.lisp
A 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/package.lsp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/arm/step.lisp
A books/kestrel/arm/tests/acl2-customization.lsp
A books/kestrel/arm/tests/simple.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/c/language/integer-operations.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser.lisp
A books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor.lisp
A books/kestrel/c/syntax/tests/concatenate.c
M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/kestrel/c/transformation/proof-generation.lisp
R books/kestrel/data/treeset/benchmark/benchmark.lsp.bak
R books/kestrel/data/treeset/benchmark/benchmark.lsp.bak.bak
R books/kestrel/data/treeset/benchmark/random.lisp.bak
M books/kestrel/data/treeset/in.lisp
M books/kestrel/data/treeset/insert-defs.lisp
M books/kestrel/data/treeset/internal/.sys/b...@useless-runes.lsp
M books/kestrel/data/treeset/internal/bst.lisp
M books/kestrel/data/treeset/internal/heap-order.lisp
M books/kestrel/data/treeset/internal/heap.lisp
M books/kestrel/data/treeset/internal/in.lisp
M books/kestrel/data/treeset/internal/split.lisp
M books/kestrel/data/treeset/internal/subset.lisp
M books/kestrel/data/treeset/subset.lisp
M books/kestrel/data/utilities/total-order/total-order.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/utilities/ld-history.lisp
M books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
M books/projects/hol-in-acl2/to-do.txt
M books/xdoc/display.lisp

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

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

Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/stringization.lisp
M books/kestrel/c/transformation/proof-generation.lisp

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

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

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

Log Message:
-----------
[axe/jvm] Slightly improve unroller.

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

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

Log Message:
-----------
[axe/x86] Slightly improve unroller.

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

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

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

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

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

Log Message:
-----------
[axe] Improve x86 and risc-v lifters.

Thread through the no-warn-ground-functions.

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

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/unroller.lisp
A books/kestrel/axe/x86/lifter-support.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/top.lisp
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe] Small improvements to lifters.

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

Changed paths:
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/output-files.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
A books/kestrel/c/transformation/add-section-attr-doc.lisp
A books/kestrel/c/transformation/add-section-attr.lisp
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/specialize.lisp
M books/kestrel/c/transformation/split-all-gso.lisp
M books/kestrel/c/transformation/split-fn-when.lisp
M books/kestrel/c/transformation/split-fn.lisp
M books/kestrel/c/transformation/split-gso.lisp
A books/kestrel/c/transformation/tests/add-section-attr/.gitignore
A books/kestrel/c/transformation/tests/add-section-attr/acl2-customization.lsp
A books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/cert.acl2
A books/kestrel/c/transformation/tests/add-section-attr/test1.c
A books/kestrel/c/transformation/tests/add-section-attr/test2.c
A books/kestrel/c/transformation/tests/add-section-attr/test3.c
M books/kestrel/c/transformation/top.lisp
A books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
A books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/utilities/top.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
M books/kestrel/fty/deffold-map-doc.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/utilities/run-json-command.lisp

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

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

Changed paths:
M books/kestrel/axe/risc-v/unroller.lisp

Log Message:
-----------
[axe/risc-v] Tweak unroller.

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

Changed paths:
M books/kestrel/utilities/redundancy.lisp

Log Message:
-----------
[utilities] Improve redundancy utils.

Use the package of the command name when making the table name. Also, add new util redundancy-table-event.

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

Changed paths:
M books/std/util/defaggregate.lisp
M books/std/util/tests/defaggregate.lisp

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

Commit: 625fcf0ef0dfc675ad36e4846eb2c2b1f31dbbd8
https://github.com/acl2/acl2/commit/625fcf0ef0dfc675ad36e4846eb2c2b1f31dbbd8
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
M books/kestrel/utilities/redundancy.lisp

Log Message:
-----------
[utilities] Improve printing.

Commit: f488d13200a4923dd73fee692d6d0a720c134c1b
https://github.com/acl2/acl2/commit/f488d13200a4923dd73fee692d6d0a720c134c1b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp

Log Message:
-----------
[axe] Improve redundancy checking.

Use the newly improved, general utilities.

Commit: a1674138cba2b2924f5563ebad7cf1eecd622d91
https://github.com/acl2/acl2/commit/a1674138cba2b2924f5563ebad7cf1eecd622d91
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
A books/kestrel/arm/top.lisp
M books/kestrel/top.lisp

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

Compare: https://github.com/acl2/acl2/compare/bb08a43351d0...a1674138cba2

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

acl2buildserver

unread,

Feb 4, 2026, 8:40:50 AM (6 days ago) Feb 4

to acl2-...@googlegroups.com

Branch: refs/heads/master

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

Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
A books/kestrel/arm/top.lisp
M books/kestrel/top.lisp

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

[arm] Add top book.

Thanks to Eric McCarthy for suggesting this.

Commit: a1674138cba2b2924f5563ebad7cf1eecd622d91
https://github.com/acl2/acl2/commit/a1674138cba2b2924f5563ebad7cf1eecd622d91
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
A books/kestrel/arm/top.lisp
M books/kestrel/top.lisp

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

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

Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
A books/kestrel/arm/top.lisp

M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp

M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/unroller.lisp
R books/kestrel/axe/x86/evaluator-x86.acl2
M books/kestrel/axe/x86/evaluator-x86.lisp

A books/kestrel/axe/x86/lifter-support.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/top.lisp
M books/kestrel/axe/x86/unroller.lisp

M books/kestrel/top.lisp
M books/kestrel/utilities/redundancy.lisp
M books/kestrel/x86/tools/lifter-support.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp

R books/kestrel/x86/x86-changes.acl2
M books/kestrel/x86/x86-changes.lisp

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

Merge commit 'a1674138cba2b2924f5563ebad7cf1eecd622d91' into HEAD

Compare: https://github.com/acl2/acl2/compare/7c7e62bba6ff...223141e65ea7

acl2buildserver

unread,

Feb 4, 2026, 8:41:36 AM (6 days ago) Feb 4

to acl2-...@googlegroups.com

Branch: refs/heads/testing

Alessandro Coglio

unread,

Feb 4, 2026, 10:54:50 PM (6 days ago) Feb 4

to acl2-...@googlegroups.com

Branch: refs/heads/testing-user-01

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

Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-03 (Tue, 03 Feb 2026)

Changed paths:

M books/kestrel/c/transformation/command-line/transform-c.lisp

Log Message:
-----------
[C2C] Improve comment.

Commit: 71cca297c2e1eb253a46e35307c0b8319c6fd4bb
https://github.com/acl2/acl2/commit/71cca297c2e1eb253a46e35307c0b8319c6fd4bb

Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-03 (Tue, 03 Feb 2026)

Changed paths:

M books/kestrel/utilities/run-json-command.lisp

Log Message:
-----------
[utilities] Change how we translate JSON's null to an ACL2 value.

Now it becomes the keyword :null, to distinguish it from nil, which is how we translate JSON's false value.

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

Commit: 73cfe6e0fdb9c9d81d6b24b7c0c3950e941cb500
https://github.com/acl2/acl2/commit/73cfe6e0fdb9c9d81d6b24b7c0c3950e941cb500

Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
A books/kestrel/arm/top.lisp
M books/kestrel/top.lisp

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

Commit: a1674138cba2b2924f5563ebad7cf1eecd622d91
https://github.com/acl2/acl2/commit/a1674138cba2b2924f5563ebad7cf1eecd622d91
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
A books/kestrel/arm/top.lisp
M books/kestrel/top.lisp

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

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

Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/unroller.lisp
M books/kestrel/axe/jvm/unroller2.lisp

M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/unroller.lisp
R books/kestrel/axe/x86/evaluator-x86.acl2
M books/kestrel/axe/x86/evaluator-x86.lisp
A books/kestrel/axe/x86/lifter-support.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/top.lisp
M books/kestrel/axe/x86/unroller.lisp

Commit: 9f3efe3d2c34d17eae2b53ff49bd499d66047f74
https://github.com/acl2/acl2/commit/9f3efe3d2c34d17eae2b53ff49bd499d66047f74
Author: Grant Jurgensen <gr...@jurgensen.dev>