[acl2/acl2] 94bcad: [axe] Add some type declarations.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 94bcad168d90391a1b4dd563f5936fbc5e92f215
https://github.com/acl2/acl2/commit/94bcad168d90391a1b4dd563f5936fbc5e92f215
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)

Changed paths:
M books/kestrel/axe/hit-counts.lisp
M books/kestrel/axe/rule-limits.lisp
M books/kestrel/axe/tries.lisp

Log Message:
-----------
[axe] Add some type declarations.


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

Changed paths:
M books/kestrel/alists-light/acons-unique.lisp

Log Message:
-----------
[alists-light] Add sanity check rule.


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

Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp

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


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

Changed paths:
M books/kestrel/axe/rule-limits.lisp

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


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

Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-limits.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/executable-parsers/elf-tools.lisp

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


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

Changed paths:
M books/kestrel/axe/rule-limits.lisp

Log Message:
-----------
[axe] Reduce dependencies.


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

Changed paths:
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/rule-limits.lisp

Log Message:
-----------
[axe] Improve rule-limit machinery.

This avoids a rare issue where the limit could be exceeded by 1 when it was exhausted while successfully relieving the hyps of a rule.


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

Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
A books/kestrel/c/syntax/tests/gincluder.c
A books/kestrel/c/syntax/tests/gincluder1.h
A books/kestrel/c/syntax/tests/gincluder2.h
A books/kestrel/c/syntax/tests/guarded.h
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.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
M books/kestrel/c/transformation/tests/add-section-attr/test3.c
M books/kestrel/c/transformation/utilities/add-attributes.lisp

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


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

Changed paths:
M books/kestrel/c/syntax/.sys/ty...@useless-runes.lsp
A books/kestrel/c/syntax/.sys/u...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/validation-...@useless-runes.lsp
M books/kestrel/c/syntax/.sys/vali...@useless-runes.lsp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
A books/kestrel/c/syntax/tests/types.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/types.lisp
A books/kestrel/c/syntax/uid.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/split-all-gso/extern-struct.c
M books/kestrel/c/transformation/tests/split-all-gso/split-all-gso.lisp
M books/kestrel/c/transformation/tests/split-all-gso/static-struct1.c
M books/kestrel/c/transformation/tests/split-all-gso/static-struct2.c
M books/kestrel/c/transformation/tests/split-gso/extern-struct.c
M books/kestrel/c/transformation/tests/split-gso/split-gso.lisp

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


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

Changed paths:
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/x86/lifter-support.lisp

Log Message:
-----------
[axe] Slightly improve lifters.


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

Changed paths:
M books/acl2s/cgen/callback.lisp
M books/kestrel/c/atc/expression-generation.lisp
M books/kestrel/c/atc/function-and-loop-generation.lisp
M books/kestrel/c/atc/function-tables.lisp
M books/kestrel/c/atc/generation-contexts.lisp
M books/kestrel/c/atc/generation.lisp
M books/kestrel/c/atc/limits.lisp
M books/kestrel/c/atc/pretty-printing-options.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/term-checkers-atc.lisp
M books/kestrel/c/atc/theorem-generation.lisp
M books/kestrel/c/package.lsp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
R books/kestrel/c/syntax/tests/gincluder.c
A books/kestrel/c/syntax/tests/gincluder1.c
M books/kestrel/c/syntax/tests/gincluder1.h
A books/kestrel/c/syntax/tests/gincluder2.c
M books/kestrel/c/syntax/tests/gincluder2.h
A books/kestrel/c/syntax/tests/gincludermod1.c
A books/kestrel/c/syntax/tests/gincludermod2.c
M books/kestrel/c/syntax/tests/guarded.h
M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-alt.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval_poly.defhol
M books/projects/hol-in-acl2/examples/eval_polyScript.sml
M books/projects/pfcs/abstract-syntax-trees.lisp

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


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

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

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


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

Changed paths:
A books/kestrel/c/transformation/command-line/tests/add-section-attr-mac.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2-mac.json
M books/kestrel/c/transformation/command-line/tests/run-tests.sh

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


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

Changed paths:
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions.lisp

Log Message:
-----------
[axe/x86] Add :feature-flags option to lifters and tester.


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

Changed paths:
M books/kestrel/x86/assumptions.lisp

Log Message:
-----------
[axe/x86] Add :bmi1 to default set of feature-flags.

Thanks to Sudarshan Srinivasan for identifying the need for this on an example.


Compare: https://github.com/acl2/acl2/compare/0247aaba4d8f...1054c590f67a

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

[Eric W. Smith]

Branch: refs/heads/master

[Eric W. Smith]

Branch: refs/heads/testing