[acl2/acl2] 14dbcd: [ATC] Use controlled configuration in a file.
0 views
Skip to first unread message
Alessandro Coglio
Feb 8, 2026, 3:19:37 PM (2 days ago) Feb 8
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 14dbcd9c7eb0f0f78dbadd8ccc9f9ea90fd6bb89
https://github.com/acl2/acl2/commit/14dbcd9c7eb0f0f78dbadd8ccc9f9ea90fd6bb89
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printing-options.lisp
Log Message:
-----------
[ATC] Use controlled configuration in a file.
Commit: c94cd1dcbc291bffa444a9f5d15a45ec2ccbec0e
https://github.com/acl2/acl2/commit/c94cd1dcbc291bffa444a9f5d15a45ec2ccbec0e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/atc/limits.lisp
Log Message:
-----------
[ATC] Add an irrelevant.
Commit: a37bb16b909402a355a1babc48db9c799aa29d8e
https://github.com/acl2/acl2/commit/a37bb16b909402a355a1babc48db9c799aa29d8e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/package.lsp
Log Message:
-----------
[ATC] Add symbol to the package.
Commit: 975c4372b0510863a05d768a8380a25690106b7a
https://github.com/acl2/acl2/commit/975c4372b0510863a05d768a8380a25690106b7a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/atc/limits.lisp
Log Message:
-----------
[ATC] Improve limit data structure.
Use translated terms internally (and untranslate them in the dedicated
operation), so we can perform substitutions. Also add a substitution operation.
Commit: 1684644eb450da0bc66d918e78e9cebfd6da95fb
https://github.com/acl2/acl2/commit/1684644eb450da0bc66d918e78e9cebfd6da95fb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/package.lsp
Log Message:
-----------
[C] Update file header.
Commit: 0f8bf279883a2e9588b8d084d94e143c17296077
https://github.com/acl2/acl2/commit/0f8bf279883a2e9588b8d084d94e143c17296077
Author: Alessandro Coglio <em...@alessandrocoglio.info>
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
M books/kestrel/axe/translate-dag-to-stp.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/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/implementation-environments.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
A books/kestrel/c/syntax/tests/conditional.c
M books/kestrel/c/syntax/tests/output-files.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
A books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.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/top.lisp
M books/kestrel/utilities/redundancy.lisp
M books/kestrel/utilities/run-json-command.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
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
M books/std/util/defaggregate.lisp
M books/std/util/tests/defaggregate.lisp
Log Message:
-----------
Merge.
Commit: b926201d3609f3b5e380ebfde2233d25b13846b7
https://github.com/acl2/acl2/commit/b926201d3609f3b5e380ebfde2233d25b13846b7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-08 (Sun, 08 Feb 2026)
Changed paths:
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/statement-generation.lisp
M books/kestrel/c/atc/term-checkers-atc.lisp
M books/kestrel/c/atc/theorem-generation.lisp
Log Message:
-----------
[ATC] Improve generated theorems.
Use a dedicated data structure to keep track, and calculate, minimal limits for
termination. Values of this data structure are turned into readable untranslated
terms. This avoids the sometimes deep and not very readable translated terms
with additions involving constants.
Commit: 9389b6cd5d9a70c67bc23b3895f76da4578b0aa0
https://github.com/acl2/acl2/commit/9389b6cd5d9a70c67bc23b3895f76da4578b0aa0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-08 (Sun, 08 Feb 2026)
Changed paths:
M books/acl2s/cgen/callback.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/step.lisp
M books/kestrel/axe/def-simplified.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/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/support-non-axe.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/tactic-prover.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-32-proof.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-64-proof.lisp
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/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
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
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/add-section-attr-doc.lisp
M books/kestrel/c/transformation/add-section-attr.lisp
A books/kestrel/c/transformation/command-line/tests/add-section-attr.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2.json
A books/kestrel/c/transformation/command-line/tests/input-files/file10.c
A books/kestrel/c/transformation/command-line/tests/input-files/file11.c
A books/kestrel/c/transformation/command-line/tests/input-files/file9.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
M books/kestrel/c/transformation/command-line/transform-c.lisp
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
M books/kestrel/c/transformation/tests/add-section-attr/test3.c
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
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
A books/kestrel/executable-parsers/.sys/elf-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/mach-o...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-e...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ex...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ma...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parsed-exec...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parser...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/pe-t...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/t...@useless-runes.lsp
A books/kestrel/executable-parsers/elf-tools.lisp
A books/kestrel/executable-parsers/mach-o-tools.lisp
A books/kestrel/executable-parsers/parse-elf-file.lisp
A books/kestrel/executable-parsers/parse-executable.lisp
A books/kestrel/executable-parsers/parse-mach-o-file.lisp
A books/kestrel/executable-parsers/parse-pe-file.lisp
A books/kestrel/executable-parsers/parsed-executable-tools.lisp
A books/kestrel/executable-parsers/parser-utils.lisp
A books/kestrel/executable-parsers/pe-tools.lisp
A books/kestrel/executable-parsers/top.lisp
M books/kestrel/json-parser/parsed-json.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/top.lisp
M books/kestrel/utilities/run-json-command.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/assumptions64.lisp
R books/kestrel/x86/parsers/.sys/elf-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/mach-o...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-e...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ex...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ma...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parsed-exec...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parser...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/pe-t...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/t...@useless-runes.lsp
R books/kestrel/x86/parsers/elf-tools.lisp
R books/kestrel/x86/parsers/mach-o-tools.lisp
R books/kestrel/x86/parsers/parse-elf-file.lisp
R books/kestrel/x86/parsers/parse-executable.lisp
R books/kestrel/x86/parsers/parse-mach-o-file.lisp
R books/kestrel/x86/parsers/parse-pe-file.lisp
R books/kestrel/x86/parsers/parsed-executable-tools.lisp
R books/kestrel/x86/parsers/parser-utils.lisp
R books/kestrel/x86/parsers/pe-tools.lisp
R books/kestrel/x86/parsers/top.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
M books/kestrel/x86/top.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
Log Message:
-----------
Merge.
Commit: fa371426dc7ba511c255166ee992ce86e68c687a
https://github.com/acl2/acl2/commit/fa371426dc7ba511c255166ee992ce86e68c687a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-08 (Sun, 08 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/e8022dad2758...fa371426dc7b
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 14dbcd9c7eb0f0f78dbadd8ccc9f9ea90fd6bb89
https://github.com/acl2/acl2/commit/14dbcd9c7eb0f0f78dbadd8ccc9f9ea90fd6bb89
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/atc/pretty-printing-options.lisp
Log Message:
-----------
[ATC] Use controlled configuration in a file.
Commit: c94cd1dcbc291bffa444a9f5d15a45ec2ccbec0e
https://github.com/acl2/acl2/commit/c94cd1dcbc291bffa444a9f5d15a45ec2ccbec0e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/atc/limits.lisp
Log Message:
-----------
[ATC] Add an irrelevant.
Commit: a37bb16b909402a355a1babc48db9c799aa29d8e
https://github.com/acl2/acl2/commit/a37bb16b909402a355a1babc48db9c799aa29d8e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/package.lsp
Log Message:
-----------
[ATC] Add symbol to the package.
Commit: 975c4372b0510863a05d768a8380a25690106b7a
https://github.com/acl2/acl2/commit/975c4372b0510863a05d768a8380a25690106b7a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/atc/limits.lisp
Log Message:
-----------
[ATC] Improve limit data structure.
Use translated terms internally (and untranslate them in the dedicated
operation), so we can perform substitutions. Also add a substitution operation.
Commit: 1684644eb450da0bc66d918e78e9cebfd6da95fb
https://github.com/acl2/acl2/commit/1684644eb450da0bc66d918e78e9cebfd6da95fb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-03 (Tue, 03 Feb 2026)
Changed paths:
M books/kestrel/c/package.lsp
Log Message:
-----------
[C] Update file header.
Commit: 0f8bf279883a2e9588b8d084d94e143c17296077
https://github.com/acl2/acl2/commit/0f8bf279883a2e9588b8d084d94e143c17296077
Author: Alessandro Coglio <em...@alessandrocoglio.info>
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
M books/kestrel/axe/translate-dag-to-stp.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/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/implementation-environments.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/parser.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
A books/kestrel/c/syntax/tests/conditional.c
M books/kestrel/c/syntax/tests/output-files.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
A books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.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/top.lisp
M books/kestrel/utilities/redundancy.lisp
M books/kestrel/utilities/run-json-command.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
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
M books/std/util/defaggregate.lisp
M books/std/util/tests/defaggregate.lisp
Log Message:
-----------
Merge.
Commit: b926201d3609f3b5e380ebfde2233d25b13846b7
https://github.com/acl2/acl2/commit/b926201d3609f3b5e380ebfde2233d25b13846b7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-08 (Sun, 08 Feb 2026)
Changed paths:
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/statement-generation.lisp
M books/kestrel/c/atc/term-checkers-atc.lisp
M books/kestrel/c/atc/theorem-generation.lisp
Log Message:
-----------
[ATC] Improve generated theorems.
Use a dedicated data structure to keep track, and calculate, minimal limits for
termination. Values of this data structure are turned into readable untranslated
terms. This avoids the sometimes deep and not very readable translated terms
with additions involving constants.
Commit: 9389b6cd5d9a70c67bc23b3895f76da4578b0aa0
https://github.com/acl2/acl2/commit/9389b6cd5d9a70c67bc23b3895f76da4578b0aa0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-08 (Sun, 08 Feb 2026)
Changed paths:
M books/acl2s/cgen/callback.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/step.lisp
M books/kestrel/axe/def-simplified.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/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/support-non-axe.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/tactic-prover.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-32-proof.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-64-proof.lisp
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/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
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
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/add-section-attr-doc.lisp
M books/kestrel/c/transformation/add-section-attr.lisp
A books/kestrel/c/transformation/command-line/tests/add-section-attr.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2.json
A books/kestrel/c/transformation/command-line/tests/input-files/file10.c
A books/kestrel/c/transformation/command-line/tests/input-files/file11.c
A books/kestrel/c/transformation/command-line/tests/input-files/file9.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
M books/kestrel/c/transformation/command-line/transform-c.lisp
M books/kestrel/c/transformation/command-line/wrappers.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/kestrel/c/transformation/tests/add-section-attr/external-foo.c
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
M books/kestrel/c/transformation/tests/add-section-attr/test3.c
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
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/call-graph.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
A books/kestrel/executable-parsers/.sys/elf-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/mach-o...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-e...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ex...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ma...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parsed-exec...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parser...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/pe-t...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/t...@useless-runes.lsp
A books/kestrel/executable-parsers/elf-tools.lisp
A books/kestrel/executable-parsers/mach-o-tools.lisp
A books/kestrel/executable-parsers/parse-elf-file.lisp
A books/kestrel/executable-parsers/parse-executable.lisp
A books/kestrel/executable-parsers/parse-mach-o-file.lisp
A books/kestrel/executable-parsers/parse-pe-file.lisp
A books/kestrel/executable-parsers/parsed-executable-tools.lisp
A books/kestrel/executable-parsers/parser-utils.lisp
A books/kestrel/executable-parsers/pe-tools.lisp
A books/kestrel/executable-parsers/top.lisp
M books/kestrel/json-parser/parsed-json.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/top.lisp
M books/kestrel/utilities/run-json-command.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/assumptions64.lisp
R books/kestrel/x86/parsers/.sys/elf-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/mach-o...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-e...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ex...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ma...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parsed-exec...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parser...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/pe-t...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/t...@useless-runes.lsp
R books/kestrel/x86/parsers/elf-tools.lisp
R books/kestrel/x86/parsers/mach-o-tools.lisp
R books/kestrel/x86/parsers/parse-elf-file.lisp
R books/kestrel/x86/parsers/parse-executable.lisp
R books/kestrel/x86/parsers/parse-mach-o-file.lisp
R books/kestrel/x86/parsers/parse-pe-file.lisp
R books/kestrel/x86/parsers/parsed-executable-tools.lisp
R books/kestrel/x86/parsers/parser-utils.lisp
R books/kestrel/x86/parsers/pe-tools.lisp
R books/kestrel/x86/parsers/top.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
M books/kestrel/x86/top.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
Log Message:
-----------
Merge.
Commit: fa371426dc7ba511c255166ee992ce86e68c687a
https://github.com/acl2/acl2/commit/fa371426dc7ba511c255166ee992ce86e68c687a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-08 (Sun, 08 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/e8022dad2758...fa371426dc7b
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Feb 8, 2026, 5:27:46 PM (2 days ago) Feb 8
to acl2-...@googlegroups.com
Branch: refs/heads/master
Alessandro Coglio
Feb 8, 2026, 5:28:37 PM (2 days ago) Feb 8
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Feb 8, 2026, 6:05:34 PM (2 days ago) Feb 8
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Commit: 19d99a9dc7815eba4c2d9d981e42bf022ddb8147
https://github.com/acl2/acl2/commit/19d99a9dc7815eba4c2d9d981e42bf022ddb8147
Author: Andrew Walter <m...@atwalter.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/acl2s/cgen/callback.lisp
Log Message:
-----------
[acl2s] Fix a type error in cgen's callback (#1899)
cgen's callback did not properly account for the fact that the ctx
argument may be a string and thus under certain circumstances it
would try to take the car of a string, causing a type error when ACL2
is built with `(safety 3)`.
This was fixed by adding a `consp` check before the offending `car`
form.
Commit: dd729c988c9d36f55c0c6dee79af958d0331a266
https://github.com/acl2/acl2/commit/dd729c988c9d36f55c0c6dee79af958d0331a266
Author: Pete Manolios <pman...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M acl2-init.lisp
M axioms.lisp
M books/GNUmakefile
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh
M books/doc/relnotes.lisp
M books/kestrel/acl2data/gather/patch-defthm.lsp
M books/kestrel/apt/solve-method-axe-rewriter.lisp
M books/kestrel/arithmetic-light/max.lisp
M books/kestrel/arithmetic-light/min.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
A books/kestrel/arm/top.lisp
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/equivalence-checker.lisp
A books/kestrel/axe/evaluator-support.lisp
M books/kestrel/axe/evaluator-tests.acl2
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/evaluator.acl2
M books/kestrel/axe/evaluator.lisp
M books/kestrel/axe/hit-counts.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/prune-term.lisp
M books/kestrel/axe/rewriter-basic-smt-tests.lisp
M books/kestrel/axe/rewriter-basic-tests.lisp
M books/kestrel/axe/rewriter-basic.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
R books/kestrel/axe/x86/evaluator-x86.acl2
M books/kestrel/axe/x86/evaluator-x86.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rewriter-x86-tests.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester-code-only.lisp
M books/kestrel/axe/x86/tester-rules.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/top.lisp
M books/kestrel/axe/x86/unroller-code-only.lisp
M books/kestrel/axe/x86/unroller.acl2
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/c/atc/generation.lisp
A books/kestrel/c/atc/limits.lisp
M books/kestrel/c/language/implementation-environments/versions.lisp
M books/kestrel/c/language/integer-operations.lisp
M books/kestrel/c/language/keywords.lisp
A books/kestrel/c/language/punctuators.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/builtin.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/lexer.lisp
A books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
A books/kestrel/c/syntax/preprocessor-evaluator.lisp
A books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
A books/kestrel/c/syntax/stringization.lisp
A books/kestrel/c/syntax/tests/c17-std-example-6.10.3.3.c
A books/kestrel/c/syntax/tests/c17-std-example-6.10.3.4.c
A books/kestrel/c/syntax/tests/c17-std-example1-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example2-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example3-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example4-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example5-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example6-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example7-6.10.3.5.c
A books/kestrel/c/syntax/tests/concatenate.c
A books/kestrel/c/syntax/tests/conditional.c
A books/kestrel/c/syntax/tests/macros.c
M books/kestrel/c/syntax/tests/output-files.lisp
M books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/validator.lisp
A books/kestrel/c/syntax/token-concatenation.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/top.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/transform-c.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/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
A books/kestrel/c/transformation/tests/add-section-attr/internal-foo.c
A books/kestrel/data/.sys/t...@useless-runes.lsp
A books/kestrel/data/acl2-customization.lsp
A books/kestrel/data/cert.acl2
A books/kestrel/data/doc.lisp
A books/kestrel/data/hash/.sys/jenkin...@useless-runes.lsp
A books/kestrel/data/hash/.sys/jen...@useless-runes.lsp
A books/kestrel/data/hash/.sys/portc...@useless-runes.lsp
A books/kestrel/data/hash/.sys/t...@useless-runes.lsp
A books/kestrel/data/hash/acl2-customization.lsp
A books/kestrel/data/hash/cert.acl2
A books/kestrel/data/hash/jenkins-defs.lisp
A books/kestrel/data/hash/jenkins.lisp
A books/kestrel/data/hash/package.lsp
A books/kestrel/data/hash/portcullis.acl2
A books/kestrel/data/hash/portcullis.lisp
A books/kestrel/data/hash/top.lisp
A books/kestrel/data/package.lsp
A books/kestrel/data/portcullis.acl2
A books/kestrel/data/portcullis.lisp
A books/kestrel/data/top.lisp
A books/kestrel/data/treeset/.sys/cardinal...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/cardi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/de...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/delet...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/del...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/diff...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/extensi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/f...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/generic-t...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/generi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/hash...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/ha...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/in-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/i...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/indu...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/inser...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/ins...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/interse...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/inte...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/iter...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/it...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/min-ma...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/min...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/portc...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/set-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/s...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/subse...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/to-ose...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/to-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/t...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/union...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/un...@useless-runes.lsp
A books/kestrel/data/treeset/acl2-customization.lsp
A books/kestrel/data/treeset/benchmark/acl2-customization.lsp
A books/kestrel/data/treeset/benchmark/benchmark.lsp
A books/kestrel/data/treeset/benchmark/cert.acl2
A books/kestrel/data/treeset/benchmark/random.lisp
A books/kestrel/data/treeset/cardinality-defs.lisp
A books/kestrel/data/treeset/cardinality.lisp
A books/kestrel/data/treeset/cert.acl2
A books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/delete-defs.lisp
A books/kestrel/data/treeset/delete.lisp
A books/kestrel/data/treeset/diff-defs.lisp
A books/kestrel/data/treeset/diff.lisp
A books/kestrel/data/treeset/doc.lisp
A books/kestrel/data/treeset/extensionality.lisp
A books/kestrel/data/treeset/fty.lisp
A books/kestrel/data/treeset/generic-typed-defs.lisp
A books/kestrel/data/treeset/generic-typed.lisp
A books/kestrel/data/treeset/hash-defs.lisp
A books/kestrel/data/treeset/hash.lisp
A books/kestrel/data/treeset/in-defs.lisp
A books/kestrel/data/treeset/in.lisp
A books/kestrel/data/treeset/induction.lisp
A books/kestrel/data/treeset/insert-defs.lisp
A books/kestrel/data/treeset/insert.lisp
A books/kestrel/data/treeset/internal/.sys/antisy...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/bst-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/b...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/count...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/co...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/delet...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/del...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/diff...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap-or...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/he...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-ord...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-o...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/i...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/inser...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/ins...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/interse...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/inte...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/iter...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/it...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/join...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/jo...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/min-ma...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/min...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/rotat...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/rot...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/split...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/sp...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/subse...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/tree...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/tr...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/union...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/un...@useless-runes.lsp
A books/kestrel/data/treeset/internal/acl2-customization.lsp
A books/kestrel/data/treeset/internal/antisymmetry.lisp
A books/kestrel/data/treeset/internal/bst-defs.lisp
A books/kestrel/data/treeset/internal/bst.lisp
A books/kestrel/data/treeset/internal/cert.acl2
A books/kestrel/data/treeset/internal/count-defs.lisp
A books/kestrel/data/treeset/internal/count.lisp
A books/kestrel/data/treeset/internal/delete-defs.lisp
A books/kestrel/data/treeset/internal/delete.lisp
A books/kestrel/data/treeset/internal/diff-defs.lisp
A books/kestrel/data/treeset/internal/diff.lisp
A books/kestrel/data/treeset/internal/doc.lisp
A books/kestrel/data/treeset/internal/heap-defs.lisp
A books/kestrel/data/treeset/internal/heap-order-defs.lisp
A books/kestrel/data/treeset/internal/heap-order.lisp
A books/kestrel/data/treeset/internal/heap.lisp
A books/kestrel/data/treeset/internal/in-defs.lisp
A books/kestrel/data/treeset/internal/in-order-defs.lisp
A books/kestrel/data/treeset/internal/in-order.lisp
A books/kestrel/data/treeset/internal/in.lisp
A books/kestrel/data/treeset/internal/insert-defs.lisp
A books/kestrel/data/treeset/internal/insert.lisp
A books/kestrel/data/treeset/internal/intersect-defs.lisp
A books/kestrel/data/treeset/internal/intersect.lisp
A books/kestrel/data/treeset/internal/iter-defs.lisp
A books/kestrel/data/treeset/internal/iter.lisp
A books/kestrel/data/treeset/internal/join-defs.lisp
A books/kestrel/data/treeset/internal/join.lisp
A books/kestrel/data/treeset/internal/min-max-defs.lisp
A books/kestrel/data/treeset/internal/min-max.lisp
A books/kestrel/data/treeset/internal/rotate-defs.lisp
A books/kestrel/data/treeset/internal/rotate.lisp
A books/kestrel/data/treeset/internal/split-defs.lisp
A books/kestrel/data/treeset/internal/split.lisp
A books/kestrel/data/treeset/internal/subset-defs.lisp
A books/kestrel/data/treeset/internal/subset.lisp
A books/kestrel/data/treeset/internal/tree-defs.lisp
A books/kestrel/data/treeset/internal/tree.lisp
A books/kestrel/data/treeset/internal/union-defs.lisp
A books/kestrel/data/treeset/internal/union.lisp
A books/kestrel/data/treeset/intersect-defs.lisp
A books/kestrel/data/treeset/intersect.lisp
A books/kestrel/data/treeset/iter-defs.lisp
A books/kestrel/data/treeset/iter.lisp
A books/kestrel/data/treeset/min-max-defs.lisp
A books/kestrel/data/treeset/min-max.lisp
A books/kestrel/data/treeset/package.lsp
A books/kestrel/data/treeset/portcullis.acl2
A books/kestrel/data/treeset/portcullis.lisp
A books/kestrel/data/treeset/set-defs.lisp
A books/kestrel/data/treeset/set.lisp
A books/kestrel/data/treeset/subset-defs.lisp
A books/kestrel/data/treeset/subset.lisp
A books/kestrel/data/treeset/to-oset-defs.lisp
A books/kestrel/data/treeset/to-oset.lisp
A books/kestrel/data/treeset/top.lisp
A books/kestrel/data/treeset/union-defs.lisp
A books/kestrel/data/treeset/union.lisp
A books/kestrel/data/utilities/.sys/list...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/li...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/nat-...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/n...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/oset...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/os...@useless-runes.lsp
A books/kestrel/data/utilities/acl2-customization.lsp
A books/kestrel/data/utilities/bit-vectors/.sys/bitop...@useless-runes.lsp
A books/kestrel/data/utilities/bit-vectors/.sys/bit...@useless-runes.lsp
A books/kestrel/data/utilities/bit-vectors/acl2-customization.lsp
A books/kestrel/data/utilities/bit-vectors/bitops-defs.lisp
A books/kestrel/data/utilities/bit-vectors/bitops.lisp
A books/kestrel/data/utilities/bit-vectors/cert.acl2
A books/kestrel/data/utilities/cert.acl2
A books/kestrel/data/utilities/fixed-size-words/.sys/fix...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/.sys/u32-...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/.sys/u...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/acl2-customization.lsp
A books/kestrel/data/utilities/fixed-size-words/cert.acl2
A books/kestrel/data/utilities/fixed-size-words/fixnum.lisp
A books/kestrel/data/utilities/fixed-size-words/u32-defs.lisp
A books/kestrel/data/utilities/fixed-size-words/u32.lisp
A books/kestrel/data/utilities/list-defs.lisp
A books/kestrel/data/utilities/list.lisp
A books/kestrel/data/utilities/oset-defs.lisp
A books/kestrel/data/utilities/oset.lisp
A books/kestrel/data/utilities/top.lisp
A books/kestrel/data/utilities/total-order/.sys/max-...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/min-...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/total-or...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/total...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/acl2-customization.lsp
A books/kestrel/data/utilities/total-order/cert.acl2
A books/kestrel/data/utilities/total-order/max-defs.lisp
A books/kestrel/data/utilities/total-order/max.lisp
A books/kestrel/data/utilities/total-order/min-defs.lisp
A books/kestrel/data/utilities/total-order/min-max.lisp
A books/kestrel/data/utilities/total-order/min.lisp
A books/kestrel/data/utilities/total-order/total-order-defs.lisp
A books/kestrel/data/utilities/total-order/total-order.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/helpers/advice-implementation.lisp
M books/kestrel/helpers/advice-tests.lisp
A books/kestrel/helpers/defrule-tests.lisp
M books/kestrel/helpers/package.lsp
M books/kestrel/helpers/speed-up-implementation.lisp
M books/kestrel/top.lisp
R books/kestrel/treeset/.sys/binary-t...@useless-runes.lsp
R books/kestrel/treeset/.sys/binar...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-ord...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-...@useless-runes.lsp
R books/kestrel/treeset/.sys/b...@useless-runes.lsp
R books/kestrel/treeset/.sys/cardinal...@useless-runes.lsp
R books/kestrel/treeset/.sys/cardi...@useless-runes.lsp
R books/kestrel/treeset/.sys/de...@useless-runes.lsp
R books/kestrel/treeset/.sys/delet...@useless-runes.lsp
R books/kestrel/treeset/.sys/del...@useless-runes.lsp
R books/kestrel/treeset/.sys/diff...@useless-runes.lsp
R books/kestrel/treeset/.sys/di...@useless-runes.lsp
R books/kestrel/treeset/.sys/double-co...@useless-runes.lsp
R books/kestrel/treeset/.sys/f...@useless-runes.lsp
R books/kestrel/treeset/.sys/ha...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap-or...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap-...@useless-runes.lsp
R books/kestrel/treeset/.sys/he...@useless-runes.lsp
R books/kestrel/treeset/.sys/in-...@useless-runes.lsp
R books/kestrel/treeset/.sys/i...@useless-runes.lsp
R books/kestrel/treeset/.sys/inser...@useless-runes.lsp
R books/kestrel/treeset/.sys/ins...@useless-runes.lsp
R books/kestrel/treeset/.sys/interse...@useless-runes.lsp
R books/kestrel/treeset/.sys/inte...@useless-runes.lsp
R books/kestrel/treeset/.sys/jenkin...@useless-runes.lsp
R books/kestrel/treeset/.sys/join...@useless-runes.lsp
R books/kestrel/treeset/.sys/jo...@useless-runes.lsp
R books/kestrel/treeset/.sys/pick-a...@useless-runes.lsp
R books/kestrel/treeset/.sys/portc...@useless-runes.lsp
R books/kestrel/treeset/.sys/rotat...@useless-runes.lsp
R books/kestrel/treeset/.sys/rot...@useless-runes.lsp
R books/kestrel/treeset/.sys/set-...@useless-runes.lsp
R books/kestrel/treeset/.sys/s...@useless-runes.lsp
R books/kestrel/treeset/.sys/split...@useless-runes.lsp
R books/kestrel/treeset/.sys/sp...@useless-runes.lsp
R books/kestrel/treeset/.sys/subse...@useless-runes.lsp
R books/kestrel/treeset/.sys/sub...@useless-runes.lsp
R books/kestrel/treeset/.sys/sum-acl2-...@useless-runes.lsp
R books/kestrel/treeset/.sys/sum-acl...@useless-runes.lsp
R books/kestrel/treeset/.sys/t...@useless-runes.lsp
R books/kestrel/treeset/.sys/total...@useless-runes.lsp
R books/kestrel/treeset/.sys/union...@useless-runes.lsp
R books/kestrel/treeset/.sys/un...@useless-runes.lsp
R books/kestrel/treeset/acl2-customization.lsp
R books/kestrel/treeset/binary-tree-defs.lisp
R books/kestrel/treeset/binary-tree.lisp
R books/kestrel/treeset/bst-defs.lisp
R books/kestrel/treeset/bst-order-defs.lisp
R books/kestrel/treeset/bst-order.lisp
R books/kestrel/treeset/bst.lisp
R books/kestrel/treeset/cardinality-defs.lisp
R books/kestrel/treeset/cardinality.lisp
R books/kestrel/treeset/cert.acl2
R books/kestrel/treeset/defs.lisp
R books/kestrel/treeset/delete-defs.lisp
R books/kestrel/treeset/delete.lisp
R books/kestrel/treeset/diff-defs.lisp
R books/kestrel/treeset/diff.lisp
R books/kestrel/treeset/double-containment.lisp
R books/kestrel/treeset/fty.lisp
R books/kestrel/treeset/hash.lisp
R books/kestrel/treeset/heap-defs.lisp
R books/kestrel/treeset/heap-order-defs.lisp
R books/kestrel/treeset/heap-order.lisp
R books/kestrel/treeset/heap.lisp
R books/kestrel/treeset/in-defs.lisp
R books/kestrel/treeset/in.lisp
R books/kestrel/treeset/insert-defs.lisp
R books/kestrel/treeset/insert.lisp
R books/kestrel/treeset/intersect-defs.lisp
R books/kestrel/treeset/intersect.lisp
R books/kestrel/treeset/jenkins-hash.lisp
R books/kestrel/treeset/join-defs.lisp
R books/kestrel/treeset/join.lisp
R books/kestrel/treeset/package.lsp
R books/kestrel/treeset/pick-a-point.lisp
R books/kestrel/treeset/portcullis.acl2
R books/kestrel/treeset/portcullis.lisp
R books/kestrel/treeset/rotate-defs.lisp
R books/kestrel/treeset/rotate.lisp
R books/kestrel/treeset/set-defs.lisp
R books/kestrel/treeset/set.lisp
R books/kestrel/treeset/split-defs.lisp
R books/kestrel/treeset/split.lisp
R books/kestrel/treeset/subset-defs.lisp
R books/kestrel/treeset/subset.lisp
R books/kestrel/treeset/sum-acl2-count-defs.lisp
R books/kestrel/treeset/sum-acl2-count.lisp
R books/kestrel/treeset/tests/.sys/mk-r...@useless-runes.lsp
R books/kestrel/treeset/tests/.sys/mk-...@useless-runes.lsp
R books/kestrel/treeset/tests/.sys/time...@useless-runes.lsp
R books/kestrel/treeset/tests/acl2-customization.lsp
R books/kestrel/treeset/tests/cert.acl2
R books/kestrel/treeset/tests/mk-random.lisp
R books/kestrel/treeset/tests/mk-set.lisp
R books/kestrel/treeset/tests/tests.lsp
R books/kestrel/treeset/tests/time-set.lisp
R books/kestrel/treeset/top.lisp
R books/kestrel/treeset/total-order.lisp
R books/kestrel/treeset/union-defs.lisp
R books/kestrel/treeset/union.lisp
M books/kestrel/utilities/ld-history.lisp
M books/kestrel/utilities/redundancy.lisp
M books/kestrel/utilities/run-json-command.lisp
M books/kestrel/utilities/verify-guards-program-tests.lisp
M books/kestrel/utilities/verify-guards-program.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
M books/kestrel/x86/top.lisp
R books/kestrel/x86/x86-changes.acl2
M books/kestrel/x86/x86-changes.lisp
M books/projects/hol-in-acl2/README
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
M books/projects/hol-in-acl2/acl2/package.lsp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
M books/projects/hol-in-acl2/acl2/theories.lisp
R books/projects/hol-in-acl2/examples/README
A books/projects/hol-in-acl2/examples/README.txt
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/eval_poly.defhol
A books/projects/hol-in-acl2/examples/eval_polyScript.sml
M books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
M books/projects/hol-in-acl2/examples/ex1-top.lisp
A books/projects/hol-in-acl2/examples/ex1.defhol
A books/projects/hol-in-acl2/examples/ex1Script.sml
R books/projects/hol-in-acl2/hol4/eval-poly.sml
R books/projects/hol-in-acl2/hol4/ex1.sml
R books/projects/hol-in-acl2/hol4/translator.sml
M books/projects/hol-in-acl2/to-do.txt
M books/projects/vescmul/int-vector-adders-meta.lisp
M books/projects/x86isa/machine/cert.acl2
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/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/register-readers-and-writers-raw.lsp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/tools/execution/top.lisp
M books/std/strings/bin-digit-char-listp.lisp
M books/std/strings/dec-digit-char-listp.lisp
M books/std/strings/hex-digit-char-listp.lisp
M books/std/strings/oct-digit-char-listp.lisp
M books/std/util/defaggregate.lisp
M books/std/util/defprojection.lisp
M books/std/util/defrule.lisp
M books/std/util/tests/defaggregate.lisp
M books/system/doc/acl2-doc.lisp
A books/tools/eval-events-from-file-doc.lisp
A books/tools/eval-events-from-file-test-data.lsp
A books/tools/eval-events-from-file-test.lisp
A books/tools/eval-events-from-file.lisp
M books/tools/top.lisp
M books/tools/with-supporters-doc.lisp
M books/tools/with-supporters.lisp
M books/xdoc/display.lisp
M defthm.lisp
M defuns.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp
M other-events.lisp
M proof-builder-b.lisp
Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/master' into testing-acl2s
Commit: 4d8e886d5429c845772acb31343190d0dd8916b9
https://github.com/acl2/acl2/commit/4d8e886d5429c845772acb31343190d0dd8916b9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Improve preprocessor implementation.
Make the maximum macro reach part of the stobj.
Commit: bc13f6577e0cebed432ea0ce8929603d2e542dde
https://github.com/acl2/acl2/commit/bc13f6577e0cebed432ea0ce8929603d2e542dde
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
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 'f1215b5012c66da463b258e2e2eb2b6e3427af68' into HEAD
Commit: 9983ebdf1a551b55f3b91a5234f31cdf51223ade
https://github.com/acl2/acl2/commit/9983ebdf1a551b55f3b91a5234f31cdf51223ade
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
Commit: 57a866ed42bcbf2f363d132b906b297c16583feb
https://github.com/acl2/acl2/commit/57a866ed42bcbf2f363d132b906b297c16583feb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Update some doc.
Commit: 837f6f84bd078f649a0bca1bd411eed507db75d5
https://github.com/acl2/acl2/commit/837f6f84bd078f649a0bca1bd411eed507db75d5
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/transformation/split-gso.lisp
-----------
Merge commit 'f837cd4a60a48c40ff73c03461b857ce306953da' into HEAD
Commit: 7f0bb469e4404dfbbc830a0979682ea3d12fa882
https://github.com/acl2/acl2/commit/7f0bb469e4404dfbbc830a0979682ea3d12fa882
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Add file dependencies to preprocessor tests.
Commit: 5705fc5abfb60ca3c9309c693290fed5977f6cfc
https://github.com/acl2/acl2/commit/5705fc5abfb60ca3c9309c693290fed5977f6cfc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Extend preprocessor to track header guard state.
This is used to recognize whether a file has the header guard form.
We still need to make use of this information.
Commit: 139a07a6b96f4631118c6aab917a2439d8e00703
https://github.com/acl2/acl2/commit/139a07a6b96f4631118c6aab917a2439d8e00703
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-07 (Sat, 07 Feb 2026)
Changed paths:
M books/acl2s/cgen/callback.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
https://github.com/acl2/acl2/commit/d3690e62efa47d116a4d6321e8a7061c336fd5c0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-07 (Sat, 07 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Accumulate output lexemes in preprocessor states.
This simplifies some code, and also enabled an upcoming more elaborate
collection of output lexemes.
Commit: e8022dad27584f564acb631c309a71e5eb6702d7
https://github.com/acl2/acl2/commit/e8022dad27584f564acb631c309a71e5eb6702d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-07 (Sat, 07 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Extend treatment of header guards.
Reorganize the collected output lexemes into chunks related to the header guard
structure. When the file has the header guard structure, also output the
directives in question.
Adjust some test expectations.
Compare: https://github.com/acl2/acl2/compare/f837cd4a60a4...fa371426dc7b
https://github.com/acl2/acl2/commit/19d99a9dc7815eba4c2d9d981e42bf022ddb8147
Author: Andrew Walter <m...@atwalter.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/acl2s/cgen/callback.lisp
Log Message:
-----------
[acl2s] Fix a type error in cgen's callback (#1899)
cgen's callback did not properly account for the fact that the ctx
argument may be a string and thus under certain circumstances it
would try to take the car of a string, causing a type error when ACL2
is built with `(safety 3)`.
This was fixed by adding a `consp` check before the offending `car`
form.
Commit: dd729c988c9d36f55c0c6dee79af958d0331a266
https://github.com/acl2/acl2/commit/dd729c988c9d36f55c0c6dee79af958d0331a266
Author: Pete Manolios <pman...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M acl2-init.lisp
M axioms.lisp
M books/GNUmakefile
M books/build/jenkins/build-multi.sh
M books/build/jenkins/build-single.sh
M books/doc/relnotes.lisp
M books/kestrel/acl2data/gather/patch-defthm.lsp
M books/kestrel/apt/solve-method-axe-rewriter.lisp
M books/kestrel/arithmetic-light/max.lisp
M books/kestrel/arithmetic-light/min.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
A books/kestrel/arm/top.lisp
M books/kestrel/auto-termination/td-cands.acl2
M books/kestrel/auto-termination/td-cands.lisp
M books/kestrel/axe/bv-intro-rules.lisp
M books/kestrel/axe/def-simplified.lisp
M books/kestrel/axe/equivalence-checker.lisp
A books/kestrel/axe/evaluator-support.lisp
M books/kestrel/axe/evaluator-tests.acl2
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/evaluator.acl2
M books/kestrel/axe/evaluator.lisp
M books/kestrel/axe/hit-counts.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/make-prover-simple.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/make-rewriter-simple.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/prune-term.lisp
M books/kestrel/axe/rewriter-basic-smt-tests.lisp
M books/kestrel/axe/rewriter-basic-tests.lisp
M books/kestrel/axe/rewriter-basic.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/support-non-axe.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-limits.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/support-non-axe.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/tactic-prover.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/unguarded-defuns.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
R books/kestrel/axe/x86/evaluator-x86.acl2
M books/kestrel/axe/x86/evaluator-x86.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-elf64.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-32-proof.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-64-proof.lisp
A books/kestrel/axe/x86/lifter-support.lisp
M books/kestrel/axe/x86/examples/factorial/factorial-macho64.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-32-proof.lisp
M books/kestrel/axe/x86/examples/popcount/popcount-64-proof.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rewriter-x86-tests.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester-code-only.lisp
M books/kestrel/axe/x86/tester-rules.lisp
M books/kestrel/axe/x86/tester.lisp
M books/kestrel/axe/x86/top.lisp
M books/kestrel/axe/x86/unroller-code-only.lisp
M books/kestrel/axe/x86/unroller.acl2
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv/convert-to-bv-rules.lisp
M books/kestrel/c/atc/generation.lisp
A books/kestrel/c/atc/limits.lisp
M books/kestrel/c/language/implementation-environments/versions.lisp
M books/kestrel/c/language/integer-operations.lisp
M books/kestrel/c/language/keywords.lisp
A books/kestrel/c/language/punctuators.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/syntax/abstract-syntax-irrelevants.lisp
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/builtin.lisp
M books/kestrel/c/syntax/disambiguator.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/lexer.lisp
A books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/output-files.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/parser-states.lisp
M books/kestrel/c/syntax/parser.lisp
A books/kestrel/c/syntax/preprocessor-evaluator.lisp
A books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-lexer.lisp
M books/kestrel/c/syntax/preprocessor-messages.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/preprocessor-reader.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/printer.lisp
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
A books/kestrel/c/syntax/stringization.lisp
A books/kestrel/c/syntax/tests/c17-std-example-6.10.3.3.c
A books/kestrel/c/syntax/tests/c17-std-example-6.10.3.4.c
A books/kestrel/c/syntax/tests/c17-std-example1-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example2-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example3-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example4-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example5-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example6-6.10.3.5.c
A books/kestrel/c/syntax/tests/c17-std-example7-6.10.3.5.c
A books/kestrel/c/syntax/tests/concatenate.c
A books/kestrel/c/syntax/tests/conditional.c
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/input-files.lisp
A books/kestrel/c/syntax/tests/gincluder1.h
A books/kestrel/c/syntax/tests/gincluder2.h
A books/kestrel/c/syntax/tests/guarded.h
A books/kestrel/c/syntax/tests/macros.c
M books/kestrel/c/syntax/tests/output-files.lisp
M books/kestrel/c/syntax/tests/parser-states.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
A books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
A books/kestrel/c/syntax/tests/stringize.c
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
A books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
M books/kestrel/c/syntax/tests/validator.lisp
A books/kestrel/c/syntax/token-concatenation.lisp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/top.lisp
A books/kestrel/c/transformation/add-section-attr-doc.lisp
A books/kestrel/c/transformation/add-section-attr.lisp
A books/kestrel/c/transformation/command-line/tests/add-section-attr.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2.json
A books/kestrel/c/transformation/command-line/tests/input-files/file10.c
A books/kestrel/c/transformation/command-line/tests/input-files/file11.c
A books/kestrel/c/transformation/command-line/tests/input-files/file9.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
A books/kestrel/c/transformation/command-line/tests/split-gso-no-extensions.json
A books/kestrel/c/transformation/command-line/tests/add-section-attr2.json
A books/kestrel/c/transformation/command-line/tests/input-files/file10.c
A books/kestrel/c/transformation/command-line/tests/input-files/file11.c
A books/kestrel/c/transformation/command-line/tests/input-files/file9.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
M books/kestrel/c/transformation/command-line/transform-c.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/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0-doc.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/external-foo.c
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/internal-foo.c
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/tests/copy-fn/copy-fn.lisp
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
A books/kestrel/data/.sys/portc...@useless-runes.lsp
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
A books/kestrel/data/.sys/t...@useless-runes.lsp
A books/kestrel/data/acl2-customization.lsp
A books/kestrel/data/cert.acl2
A books/kestrel/data/doc.lisp
A books/kestrel/data/hash/.sys/jenkin...@useless-runes.lsp
A books/kestrel/data/hash/.sys/jen...@useless-runes.lsp
A books/kestrel/data/hash/.sys/portc...@useless-runes.lsp
A books/kestrel/data/hash/.sys/t...@useless-runes.lsp
A books/kestrel/data/hash/acl2-customization.lsp
A books/kestrel/data/hash/cert.acl2
A books/kestrel/data/hash/jenkins-defs.lisp
A books/kestrel/data/hash/jenkins.lisp
A books/kestrel/data/hash/package.lsp
A books/kestrel/data/hash/portcullis.acl2
A books/kestrel/data/hash/portcullis.lisp
A books/kestrel/data/hash/top.lisp
A books/kestrel/data/package.lsp
A books/kestrel/data/portcullis.acl2
A books/kestrel/data/portcullis.lisp
A books/kestrel/data/top.lisp
A books/kestrel/data/treeset/.sys/cardinal...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/cardi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/de...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/delet...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/del...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/diff...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/extensi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/f...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/generic-t...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/generi...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/hash...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/ha...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/in-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/i...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/indu...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/inser...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/ins...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/interse...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/inte...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/iter...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/it...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/min-ma...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/min...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/portc...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/set-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/s...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/subse...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/to-ose...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/to-...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/t...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/union...@useless-runes.lsp
A books/kestrel/data/treeset/.sys/un...@useless-runes.lsp
A books/kestrel/data/treeset/acl2-customization.lsp
A books/kestrel/data/treeset/benchmark/acl2-customization.lsp
A books/kestrel/data/treeset/benchmark/benchmark.lsp
A books/kestrel/data/treeset/benchmark/cert.acl2
A books/kestrel/data/treeset/benchmark/random.lisp
A books/kestrel/data/treeset/cardinality-defs.lisp
A books/kestrel/data/treeset/cardinality.lisp
A books/kestrel/data/treeset/cert.acl2
A books/kestrel/data/treeset/defs.lisp
A books/kestrel/data/treeset/delete-defs.lisp
A books/kestrel/data/treeset/delete.lisp
A books/kestrel/data/treeset/diff-defs.lisp
A books/kestrel/data/treeset/diff.lisp
A books/kestrel/data/treeset/doc.lisp
A books/kestrel/data/treeset/extensionality.lisp
A books/kestrel/data/treeset/fty.lisp
A books/kestrel/data/treeset/generic-typed-defs.lisp
A books/kestrel/data/treeset/generic-typed.lisp
A books/kestrel/data/treeset/hash-defs.lisp
A books/kestrel/data/treeset/hash.lisp
A books/kestrel/data/treeset/in-defs.lisp
A books/kestrel/data/treeset/in.lisp
A books/kestrel/data/treeset/induction.lisp
A books/kestrel/data/treeset/insert-defs.lisp
A books/kestrel/data/treeset/insert.lisp
A books/kestrel/data/treeset/internal/.sys/antisy...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/bst-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/b...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/count...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/co...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/delet...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/del...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/diff...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/di...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap-or...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/heap-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/he...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-ord...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/in-o...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/i...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/inser...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/ins...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/interse...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/inte...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/iter...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/it...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/join...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/jo...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/min-ma...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/min...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/rotat...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/rot...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/split...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/sp...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/subse...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/sub...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/tree...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/tr...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/union...@useless-runes.lsp
A books/kestrel/data/treeset/internal/.sys/un...@useless-runes.lsp
A books/kestrel/data/treeset/internal/acl2-customization.lsp
A books/kestrel/data/treeset/internal/antisymmetry.lisp
A books/kestrel/data/treeset/internal/bst-defs.lisp
A books/kestrel/data/treeset/internal/bst.lisp
A books/kestrel/data/treeset/internal/cert.acl2
A books/kestrel/data/treeset/internal/count-defs.lisp
A books/kestrel/data/treeset/internal/count.lisp
A books/kestrel/data/treeset/internal/delete-defs.lisp
A books/kestrel/data/treeset/internal/delete.lisp
A books/kestrel/data/treeset/internal/diff-defs.lisp
A books/kestrel/data/treeset/internal/diff.lisp
A books/kestrel/data/treeset/internal/doc.lisp
A books/kestrel/data/treeset/internal/heap-defs.lisp
A books/kestrel/data/treeset/internal/heap-order-defs.lisp
A books/kestrel/data/treeset/internal/heap-order.lisp
A books/kestrel/data/treeset/internal/heap.lisp
A books/kestrel/data/treeset/internal/in-defs.lisp
A books/kestrel/data/treeset/internal/in-order-defs.lisp
A books/kestrel/data/treeset/internal/in-order.lisp
A books/kestrel/data/treeset/internal/in.lisp
A books/kestrel/data/treeset/internal/insert-defs.lisp
A books/kestrel/data/treeset/internal/insert.lisp
A books/kestrel/data/treeset/internal/intersect-defs.lisp
A books/kestrel/data/treeset/internal/intersect.lisp
A books/kestrel/data/treeset/internal/iter-defs.lisp
A books/kestrel/data/treeset/internal/iter.lisp
A books/kestrel/data/treeset/internal/join-defs.lisp
A books/kestrel/data/treeset/internal/join.lisp
A books/kestrel/data/treeset/internal/min-max-defs.lisp
A books/kestrel/data/treeset/internal/min-max.lisp
A books/kestrel/data/treeset/internal/rotate-defs.lisp
A books/kestrel/data/treeset/internal/rotate.lisp
A books/kestrel/data/treeset/internal/split-defs.lisp
A books/kestrel/data/treeset/internal/split.lisp
A books/kestrel/data/treeset/internal/subset-defs.lisp
A books/kestrel/data/treeset/internal/subset.lisp
A books/kestrel/data/treeset/internal/tree-defs.lisp
A books/kestrel/data/treeset/internal/tree.lisp
A books/kestrel/data/treeset/internal/union-defs.lisp
A books/kestrel/data/treeset/internal/union.lisp
A books/kestrel/data/treeset/intersect-defs.lisp
A books/kestrel/data/treeset/intersect.lisp
A books/kestrel/data/treeset/iter-defs.lisp
A books/kestrel/data/treeset/iter.lisp
A books/kestrel/data/treeset/min-max-defs.lisp
A books/kestrel/data/treeset/min-max.lisp
A books/kestrel/data/treeset/package.lsp
A books/kestrel/data/treeset/portcullis.acl2
A books/kestrel/data/treeset/portcullis.lisp
A books/kestrel/data/treeset/set-defs.lisp
A books/kestrel/data/treeset/set.lisp
A books/kestrel/data/treeset/subset-defs.lisp
A books/kestrel/data/treeset/subset.lisp
A books/kestrel/data/treeset/to-oset-defs.lisp
A books/kestrel/data/treeset/to-oset.lisp
A books/kestrel/data/treeset/top.lisp
A books/kestrel/data/treeset/union-defs.lisp
A books/kestrel/data/treeset/union.lisp
A books/kestrel/data/utilities/.sys/list...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/li...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/nat-...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/n...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/oset...@useless-runes.lsp
A books/kestrel/data/utilities/.sys/os...@useless-runes.lsp
A books/kestrel/data/utilities/acl2-customization.lsp
A books/kestrel/data/utilities/bit-vectors/.sys/bitop...@useless-runes.lsp
A books/kestrel/data/utilities/bit-vectors/.sys/bit...@useless-runes.lsp
A books/kestrel/data/utilities/bit-vectors/acl2-customization.lsp
A books/kestrel/data/utilities/bit-vectors/bitops-defs.lisp
A books/kestrel/data/utilities/bit-vectors/bitops.lisp
A books/kestrel/data/utilities/bit-vectors/cert.acl2
A books/kestrel/data/utilities/cert.acl2
A books/kestrel/data/utilities/fixed-size-words/.sys/fix...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/.sys/u32-...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/.sys/u...@useless-runes.lsp
A books/kestrel/data/utilities/fixed-size-words/acl2-customization.lsp
A books/kestrel/data/utilities/fixed-size-words/cert.acl2
A books/kestrel/data/utilities/fixed-size-words/fixnum.lisp
A books/kestrel/data/utilities/fixed-size-words/u32-defs.lisp
A books/kestrel/data/utilities/fixed-size-words/u32.lisp
A books/kestrel/data/utilities/list-defs.lisp
A books/kestrel/data/utilities/list.lisp
A books/kestrel/data/utilities/oset-defs.lisp
A books/kestrel/data/utilities/oset.lisp
A books/kestrel/data/utilities/top.lisp
A books/kestrel/data/utilities/total-order/.sys/max-...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/min-...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/m...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/total-or...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/.sys/total...@useless-runes.lsp
A books/kestrel/data/utilities/total-order/acl2-customization.lsp
A books/kestrel/data/utilities/total-order/cert.acl2
A books/kestrel/data/utilities/total-order/max-defs.lisp
A books/kestrel/data/utilities/total-order/max.lisp
A books/kestrel/data/utilities/total-order/min-defs.lisp
A books/kestrel/data/utilities/total-order/min-max.lisp
A books/kestrel/data/utilities/total-order/min.lisp
A books/kestrel/data/utilities/total-order/total-order-defs.lisp
A books/kestrel/data/utilities/total-order/total-order.lisp
A books/kestrel/executable-parsers/.sys/elf-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/mach-o...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-e...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ex...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ma...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parsed-exec...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parser...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/pe-t...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/t...@useless-runes.lsp
A books/kestrel/executable-parsers/elf-tools.lisp
A books/kestrel/executable-parsers/mach-o-tools.lisp
A books/kestrel/executable-parsers/parse-elf-file.lisp
A books/kestrel/executable-parsers/parse-executable.lisp
A books/kestrel/executable-parsers/parse-mach-o-file.lisp
A books/kestrel/executable-parsers/parse-pe-file.lisp
A books/kestrel/executable-parsers/parsed-executable-tools.lisp
A books/kestrel/executable-parsers/parser-utils.lisp
A books/kestrel/executable-parsers/pe-tools.lisp
A books/kestrel/executable-parsers/top.lisp
M books/kestrel/fty/deffold-map-doc.lisp
A books/kestrel/executable-parsers/.sys/mach-o...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-e...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ex...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-ma...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parse-...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parsed-exec...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/parser...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/pe-t...@useless-runes.lsp
A books/kestrel/executable-parsers/.sys/t...@useless-runes.lsp
A books/kestrel/executable-parsers/elf-tools.lisp
A books/kestrel/executable-parsers/mach-o-tools.lisp
A books/kestrel/executable-parsers/parse-elf-file.lisp
A books/kestrel/executable-parsers/parse-executable.lisp
A books/kestrel/executable-parsers/parse-mach-o-file.lisp
A books/kestrel/executable-parsers/parse-pe-file.lisp
A books/kestrel/executable-parsers/parsed-executable-tools.lisp
A books/kestrel/executable-parsers/parser-utils.lisp
A books/kestrel/executable-parsers/pe-tools.lisp
A books/kestrel/executable-parsers/top.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/helpers/advice-implementation.lisp
M books/kestrel/helpers/advice-tests.lisp
A books/kestrel/helpers/defrule-tests.lisp
M books/kestrel/helpers/package.lsp
M books/kestrel/helpers/speed-up-implementation.lisp
M books/kestrel/json-parser/parsed-json.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/top-doc.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
M books/kestrel/top.lisp
R books/kestrel/treeset/.sys/binary-t...@useless-runes.lsp
R books/kestrel/treeset/.sys/binar...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-ord...@useless-runes.lsp
R books/kestrel/treeset/.sys/bst-...@useless-runes.lsp
R books/kestrel/treeset/.sys/b...@useless-runes.lsp
R books/kestrel/treeset/.sys/cardinal...@useless-runes.lsp
R books/kestrel/treeset/.sys/cardi...@useless-runes.lsp
R books/kestrel/treeset/.sys/de...@useless-runes.lsp
R books/kestrel/treeset/.sys/delet...@useless-runes.lsp
R books/kestrel/treeset/.sys/del...@useless-runes.lsp
R books/kestrel/treeset/.sys/diff...@useless-runes.lsp
R books/kestrel/treeset/.sys/di...@useless-runes.lsp
R books/kestrel/treeset/.sys/double-co...@useless-runes.lsp
R books/kestrel/treeset/.sys/f...@useless-runes.lsp
R books/kestrel/treeset/.sys/ha...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap-or...@useless-runes.lsp
R books/kestrel/treeset/.sys/heap-...@useless-runes.lsp
R books/kestrel/treeset/.sys/he...@useless-runes.lsp
R books/kestrel/treeset/.sys/in-...@useless-runes.lsp
R books/kestrel/treeset/.sys/i...@useless-runes.lsp
R books/kestrel/treeset/.sys/inser...@useless-runes.lsp
R books/kestrel/treeset/.sys/ins...@useless-runes.lsp
R books/kestrel/treeset/.sys/interse...@useless-runes.lsp
R books/kestrel/treeset/.sys/inte...@useless-runes.lsp
R books/kestrel/treeset/.sys/jenkin...@useless-runes.lsp
R books/kestrel/treeset/.sys/join...@useless-runes.lsp
R books/kestrel/treeset/.sys/jo...@useless-runes.lsp
R books/kestrel/treeset/.sys/pick-a...@useless-runes.lsp
R books/kestrel/treeset/.sys/portc...@useless-runes.lsp
R books/kestrel/treeset/.sys/rotat...@useless-runes.lsp
R books/kestrel/treeset/.sys/rot...@useless-runes.lsp
R books/kestrel/treeset/.sys/set-...@useless-runes.lsp
R books/kestrel/treeset/.sys/s...@useless-runes.lsp
R books/kestrel/treeset/.sys/split...@useless-runes.lsp
R books/kestrel/treeset/.sys/sp...@useless-runes.lsp
R books/kestrel/treeset/.sys/subse...@useless-runes.lsp
R books/kestrel/treeset/.sys/sub...@useless-runes.lsp
R books/kestrel/treeset/.sys/sum-acl2-...@useless-runes.lsp
R books/kestrel/treeset/.sys/sum-acl...@useless-runes.lsp
R books/kestrel/treeset/.sys/t...@useless-runes.lsp
R books/kestrel/treeset/.sys/total...@useless-runes.lsp
R books/kestrel/treeset/.sys/union...@useless-runes.lsp
R books/kestrel/treeset/.sys/un...@useless-runes.lsp
R books/kestrel/treeset/acl2-customization.lsp
R books/kestrel/treeset/binary-tree-defs.lisp
R books/kestrel/treeset/binary-tree.lisp
R books/kestrel/treeset/bst-defs.lisp
R books/kestrel/treeset/bst-order-defs.lisp
R books/kestrel/treeset/bst-order.lisp
R books/kestrel/treeset/bst.lisp
R books/kestrel/treeset/cardinality-defs.lisp
R books/kestrel/treeset/cardinality.lisp
R books/kestrel/treeset/cert.acl2
R books/kestrel/treeset/defs.lisp
R books/kestrel/treeset/delete-defs.lisp
R books/kestrel/treeset/delete.lisp
R books/kestrel/treeset/diff-defs.lisp
R books/kestrel/treeset/diff.lisp
R books/kestrel/treeset/double-containment.lisp
R books/kestrel/treeset/fty.lisp
R books/kestrel/treeset/hash.lisp
R books/kestrel/treeset/heap-defs.lisp
R books/kestrel/treeset/heap-order-defs.lisp
R books/kestrel/treeset/heap-order.lisp
R books/kestrel/treeset/heap.lisp
R books/kestrel/treeset/in-defs.lisp
R books/kestrel/treeset/in.lisp
R books/kestrel/treeset/insert-defs.lisp
R books/kestrel/treeset/insert.lisp
R books/kestrel/treeset/intersect-defs.lisp
R books/kestrel/treeset/intersect.lisp
R books/kestrel/treeset/jenkins-hash.lisp
R books/kestrel/treeset/join-defs.lisp
R books/kestrel/treeset/join.lisp
R books/kestrel/treeset/package.lsp
R books/kestrel/treeset/pick-a-point.lisp
R books/kestrel/treeset/portcullis.acl2
R books/kestrel/treeset/portcullis.lisp
R books/kestrel/treeset/rotate-defs.lisp
R books/kestrel/treeset/rotate.lisp
R books/kestrel/treeset/set-defs.lisp
R books/kestrel/treeset/set.lisp
R books/kestrel/treeset/split-defs.lisp
R books/kestrel/treeset/split.lisp
R books/kestrel/treeset/subset-defs.lisp
R books/kestrel/treeset/subset.lisp
R books/kestrel/treeset/sum-acl2-count-defs.lisp
R books/kestrel/treeset/sum-acl2-count.lisp
R books/kestrel/treeset/tests/.sys/mk-r...@useless-runes.lsp
R books/kestrel/treeset/tests/.sys/mk-...@useless-runes.lsp
R books/kestrel/treeset/tests/.sys/time...@useless-runes.lsp
R books/kestrel/treeset/tests/acl2-customization.lsp
R books/kestrel/treeset/tests/cert.acl2
R books/kestrel/treeset/tests/mk-random.lisp
R books/kestrel/treeset/tests/mk-set.lisp
R books/kestrel/treeset/tests/tests.lsp
R books/kestrel/treeset/tests/time-set.lisp
R books/kestrel/treeset/top.lisp
R books/kestrel/treeset/total-order.lisp
R books/kestrel/treeset/union-defs.lisp
R books/kestrel/treeset/union.lisp
M books/kestrel/utilities/ld-history.lisp
M books/kestrel/utilities/redundancy.lisp
M books/kestrel/utilities/run-json-command.lisp
M books/kestrel/utilities/verify-guards-program-tests.lisp
M books/kestrel/utilities/verify-guards-program.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/assumptions64.lisp
M books/kestrel/x86/package.lsp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/assumptions64.lisp
R books/kestrel/x86/parsers/.sys/elf-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/mach-o...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-e...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ex...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ma...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parsed-exec...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parser...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/pe-t...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/t...@useless-runes.lsp
R books/kestrel/x86/parsers/elf-tools.lisp
R books/kestrel/x86/parsers/mach-o-tools.lisp
R books/kestrel/x86/parsers/parse-elf-file.lisp
R books/kestrel/x86/parsers/parse-executable.lisp
R books/kestrel/x86/parsers/parse-mach-o-file.lisp
R books/kestrel/x86/parsers/parse-pe-file.lisp
R books/kestrel/x86/parsers/parsed-executable-tools.lisp
R books/kestrel/x86/parsers/parser-utils.lisp
R books/kestrel/x86/parsers/pe-tools.lisp
R books/kestrel/x86/parsers/top.lisp
M books/kestrel/x86/tools/lifter-support.lisp
R books/kestrel/x86/parsers/.sys/mach-o...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-e...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ex...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-ma...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parse-...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parsed-exec...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/parser...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/pe-t...@useless-runes.lsp
R books/kestrel/x86/parsers/.sys/t...@useless-runes.lsp
R books/kestrel/x86/parsers/elf-tools.lisp
R books/kestrel/x86/parsers/mach-o-tools.lisp
R books/kestrel/x86/parsers/parse-elf-file.lisp
R books/kestrel/x86/parsers/parse-executable.lisp
R books/kestrel/x86/parsers/parse-mach-o-file.lisp
R books/kestrel/x86/parsers/parse-pe-file.lisp
R books/kestrel/x86/parsers/parsed-executable-tools.lisp
R books/kestrel/x86/parsers/parser-utils.lisp
R books/kestrel/x86/parsers/pe-tools.lisp
R books/kestrel/x86/parsers/top.lisp
M books/kestrel/x86/tools/unroll-x86-code-old.lisp
M books/kestrel/x86/top.lisp
R books/kestrel/x86/x86-changes.acl2
M books/kestrel/x86/x86-changes.lisp
M books/projects/hol-in-acl2/README
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
M books/projects/hol-in-acl2/acl2/package.lsp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
M books/projects/hol-in-acl2/acl2/theories.lisp
R books/projects/hol-in-acl2/examples/README
A books/projects/hol-in-acl2/examples/README.txt
M books/projects/hol-in-acl2/examples/eval-poly-proof.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy-exports.lisp
M books/projects/hol-in-acl2/examples/eval-poly-thy.lisp
M books/projects/hol-in-acl2/examples/eval-poly-top.lisp
A books/projects/hol-in-acl2/examples/eval_poly.defhol
A books/projects/hol-in-acl2/examples/eval_polyScript.sml
M books/projects/hol-in-acl2/examples/ex1-proof.lisp
M books/projects/hol-in-acl2/examples/ex1-thy-exports.lisp
M books/projects/hol-in-acl2/examples/ex1-thy.lisp
M books/projects/hol-in-acl2/examples/ex1-top.lisp
A books/projects/hol-in-acl2/examples/ex1.defhol
A books/projects/hol-in-acl2/examples/ex1Script.sml
R books/projects/hol-in-acl2/hol4/eval-poly.sml
R books/projects/hol-in-acl2/hol4/ex1.sml
R books/projects/hol-in-acl2/hol4/translator.sml
M books/projects/hol-in-acl2/to-do.txt
M books/projects/vescmul/int-vector-adders-meta.lisp
M books/projects/x86isa/machine/cert.acl2
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/other-non-det.lisp
M books/projects/x86isa/machine/paging.acl2
M books/projects/x86isa/machine/physical-memory.acl2
M books/projects/x86isa/machine/prefix-modrm-sib-decoding.acl2
M books/projects/x86isa/machine/register-readers-and-writers-raw.lsp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/tools/execution/top.lisp
M books/std/strings/bin-digit-char-listp.lisp
M books/std/strings/dec-digit-char-listp.lisp
M books/std/strings/hex-digit-char-listp.lisp
M books/std/strings/oct-digit-char-listp.lisp
M books/std/util/defaggregate.lisp
M books/std/util/defprojection.lisp
M books/std/util/defrule.lisp
M books/std/util/tests/defaggregate.lisp
M books/system/doc/acl2-doc.lisp
A books/tools/eval-events-from-file-doc.lisp
A books/tools/eval-events-from-file-test-data.lsp
A books/tools/eval-events-from-file-test.lisp
A books/tools/eval-events-from-file.lisp
M books/tools/top.lisp
M books/tools/with-supporters-doc.lisp
M books/tools/with-supporters.lisp
M books/xdoc/display.lisp
M defthm.lisp
M defuns.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp
M other-events.lisp
M proof-builder-b.lisp
Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/master' into testing-acl2s
Commit: 4d8e886d5429c845772acb31343190d0dd8916b9
https://github.com/acl2/acl2/commit/4d8e886d5429c845772acb31343190d0dd8916b9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
-----------
[C$] Improve preprocessor implementation.
Make the maximum macro reach part of the stobj.
Commit: bc13f6577e0cebed432ea0ce8929603d2e542dde
https://github.com/acl2/acl2/commit/bc13f6577e0cebed432ea0ce8929603d2e542dde
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
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 'f1215b5012c66da463b258e2e2eb2b6e3427af68' into HEAD
Commit: 9983ebdf1a551b55f3b91a5234f31cdf51223ade
https://github.com/acl2/acl2/commit/9983ebdf1a551b55f3b91a5234f31cdf51223ade
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
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
Log Message:
-----------
Small updates to eval_poly example of hol-in-acl2 project
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
Log Message:
-----------
Commit: 57a866ed42bcbf2f363d132b906b297c16583feb
https://github.com/acl2/acl2/commit/57a866ed42bcbf2f363d132b906b297c16583feb
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Update some doc.
Commit: 837f6f84bd078f649a0bca1bd411eed507db75d5
https://github.com/acl2/acl2/commit/837f6f84bd078f649a0bca1bd411eed507db75d5
Author: ACL2 Build Server <acl2bui...@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/.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/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/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:
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
-----------
Merge commit 'f837cd4a60a48c40ff73c03461b857ce306953da' into HEAD
Commit: 7f0bb469e4404dfbbc830a0979682ea3d12fa882
https://github.com/acl2/acl2/commit/7f0bb469e4404dfbbc830a0979682ea3d12fa882
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Add file dependencies to preprocessor tests.
Commit: 5705fc5abfb60ca3c9309c693290fed5977f6cfc
https://github.com/acl2/acl2/commit/5705fc5abfb60ca3c9309c693290fed5977f6cfc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-06 (Fri, 06 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
-----------
[C$] Extend preprocessor to track header guard state.
This is used to recognize whether a file has the header guard form.
We still need to make use of this information.
Commit: 139a07a6b96f4631118c6aab917a2439d8e00703
https://github.com/acl2/acl2/commit/139a07a6b96f4631118c6aab917a2439d8e00703
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-07 (Sat, 07 Feb 2026)
Changed paths:
M books/acl2s/cgen/callback.lisp
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/.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/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/split-gso.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/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
M books/kestrel/c/transformation/utilities/add-attributes.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
M books/kestrel/c/transformation/utilities/add-attributes.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
Log Message:
-----------
Merge.
Commit: d3690e62efa47d116a4d6321e8a7061c336fd5c0
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
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/d3690e62efa47d116a4d6321e8a7061c336fd5c0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-07 (Sat, 07 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
-----------
[C$] Accumulate output lexemes in preprocessor states.
This simplifies some code, and also enabled an upcoming more elaborate
collection of output lexemes.
Commit: e8022dad27584f564acb631c309a71e5eb6702d7
https://github.com/acl2/acl2/commit/e8022dad27584f564acb631c309a71e5eb6702d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-07 (Sat, 07 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
Reorganize the collected output lexemes into chunks related to the header guard
structure. When the file has the header guard structure, also output the
directives in question.
Adjust some test expectations.
Reply all
Reply to author
Forward
0 new messages