[acl2/acl2] 44fde6: [axe] Improve redundancy machinery and uses of val...
0 views
Skip to first unread message
Eric W. Smith
Feb 5, 2026, 6:31:10 PM (5 days ago) Feb 5
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 44fde69b955a79e3e74af12840569b60591fb9a1
https://github.com/acl2/acl2/commit/44fde69b955a79e3e74af12840569b60591fb9a1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/axe/def-simplified.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/make-rewriter-simple.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
Log Message:
-----------
[axe] Improve redundancy machinery and uses of value-triple.
Commit: c66fac4689c96e137caa20ca95081704b7d1f3bf
https://github.com/acl2/acl2/commit/c66fac4689c96e137caa20ca95081704b7d1f3bf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
[axe/x86] Add rule.
Commit: 908f0e8bc41200a42d2b4acef87de7eb71a8f0aa
https://github.com/acl2/acl2/commit/908f0e8bc41200a42d2b4acef87de7eb71a8f0aa
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/x86/unroller.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
Log Message:
-----------
[lists-light] Split out set-difference-eq-fast.
Also improve it and add set-difference-equal-fast.
Commit: 88b62cab65427dbebbb366760d12a22e28ad73d3
https://github.com/acl2/acl2/commit/88b62cab65427dbebbb366760d12a22e28ad73d3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/arm/package.lsp
M books/kestrel/arm/step.lisp
Log Message:
-----------
[arm] Tweaks.
Commit: c88e41ed75df99473adfe70dd8513ce51cb9735d
https://github.com/acl2/acl2/commit/c88e41ed75df99473adfe70dd8513ce51cb9735d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/lists-light/top.lisp
Log Message:
-----------
[lists-light] Update copyright year.
Commit: b7ccffebe457f9572c6cb634f144ddb26a17150f
https://github.com/acl2/acl2/commit/b7ccffebe457f9572c6cb634f144ddb26a17150f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/arm/instructions.lisp
Log Message:
-----------
[arm] Add missing comments.
Commit: 40c0e2ce5064af8fddb0c5877e235009379103fb
https://github.com/acl2/acl2/commit/40c0e2ce5064af8fddb0c5877e235009379103fb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
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/preprocessor-evaluator.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/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/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
Log Message:
-----------
Merge.
Commit: a9a6e94bc063aa8a6724e10fb612b3ddfa29a0ac
https://github.com/acl2/acl2/commit/a9a6e94bc063aa8a6724e10fb612b3ddfa29a0ac
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/risc-v/unroller.lisp
Log Message:
-----------
[axe/risc-v] Clean up a bit.
Commit: e64071624d858c8856d6de20c4470ffa11ac5ae7
https://github.com/acl2/acl2/commit/e64071624d858c8856d6de20c4470ffa11ac5ae7
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
[axe/x86] Add more checking of ELF files.
Commit: cebcc6d709b6572b0bfd8eb8fb63b7533a1780eb
https://github.com/acl2/acl2/commit/cebcc6d709b6572b0bfd8eb8fb63b7533a1780eb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
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/wrappers.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/json-parser/parsed-json.lisp
Log Message:
-----------
Merge.
Commit: b142871cb89c5829808ea9d2efe72b4231a6e212
https://github.com/acl2/acl2/commit/b142871cb89c5829808ea9d2efe72b4231a6e212
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/x86/parsers/top.lisp
Log Message:
-----------
[parsers] Document a bit.
Commit: e455d0a0cee88ebf010d50b25083d88ee9f39463
https://github.com/acl2/acl2/commit/e455d0a0cee88ebf010d50b25083d88ee9f39463
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/support-non-axe.lisp
M books/kestrel/axe/risc-v/unroller.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
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/top.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
Log Message:
-----------
[executable-parsers] Move the parsers out books/kestrel/x86/.
These are not x86-specific, so I moved them to a new directory, books/kestrel/executable-parsers/.
Commit: 961375ef9db599decd489aa75ecca35ac13b9959
https://github.com/acl2/acl2/commit/961375ef9db599decd489aa75ecca35ac13b9959
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/a2035904bac1...961375ef9db5
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 44fde69b955a79e3e74af12840569b60591fb9a1
https://github.com/acl2/acl2/commit/44fde69b955a79e3e74af12840569b60591fb9a1
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/axe/def-simplified.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/make-rewriter-simple.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/unroll-spec-basic.lisp
M books/kestrel/axe/unroll-spec.lisp
Log Message:
-----------
[axe] Improve redundancy machinery and uses of value-triple.
Commit: c66fac4689c96e137caa20ca95081704b7d1f3bf
https://github.com/acl2/acl2/commit/c66fac4689c96e137caa20ca95081704b7d1f3bf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
[axe/x86] Add rule.
Commit: 908f0e8bc41200a42d2b4acef87de7eb71a8f0aa
https://github.com/acl2/acl2/commit/908f0e8bc41200a42d2b4acef87de7eb71a8f0aa
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/x86/unroller.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
Log Message:
-----------
[lists-light] Split out set-difference-eq-fast.
Also improve it and add set-difference-equal-fast.
Commit: 88b62cab65427dbebbb366760d12a22e28ad73d3
https://github.com/acl2/acl2/commit/88b62cab65427dbebbb366760d12a22e28ad73d3
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/arm/package.lsp
M books/kestrel/arm/step.lisp
Log Message:
-----------
[arm] Tweaks.
Commit: c88e41ed75df99473adfe70dd8513ce51cb9735d
https://github.com/acl2/acl2/commit/c88e41ed75df99473adfe70dd8513ce51cb9735d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/lists-light/top.lisp
Log Message:
-----------
[lists-light] Update copyright year.
Commit: b7ccffebe457f9572c6cb634f144ddb26a17150f
https://github.com/acl2/acl2/commit/b7ccffebe457f9572c6cb634f144ddb26a17150f
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-04 (Wed, 04 Feb 2026)
Changed paths:
M books/kestrel/arm/instructions.lisp
Log Message:
-----------
[arm] Add missing comments.
Commit: 40c0e2ce5064af8fddb0c5877e235009379103fb
https://github.com/acl2/acl2/commit/40c0e2ce5064af8fddb0c5877e235009379103fb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
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/preprocessor-evaluator.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/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/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
A books/projects/hol-in-acl2/acl2/hpp-set.lisp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
Log Message:
-----------
Merge.
Commit: a9a6e94bc063aa8a6724e10fb612b3ddfa29a0ac
https://github.com/acl2/acl2/commit/a9a6e94bc063aa8a6724e10fb612b3ddfa29a0ac
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/risc-v/unroller.lisp
Log Message:
-----------
[axe/risc-v] Clean up a bit.
Commit: e64071624d858c8856d6de20c4470ffa11ac5ae7
https://github.com/acl2/acl2/commit/e64071624d858c8856d6de20c4470ffa11ac5ae7
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
[axe/x86] Add more checking of ELF files.
Commit: cebcc6d709b6572b0bfd8eb8fb63b7533a1780eb
https://github.com/acl2/acl2/commit/cebcc6d709b6572b0bfd8eb8fb63b7533a1780eb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
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/wrappers.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/json-parser/parsed-json.lisp
Log Message:
-----------
Merge.
Commit: b142871cb89c5829808ea9d2efe72b4231a6e212
https://github.com/acl2/acl2/commit/b142871cb89c5829808ea9d2efe72b4231a6e212
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/x86/parsers/top.lisp
Log Message:
-----------
[parsers] Document a bit.
Commit: e455d0a0cee88ebf010d50b25083d88ee9f39463
https://github.com/acl2/acl2/commit/e455d0a0cee88ebf010d50b25083d88ee9f39463
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/support-non-axe.lisp
M books/kestrel/axe/risc-v/unroller.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
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/top.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
Log Message:
-----------
[executable-parsers] Move the parsers out books/kestrel/x86/.
These are not x86-specific, so I moved them to a new directory, books/kestrel/executable-parsers/.
Commit: 961375ef9db599decd489aa75ecca35ac13b9959
https://github.com/acl2/acl2/commit/961375ef9db599decd489aa75ecca35ac13b9959
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/a2035904bac1...961375ef9db5
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Eric W. Smith
Feb 5, 2026, 9:45:25 PM (5 days ago) Feb 5
to acl2-...@googlegroups.com
Branch: refs/heads/master
Eric W. Smith
Feb 5, 2026, 9:46:33 PM (5 days ago) Feb 5
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Feb 5, 2026, 11:48:16 PM (5 days ago) Feb 5
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: aec9711b355460b95603d36c4bcfb41f3a940eaf
https://github.com/acl2/acl2/commit/aec9711b355460b95603d36c4bcfb41f3a940eaf
M books/kestrel/c/transformation/simpadd0-doc.lisp
Log Message:
-----------
[C2C] Add missing space in doc.
Commit: 3b414852efb839dd518f830546aa164e75848df2
https://github.com/acl2/acl2/commit/3b414852efb839dd518f830546aa164e75848df2
https://github.com/acl2/acl2/commit/be3e624287f2f9bacacf9198842b413a542b9739
M books/kestrel/json-parser/parsed-json.lisp
Log Message:
-----------
[json-parser] Add some operations on parsed-json-objects.
Commit: 375d525b7577356e87e38d15937da345987f62d5
https://github.com/acl2/acl2/commit/375d525b7577356e87e38d15937da345987f62d5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Remove local theorem no longer needed.
Commit: be6e4cc06bafcf4744ec33d62e19fce58f2cfd47
https://github.com/acl2/acl2/commit/be6e4cc06bafcf4744ec33d62e19fce58f2cfd47
Author: Grant Jurgensen <gr...@jurgensen.dev>
Log Message:
-----------
[C2C] Fix name of add-section-attr keyword argument
Thanks to Eric Smith for noticing the name in the XDOC was different
from the actual expected name.
Commit: ec5ec43bc8719f2045a66752955914f174be93a4
https://github.com/acl2/acl2/commit/ec5ec43bc8719f2045a66752955914f174be93a4
Author: Grant Jurgensen <gr...@jurgensen.dev>
Log Message:
-----------
[C2C] Add add-section-attr test case
Commit: 3c075a8dbd16130a6f78ffbcd44f830c5dde764a
https://github.com/acl2/acl2/commit/3c075a8dbd16130a6f78ffbcd44f830c5dde764a
M books/kestrel/c/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
Log Message:
-----------
Merge.
Commit: 06e787f9bf93330206699045d6281e5a0d819ef6
https://github.com/acl2/acl2/commit/06e787f9bf93330206699045d6281e5a0d819ef6
-----------
[C2C] Add command-line wrapper for add-section-attr transformation.
Commit: 91cd0157442919f30af9f7ad74a7ada0c199d9af
https://github.com/acl2/acl2/commit/91cd0157442919f30af9f7ad74a7ada0c199d9af
Author: Grant Jurgensen <gr...@jurgensen.dev>
A books/kestrel/c/transformation/command-line/tests/input-files/file11.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
Log Message:
-----------
[C2C] Add a command-line add-section-attr test
Commit: cebcc6d709b6572b0bfd8eb8fb63b7533a1780eb
https://github.com/acl2/acl2/commit/cebcc6d709b6572b0bfd8eb8fb63b7533a1780eb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
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/wrappers.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/json-parser/parsed-json.lisp
Log Message:
-----------
Merge.
Commit: 7666f70fabf7392672445242fc2f70190b3960ff
https://github.com/acl2/acl2/commit/7666f70fabf7392672445242fc2f70190b3960ff
Author: Alessandro Coglio <em...@alessandrocoglio.info>
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Have macro lookup return 'reach'.
This will support a more nuanced way to check for self-contained files.
Commit: b142871cb89c5829808ea9d2efe72b4231a6e212
https://github.com/acl2/acl2/commit/b142871cb89c5829808ea9d2efe72b4231a6e212
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/x86/parsers/top.lisp
Log Message:
-----------
[parsers] Document a bit.
Commit: a2035904bac1b4e6275faabf5398a28ad57566b0
https://github.com/acl2/acl2/commit/a2035904bac1b4e6275faabf5398a28ad57566b0
Author: Grant Jurgensen <gr...@jurgensen.dev>
This is similar to the previous UID bug. Function definitions were not
always reusing UIDs as they should.
Commit: 7b3247e04871dc472d4aa23174a325d368709f62
https://github.com/acl2/acl2/commit/7b3247e04871dc472d4aa23174a325d368709f62
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Track maximum macro reach during preprocessing.
Commit: 961375ef9db599decd489aa75ecca35ac13b9959
https://github.com/acl2/acl2/commit/961375ef9db599decd489aa75ecca35ac13b9959
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
Merge.
Commit: ad2b433146a23999ad649b504efdcf35ae97ce5b
https://github.com/acl2/acl2/commit/ad2b433146a23999ad649b504efdcf35ae97ce5b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Return max macro reach from `pproc-file`.
Commit: 187db0869b1cd6bd73b37179bd728ea2586d0b4d
https://github.com/acl2/acl2/commit/187db0869b1cd6bd73b37179bd728ea2586d0b4d
Log Message:
-----------
[axe/x86] Split out position-independent check for ELF files.
Commit: 932a3459b62161cb8cf90760cf798c8dc6528f85
https://github.com/acl2/acl2/commit/932a3459b62161cb8cf90760cf798c8dc6528f85
Commit: 80b534e2b0738e96580859a097af44d897bfad38
https://github.com/acl2/acl2/commit/80b534e2b0738e96580859a097af44d897bfad38
M books/kestrel/axe/imported-symbols.lisp
Log Message:
-----------
[axe] Extend list of imported symbols.
Commit: 0031f784c5607b006ddc1d935b33893e05741035
https://github.com/acl2/acl2/commit/0031f784c5607b006ddc1d935b33893e05741035
Commit: 3c3902a351fe33e7bebad3ef30501a5d5e02a701
https://github.com/acl2/acl2/commit/3c3902a351fe33e7bebad3ef30501a5d5e02a701
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Improve and simplify preprocessor.
Eliminate the `not-self-contained-p` flag, using the max reach instead. Also, do
not treat max reach > 0 as an exception, but instead continue preprocessing the
file.
Commit: 3924a355b89b6b66167c564ac54c3b6d3b15088a
https://github.com/acl2/acl2/commit/3924a355b89b6b66167c564ac54c3b6d3b15088a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Improve handling of non-self-contained files.
Instead of adding the bytes of the included file to the stobj, use directly
the lexemes coming from the attempt to preprocess the file as self-contained,
which would be the same lexemes anyhow.
Although the C standard is not super-clear about the level at which included
files are expanded in place (byte level, character level, or lexical level), the
syntax of the `#include` directive suggests that the lexical level is the right
one. In some contrived cases, Clang and GCC exhibit some strange (and not
mutually consistent) behaviors that do not quite match that interpretation, but
that still seems the right interpretation.
Commit: f8111fd1b5fa3ea69278f70766be671d3136caa7
https://github.com/acl2/acl2/commit/f8111fd1b5fa3ea69278f70766be671d3136caa7
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/unroller.lisp
Generate the repeatedly-run function from a template.
Commit: b407e741815b821326c6cacd1097c5632d29ae05
https://github.com/acl2/acl2/commit/b407e741815b821326c6cacd1097c5632d29ae05
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Log Message:
-----------
[C$] Streamline some preprocessor code.
Have `pproc-file` return a (reversed) list of lexemes and a macro scope, not
packaged into an `scfile`, and do not extend the `preprocessed` alist there.
Let the callers do all of that, if the file is self-contained; if it is not,
the lexemes and macros are used in a different way.
Commit: 712aeecaa6c75c47be2f4992d1e6e56353f0a797
https://github.com/acl2/acl2/commit/712aeecaa6c75c47be2f4992d1e6e56353f0a797
Author: Alessandro Coglio <em...@alessandrocoglio.info>
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Use logical integer fixer in executable code.
Commit: e597f9881ae630e61ef891c75f4ba8f210ca0738
https://github.com/acl2/acl2/commit/e597f9881ae630e61ef891c75f4ba8f210ca0738
Author: Alessandro Coglio <em...@alessandrocoglio.info>
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Simplify a data structure.
We do not need to have a `macros` component in `scfile`, after some code changes
we have made.
Commit: d2512b28f7657b7f9a4e8e655ab3119cad637b29
https://github.com/acl2/acl2/commit/d2512b28f7657b7f9a4e8e655ab3119cad637b29
Author: Alessandro Coglio <em...@alessandrocoglio.info>
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/c/syntax/validator.lisp
M books/kestrel/c/transformation/add-section-attr-doc.lisp
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
Merge.
Commit: 0d5727f68082c562e5e0ba10ef358f0d1314b3d4
https://github.com/acl2/acl2/commit/0d5727f68082c562e5e0ba10ef358f0d1314b3d4
M books/kestrel/axe/step-increments.lisp
Log Message:
-----------
[axe] Improve comment.
Commit: 382b9ebac8877837600264d54ec0af3fe00b13c1
https://github.com/acl2/acl2/commit/382b9ebac8877837600264d54ec0af3fe00b13c1
M books/kestrel/axe/rule-limits.lisp
Log Message:
-----------
[axe] Add a rule.
Commit: 5b959374c2c16281f04bc58a278d0e7fe71096b1
https://github.com/acl2/acl2/commit/5b959374c2c16281f04bc58a278d0e7fe71096b1
M books/kestrel/axe/risc-v/rule-lists.lisp
Commit: ade645ebcea7e92a7819ec13d22179ffacf22a71
https://github.com/acl2/acl2/commit/ade645ebcea7e92a7819ec13d22179ffacf22a71
Author: Alessandro Coglio <em...@alessandrocoglio.info>
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.lisp
Log Message:
-----------
[C$] Add a preprocessor test with header guards.
Not quite doing what we want just yet, but getting there.
Commit: f1282125f26638942eb5f0da51ba98740ad8e078
https://github.com/acl2/acl2/commit/f1282125f26638942eb5f0da51ba98740ad8e078
M books/kestrel/axe/lifter-common.lisp
Log Message:
-----------
[axe] Fix/improve step counting and printing.
Commit: 8c7f09bd438f3aca2e9e2c516993f4ace993e59a
https://github.com/acl2/acl2/commit/8c7f09bd438f3aca2e9e2c516993f4ace993e59a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
Log Message:
-----------
[C$] Simplify preprocessor stobj.
Now that we are handling included file expansion (when not self-contained) at
the lexical level, we no longer need the array of byte sequences.
Commit: 41dd9ee939c5cfdd2ba7606f4307752088fc7451
https://github.com/acl2/acl2/commit/41dd9ee939c5cfdd2ba7606f4307752088fc7451
Author: Alessandro Coglio <em...@alessandrocoglio.info>
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-limits.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/executable-parsers/elf-tools.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/6356fc47b78c...41dd9ee939c5
https://github.com/acl2/acl2/commit/aec9711b355460b95603d36c4bcfb41f3a940eaf
M books/kestrel/c/transformation/simpadd0-doc.lisp
Log Message:
-----------
[C2C] Add missing space in doc.
Commit: 3b414852efb839dd518f830546aa164e75848df2
https://github.com/acl2/acl2/commit/3b414852efb839dd518f830546aa164e75848df2
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/preprocessor-evaluator.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/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/input-files.lisp
M books/kestrel/c/syntax/macro-tables.lisp
M books/kestrel/c/syntax/preprocessor-evaluator.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/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/projects/hol-in-acl2/acl2/hpp-set.lisp
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
Log Message:
-----------
Merge.
Commit: be3e624287f2f9bacacf9198842b413a542b9739
R books/projects/hol-in-acl2/acl2/set-of-hol-values.lisp
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/be3e624287f2f9bacacf9198842b413a542b9739
M books/kestrel/json-parser/parsed-json.lisp
Log Message:
-----------
[json-parser] Add some operations on parsed-json-objects.
Commit: 375d525b7577356e87e38d15937da345987f62d5
https://github.com/acl2/acl2/commit/375d525b7577356e87e38d15937da345987f62d5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
Changed paths:
Log Message:
-----------
[C$] Remove local theorem no longer needed.
Commit: be6e4cc06bafcf4744ec33d62e19fce58f2cfd47
https://github.com/acl2/acl2/commit/be6e4cc06bafcf4744ec33d62e19fce58f2cfd47
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/transformation/add-section-attr-doc.lisp
Changed paths:
Log Message:
-----------
[C2C] Fix name of add-section-attr keyword argument
Thanks to Eric Smith for noticing the name in the XDOC was different
from the actual expected name.
Commit: ec5ec43bc8719f2045a66752955914f174be93a4
https://github.com/acl2/acl2/commit/ec5ec43bc8719f2045a66752955914f174be93a4
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
Changed paths:
Log Message:
-----------
[C2C] Add add-section-attr test case
Commit: 3c075a8dbd16130a6f78ffbcd44f830c5dde764a
https://github.com/acl2/acl2/commit/3c075a8dbd16130a6f78ffbcd44f830c5dde764a
M books/kestrel/c/transformation/add-section-attr-doc.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
Log Message:
-----------
Merge.
Commit: 06e787f9bf93330206699045d6281e5a0d819ef6
https://github.com/acl2/acl2/commit/06e787f9bf93330206699045d6281e5a0d819ef6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
A books/kestrel/c/transformation/command-line/tests/add-section-attr.json
A books/kestrel/c/transformation/command-line/tests/input-files/file10.c
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
A books/kestrel/c/transformation/command-line/tests/add-section-attr.json
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/wrappers.lisp
Log Message:
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
M books/kestrel/c/transformation/command-line/wrappers.lisp
-----------
[C2C] Add command-line wrapper for add-section-attr transformation.
https://github.com/acl2/acl2/commit/91cd0157442919f30af9f7ad74a7ada0c199d9af
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
A books/kestrel/c/transformation/command-line/tests/add-section-attr2.json
Changed paths:
A books/kestrel/c/transformation/command-line/tests/input-files/file11.c
M books/kestrel/c/transformation/command-line/tests/run-tests.sh
Log Message:
-----------
[C2C] Add a command-line add-section-attr test
Commit: cebcc6d709b6572b0bfd8eb8fb63b7533a1780eb
https://github.com/acl2/acl2/commit/cebcc6d709b6572b0bfd8eb8fb63b7533a1780eb
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
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/wrappers.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/json-parser/parsed-json.lisp
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/7666f70fabf7392672445242fc2f70190b3960ff
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/macro-tables.lisp
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Log Message:
-----------
[C$] Have macro lookup return 'reach'.
This will support a more nuanced way to check for self-contained files.
Commit: b142871cb89c5829808ea9d2efe72b4231a6e212
https://github.com/acl2/acl2/commit/b142871cb89c5829808ea9d2efe72b4231a6e212
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/x86/parsers/top.lisp
Log Message:
-----------
[parsers] Document a bit.
https://github.com/acl2/acl2/commit/a2035904bac1b4e6275faabf5398a28ad57566b0
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
[C$] Fix validator UID bug
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
This is similar to the previous UID bug. Function definitions were not
always reusing UIDs as they should.
https://github.com/acl2/acl2/commit/7b3247e04871dc472d4aa23174a325d368709f62
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Changed paths:
Log Message:
-----------
[C$] Track maximum macro reach during preprocessing.
Commit: 961375ef9db599decd489aa75ecca35ac13b9959
https://github.com/acl2/acl2/commit/961375ef9db599decd489aa75ecca35ac13b9959
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/ad2b433146a23999ad649b504efdcf35ae97ce5b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Changed paths:
Log Message:
-----------
[C$] Return max macro reach from `pproc-file`.
Commit: 187db0869b1cd6bd73b37179bd728ea2586d0b4d
https://github.com/acl2/acl2/commit/187db0869b1cd6bd73b37179bd728ea2586d0b4d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/executable-parsers/elf-tools.lisp
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
[axe/x86] Split out position-independent check for ELF files.
Commit: 932a3459b62161cb8cf90760cf798c8dc6528f85
https://github.com/acl2/acl2/commit/932a3459b62161cb8cf90760cf798c8dc6528f85
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/risc-v/unroller.lisp
Log Message:
-----------
[axe/risc-v] Add support for :position-independent :auto.
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/risc-v/unroller.lisp
Log Message:
-----------
Commit: 80b534e2b0738e96580859a097af44d897bfad38
https://github.com/acl2/acl2/commit/80b534e2b0738e96580859a097af44d897bfad38
M books/kestrel/axe/imported-symbols.lisp
Log Message:
-----------
[axe] Extend list of imported symbols.
Commit: 0031f784c5607b006ddc1d935b33893e05741035
https://github.com/acl2/acl2/commit/0031f784c5607b006ddc1d935b33893e05741035
Author: Eric Smith <ews...@gmail.com>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/risc-v/unroller.lisp
Log Message:
-----------
[axe/risc-v] Fix handling of position-independentp.
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/risc-v/unroller.lisp
Log Message:
-----------
Commit: 3c3902a351fe33e7bebad3ef30501a5d5e02a701
https://github.com/acl2/acl2/commit/3c3902a351fe33e7bebad3ef30501a5d5e02a701
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Changed paths:
Log Message:
-----------
[C$] Improve and simplify preprocessor.
Eliminate the `not-self-contained-p` flag, using the max reach instead. Also, do
not treat max reach > 0 as an exception, but instead continue preprocessing the
file.
Commit: 3924a355b89b6b66167c564ac54c3b6d3b15088a
https://github.com/acl2/acl2/commit/3924a355b89b6b66167c564ac54c3b6d3b15088a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Changed paths:
Log Message:
-----------
[C$] Improve handling of non-self-contained files.
Instead of adding the bytes of the included file to the stobj, use directly
the lexemes coming from the attempt to preprocess the file as self-contained,
which would be the same lexemes anyhow.
Although the C standard is not super-clear about the level at which included
files are expanded in place (byte level, character level, or lexical level), the
syntax of the `#include` directive suggests that the lexical level is the right
one. In some contrived cases, Clang and GCC exhibit some strange (and not
mutually consistent) behaviors that do not quite match that interpretation, but
that still seems the right interpretation.
Commit: f8111fd1b5fa3ea69278f70766be671d3136caa7
https://github.com/acl2/acl2/commit/f8111fd1b5fa3ea69278f70766be671d3136caa7
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/unroller.lisp
Log Message:
-----------
[axe] Improve x86 and risc-v lifters.
Log Message:
-----------
Generate the repeatedly-run function from a template.
Commit: b407e741815b821326c6cacd1097c5632d29ae05
https://github.com/acl2/acl2/commit/b407e741815b821326c6cacd1097c5632d29ae05
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Changed paths:
Log Message:
-----------
[C$] Streamline some preprocessor code.
Have `pproc-file` return a (reversed) list of lexemes and a macro scope, not
packaged into an `scfile`, and do not extend the `preprocessed` alist there.
Let the callers do all of that, if the file is self-contained; if it is not,
the lexemes and macros are used in a different way.
Commit: 712aeecaa6c75c47be2f4992d1e6e56353f0a797
https://github.com/acl2/acl2/commit/712aeecaa6c75c47be2f4992d1e6e56353f0a797
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/macro-tables.lisp
Changed paths:
M books/kestrel/c/syntax/implementation-environments.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/preprocessor-evaluator.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Use logical integer fixer in executable code.
Commit: e597f9881ae630e61ef891c75f4ba8f210ca0738
https://github.com/acl2/acl2/commit/e597f9881ae630e61ef891c75f4ba8f210ca0738
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor.lisp
Changed paths:
M books/kestrel/c/syntax/tests/preprocessor.lisp
Log Message:
-----------
[C$] Simplify a data structure.
We do not need to have a `macros` component in `scfile`, after some code changes
we have made.
Commit: d2512b28f7657b7f9a4e8e655ab3119cad637b29
https://github.com/acl2/acl2/commit/d2512b28f7657b7f9a4e8e655ab3119cad637b29
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/arm/instructions.lisp
Changed paths:
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/make-rewriter-simple.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/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/assumptions.lisp
M books/kestrel/axe/risc-v/support-non-axe.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/risc-v/support-non-axe.lisp
M books/kestrel/axe/risc-v/unroller.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/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/tests/validator.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/validator.lisp
M books/kestrel/c/transformation/add-section-attr-doc.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/wrappers.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/tests/add-section-attr/add-section-attr.lisp
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/wrappers.lisp
M books/kestrel/c/transformation/simpadd0-doc.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/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
A books/kestrel/lists-light/set-difference-equal-fast.lisp
M books/kestrel/lists-light/top.lisp
Commit: 0d5727f68082c562e5e0ba10ef358f0d1314b3d4
https://github.com/acl2/acl2/commit/0d5727f68082c562e5e0ba10ef358f0d1314b3d4
M books/kestrel/axe/step-increments.lisp
Log Message:
-----------
[axe] Improve comment.
Commit: 382b9ebac8877837600264d54ec0af3fe00b13c1
https://github.com/acl2/acl2/commit/382b9ebac8877837600264d54ec0af3fe00b13c1
M books/kestrel/axe/rule-limits.lisp
Log Message:
-----------
[axe] Add a rule.
Commit: 5b959374c2c16281f04bc58a278d0e7fe71096b1
https://github.com/acl2/acl2/commit/5b959374c2c16281f04bc58a278d0e7fe71096b1
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroller.lisp
Log Message:
-----------
[axe/risc-v] Clarify implementation.
Log Message:
-----------
Commit: ade645ebcea7e92a7819ec13d22179ffacf22a71
https://github.com/acl2/acl2/commit/ade645ebcea7e92a7819ec13d22179ffacf22a71
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
A books/kestrel/c/syntax/tests/gincluder.c
Changed paths:
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.lisp
Log Message:
-----------
[C$] Add a preprocessor test with header guards.
Not quite doing what we want just yet, but getting there.
Commit: f1282125f26638942eb5f0da51ba98740ad8e078
https://github.com/acl2/acl2/commit/f1282125f26638942eb5f0da51ba98740ad8e078
M books/kestrel/axe/lifter-common.lisp
Log Message:
-----------
[axe] Fix/improve step counting and printing.
Commit: 8c7f09bd438f3aca2e9e2c516993f4ace993e59a
https://github.com/acl2/acl2/commit/8c7f09bd438f3aca2e9e2c516993f4ace993e59a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/c/syntax/preprocessor-reader.lisp
Changed paths:
M books/kestrel/c/syntax/preprocessor-states.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-reader.lisp
Log Message:
-----------
[C$] Simplify preprocessor stobj.
Now that we are handling included file expansion (when not self-contained) at
the lexical level, we no longer need the array of byte sequences.
Commit: 41dd9ee939c5cfdd2ba7606f4307752088fc7451
https://github.com/acl2/acl2/commit/41dd9ee939c5cfdd2ba7606f4307752088fc7451
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-05 (Thu, 05 Feb 2026)
Changed paths:
M books/kestrel/axe/imported-symbols.lisp
Changed paths:
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-limits.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/executable-parsers/elf-tools.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/6356fc47b78c...41dd9ee939c5
Reply all
Reply to author
Forward
0 new messages