[acl2/acl2] 79546a: [C$] Add a theorem.
0 views
Skip to first unread message
Alessandro Coglio
Aug 14, 2026, 3:37:05 AM (6 days ago) Aug 14
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 79546a675a1c9e78f2437f5815ca7c5d619f62f4
https://github.com/acl2/acl2/commit/79546a675a1c9e78f2437f5815ca7c5d619f62f4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
Log Message:
-----------
[C$] Add a theorem.
Commit: 84b9ed0d7e9b1f5fc19fed4a0947e6df68280f51
https://github.com/acl2/acl2/commit/84b9ed0d7e9b1f5fc19fed4a0947e6df68280f51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
Log Message:
-----------
[C$] Add an inversion theorem.
Commit: 020d8c8fe242163063dcb8b20e9d7c11833b96a3
https://github.com/acl2/acl2/commit/020d8c8fe242163063dcb8b20e9d7c11833b96a3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
Log Message:
-----------
[C$] Improve some ldm code.
Have explicit cases for the unary operators.
Commit: ccefe290919c013915caf2c73e937edf59dc61cc
https://github.com/acl2/acl2/commit/ccefe290919c013915caf2c73e937edf59dc61cc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
Log Message:
-----------
[C$] Add an inversion theorem.
Commit: 7204362d509cc3d08cf7d97d1b8183fb30a3a837
https://github.com/acl2/acl2/commit/7204362d509cc3d08cf7d97d1b8183fb30a3a837
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
Log Message:
-----------
[C$] Refactor some code.
Use the language definition mapping of the unary operators.
Commit: befc110e40863e518b859112fa848dd3e01faa32
https://github.com/acl2/acl2/commit/befc110e40863e518b859112fa848dd3e01faa32
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
Log Message:
-----------
[C$] Add an inversion theorem.
Commit: bd80e3996c27f7a1eecca843937769f1e052da23
https://github.com/acl2/acl2/commit/bd80e3996c27f7a1eecca843937769f1e052da23
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
A books/kestrel/c/transformation/struct-type-split-proofs0.lisp
A books/kestrel/c/transformation/tests/struct-type-split/gso.c
Log Message:
-----------
[STS] Add example to study proof generation.
Commit: 0a319aacb5fe03c8b0c9852dbe4ea0e838b2fdbd
https://github.com/acl2/acl2/commit/0a319aacb5fe03c8b0c9852dbe4ea0e838b2fdbd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
A books/kestrel/c/transformation/struct-type-split-proofs1.lisp
Log Message:
-----------
[STS] A preliminary proof for the simple example.
Commit: a94a6ea5bc94e633f89a3d7f24a78c5deb5f631d
https://github.com/acl2/acl2/commit/a94a6ea5bc94e633f89a3d7f24a78c5deb5f631d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
A books/kestrel/c/transformation/struct-type-split-proofs2.lisp
Log Message:
-----------
[STS] Start work on more systematic proof approach.
Commit: a37c7d434d65bcaf7e80e1d251c851f0977000a5
https://github.com/acl2/acl2/commit/a37c7d434d65bcaf7e80e1d251c851f0977000a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/arithmetic-light/.sys/fl...@useless-runes.lsp
M books/kestrel/arithmetic-light/divide.lisp
M books/kestrel/arithmetic-light/times.lisp
M books/kestrel/arithmetic-light/truncate.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/all-variable-operations.lisp
A books/kestrel/remora/all-variables-under-desugaring.lisp
R books/kestrel/remora/bound-and-free-variable-operations.lisp
A books/kestrel/remora/bound-variable-operations.lisp
A books/kestrel/remora/bound-variables-under-desugaring.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
A books/kestrel/remora/free-variable-operations.lisp
A books/kestrel/remora/free-variables-under-desugaring.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/kestrel/utilities/if.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
M books/kestrel/x86/support-x86.lisp
A books/kestrel/x86/support-x86b.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Commit: 8261e4b8172a8fc20e597d6045494ce0f54efaaf
https://github.com/acl2/acl2/commit/8261e4b8172a8fc20e597d6045494ce0f54efaaf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/5f4f42d0e4b2...8261e4b8172a
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 79546a675a1c9e78f2437f5815ca7c5d619f62f4
https://github.com/acl2/acl2/commit/79546a675a1c9e78f2437f5815ca7c5d619f62f4
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
Log Message:
-----------
[C$] Add a theorem.
Commit: 84b9ed0d7e9b1f5fc19fed4a0947e6df68280f51
https://github.com/acl2/acl2/commit/84b9ed0d7e9b1f5fc19fed4a0947e6df68280f51
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
Log Message:
-----------
[C$] Add an inversion theorem.
Commit: 020d8c8fe242163063dcb8b20e9d7c11833b96a3
https://github.com/acl2/acl2/commit/020d8c8fe242163063dcb8b20e9d7c11833b96a3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
Log Message:
-----------
[C$] Improve some ldm code.
Have explicit cases for the unary operators.
Commit: ccefe290919c013915caf2c73e937edf59dc61cc
https://github.com/acl2/acl2/commit/ccefe290919c013915caf2c73e937edf59dc61cc
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
Log Message:
-----------
[C$] Add an inversion theorem.
Commit: 7204362d509cc3d08cf7d97d1b8183fb30a3a837
https://github.com/acl2/acl2/commit/7204362d509cc3d08cf7d97d1b8183fb30a3a837
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
Log Message:
-----------
[C$] Refactor some code.
Use the language definition mapping of the unary operators.
Commit: befc110e40863e518b859112fa848dd3e01faa32
https://github.com/acl2/acl2/commit/befc110e40863e518b859112fa848dd3e01faa32
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
Log Message:
-----------
[C$] Add an inversion theorem.
Commit: bd80e3996c27f7a1eecca843937769f1e052da23
https://github.com/acl2/acl2/commit/bd80e3996c27f7a1eecca843937769f1e052da23
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
A books/kestrel/c/transformation/struct-type-split-proofs0.lisp
A books/kestrel/c/transformation/tests/struct-type-split/gso.c
Log Message:
-----------
[STS] Add example to study proof generation.
Commit: 0a319aacb5fe03c8b0c9852dbe4ea0e838b2fdbd
https://github.com/acl2/acl2/commit/0a319aacb5fe03c8b0c9852dbe4ea0e838b2fdbd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
A books/kestrel/c/transformation/struct-type-split-proofs1.lisp
Log Message:
-----------
[STS] A preliminary proof for the simple example.
Commit: a94a6ea5bc94e633f89a3d7f24a78c5deb5f631d
https://github.com/acl2/acl2/commit/a94a6ea5bc94e633f89a3d7f24a78c5deb5f631d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
A books/kestrel/c/transformation/struct-type-split-proofs2.lisp
Log Message:
-----------
[STS] Start work on more systematic proof approach.
Commit: a37c7d434d65bcaf7e80e1d251c851f0977000a5
https://github.com/acl2/acl2/commit/a37c7d434d65bcaf7e80e1d251c851f0977000a5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/arithmetic-light/.sys/fl...@useless-runes.lsp
M books/kestrel/arithmetic-light/divide.lisp
M books/kestrel/arithmetic-light/times.lisp
M books/kestrel/arithmetic-light/truncate.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/c/transformation/utilities/.sys/rena...@useless-runes.lsp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce.lisp
M books/kestrel/remora/abstract-syntax-structurals.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
A books/kestrel/remora/all-variable-operations.lisp
A books/kestrel/remora/all-variables-under-desugaring.lisp
R books/kestrel/remora/bound-and-free-variable-operations.lisp
A books/kestrel/remora/bound-variable-operations.lisp
A books/kestrel/remora/bound-variables-under-desugaring.lisp
M books/kestrel/remora/desugaring.lisp
M books/kestrel/remora/evaluation.lisp
A books/kestrel/remora/free-variable-operations.lisp
A books/kestrel/remora/free-variables-under-desugaring.lisp
M books/kestrel/remora/unique-names.lisp
M books/kestrel/remora/variable-renaming-alpha-operations.lisp
M books/kestrel/remora/variable-renaming-operations.lisp
M books/kestrel/remora/variable-substitution-alpha-operations.lisp
M books/kestrel/remora/variable-substitution-operations.lisp
M books/kestrel/utilities/if.lisp
M books/kestrel/x86/assumptions-new.lisp
M books/kestrel/x86/read-over-write-rules64.lisp
M books/kestrel/x86/support-x86.lisp
A books/kestrel/x86/support-x86b.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Commit: 8261e4b8172a8fc20e597d6045494ce0f54efaaf
https://github.com/acl2/acl2/commit/8261e4b8172a8fc20e597d6045494ce0f54efaaf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-13 (Thu, 13 Aug 2026)
Changed paths:
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-direct.lisp
M books/kestrel/c/syntax/abstract-syntax-formal-mapping-inverse.lisp
M books/kestrel/c/syntax/abstract-syntax-operations.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/5f4f42d0e4b2...8261e4b8172a
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Alessandro Coglio
Aug 14, 2026, 3:37:40 AM (6 days ago) Aug 14
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Alessandro Coglio
Aug 18, 2026, 12:21:12 AM (yesterday) Aug 18
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Commit: 3b9f988f912738bdcae80ec3d4722754e36d7d86
https://github.com/acl2/acl2/commit/3b9f988f912738bdcae80ec3d4722754e36d7d86
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-08-14 (Fri, 14 Aug 2026)
Changed paths:
M books/kestrel/filepath/paths.lisp
Log Message:
-----------
Merge commit 'd9b0416fda993c66483ea1ae64390d02352397f3' into HEAD
Commit: c4172f0ef0ea2e5d9746f5bab3143ae498328abf
https://github.com/acl2/acl2/commit/c4172f0ef0ea2e5d9746f5bab3143ae498328abf
Author: Mihir Mehta <mi...@cs.utexas.edu>
Date: 2026-08-16 (Sun, 16 Aug 2026)
Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser-tests.lisp
Log Message:
-----------
[cpp-syntax] Add disambiguation
Commit: 9fe4354715a6beb53a9041cf03ef027d23b48009
https://github.com/acl2/acl2/commit/9fe4354715a6beb53a9041cf03ef027d23b48009
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/support.lisp
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/booleans/booleans.lisp
M books/kestrel/booleans/boolif.lisp
Log Message:
-----------
Merge commit 'aeb37a331f679c81e15be5dfd17d84eed57a2cbc' into HEAD
Commit: a516e85ca580d7d63d28dcd6376b0d3b52de51e0
https://github.com/acl2/acl2/commit/a516e85ca580d7d63d28dcd6376b0d3b52de51e0
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/support.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv/bvminus.lisp
Log Message:
-----------
Merge commit 'aefd4216019a58a443b7ebedba0ae5673050bd5d' into HEAD
Commit: a4b406f083f1ef6ce0e1a0d09ae496037a121757
https://github.com/acl2/acl2/commit/a4b406f083f1ef6ce0e1a0d09ae496037a121757
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
R books/kestrel/remora/dimension-equivalence-infrules.lisp
A books/kestrel/remora/ispace-equivalence-infrules.lisp
M books/kestrel/remora/static-semantics.lisp
Log Message:
-----------
[Remora] Rename a file and topic.
Commit: 336abd732424d63d5f7ef141cd465df318ca02ae
https://github.com/acl2/acl2/commit/336abd732424d63d5f7ef141cd465df318ca02ae
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/unroller.lisp
A books/kestrel/remora/abstract-syntax-haskell.lisp
M books/kestrel/remora/abstract-syntax.lisp
Log Message:
-----------
Merge commit 'c66e32d196673e45864c37220f463419d8f0ae16' into HEAD
Commit: 2d5a9b32d5790e589a63f715ddb2ac09559b5ed7
https://github.com/acl2/acl2/commit/2d5a9b32d5790e589a63f715ddb2ac09559b5ed7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Improve some predicate names.
Commit: 313fbf5280e12f4c9939fdac1cac0c20fae7abac
https://github.com/acl2/acl2/commit/313fbf5280e12f4c9939fdac1cac0c20fae7abac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add some explanatory comments.
Commit: 0a336ba3a0c4e0a4d19400417dd9d180d5bd2e10
https://github.com/acl2/acl2/commit/0a336ba3a0c4e0a4d19400417dd9d180d5bd2e10
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Start rules for shape/ispace equivalence.
Commit: 0dcab15ae91d6272b3528f6e2def15066eeac0bf
https://github.com/acl2/acl2/commit/0dcab15ae91d6272b3528f6e2def15066eeac0bf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add some shape normalization rules.
Commit: 35b9e4c9df71a1ad583a9e38fd679b8f6e3f9ed9
https://github.com/acl2/acl2/commit/35b9e4c9df71a1ad583a9e38fd679b8f6e3f9ed9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Improve some layout and variable names.
Commit: cf06ed65e9aa54d84c06c319b5998ab46fd60fd9
https://github.com/acl2/acl2/commit/cf06ed65e9aa54d84c06c319b5998ab46fd60fd9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add normalization rules for `++`.
Commit: 939355ead356bac5c7f4f27785539b4c7989e9aa
https://github.com/acl2/acl2/commit/939355ead356bac5c7f4f27785539b4c7989e9aa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add rules for splice normalization.
Commit: 8b045d1431e9212b93aff61a0138687576041c83
https://github.com/acl2/acl2/commit/8b045d1431e9212b93aff61a0138687576041c83
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add rules for free monoid properties.
Commit: 27abad2efd5fbf113a4eea1c5b54ef8e530a0fea
https://github.com/acl2/acl2/commit/27abad2efd5fbf113a4eea1c5b54ef8e530a0fea
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/fresh-variable-operations.lisp
M books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/monomorphize.lisp
A books/kestrel/remora/unicode.lisp
M books/kestrel/remora/unique-names-validation.lisp
A books/kestrel/remora/unique-names-well-formedness.lisp
M books/kestrel/utilities/strings/strings-codes.lisp
Log Message:
-----------
Merge commit '219f1a4866012ed0d5ae935431e26ac73329a9ec' into HEAD
Commit: 79fa093d857cd44b38cd1212cca4cca34bc77419
https://github.com/acl2/acl2/commit/79fa093d857cd44b38cd1212cca4cca34bc77419
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Fix some typos and layout.
Commit: 4d97e525ed332d06e15486fc43a598734906f694
https://github.com/acl2/acl2/commit/4d97e525ed332d06e15486fc43a598734906f694
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Simplify two inference rule names.
Commit: db06304e601c62f76ada4c0953ca7d420b848cab
https://github.com/acl2/acl2/commit/db06304e601c62f76ada4c0953ca7d420b848cab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
We still calculate those events, but we do not submit them to ACL2, we do not
describe them in the user documentation, and we do not expect them in the tests.
This is a step towards eventual removal, but we keep the code around a little
longer, just in case.
Commit: 7f9c70260afb61b02202fd1ddc16aeda38b911b5
https://github.com/acl2/acl2/commit/7f9c70260afb61b02202fd1ddc16aeda38b911b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add mising bridge rule.
Commit: 4a7b4a847b1afc72c9e6a4b249f92858bfd0fe9c
https://github.com/acl2/acl2/commit/4a7b4a847b1afc72c9e6a4b249f92858bfd0fe9c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/support.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv/bvminus.lisp
A books/kestrel/remora/abstract-syntax-haskell.lisp
M books/kestrel/remora/abstract-syntax.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
https://github.com/acl2/acl2/commit/9efecef4a446f50c88f471657aa6d077a89b2ed5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Tweak for consistent layout.
Commit: c46375845fb36a54cc0a90f739c37eaec2db7928
https://github.com/acl2/acl2/commit/c46375845fb36a54cc0a90f739c37eaec2db7928
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Simply two inference rules.
Commit: 0179e638c999bee9cf7fec515bd0e7b1e70b87d7
https://github.com/acl2/acl2/commit/0179e638c999bee9cf7fec515bd0e7b1e70b87d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/fresh-variable-operations.lisp
M books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/monomorphize.lisp
A books/kestrel/remora/unicode.lisp
M books/kestrel/remora/unique-names-validation.lisp
A books/kestrel/remora/unique-names-well-formedness.lisp
M books/kestrel/utilities/strings/strings-codes.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/219f1a486601...0179e638c999
https://github.com/acl2/acl2/commit/3b9f988f912738bdcae80ec3d4722754e36d7d86
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-08-14 (Fri, 14 Aug 2026)
Changed paths:
M books/kestrel/filepath/paths.lisp
Log Message:
-----------
Merge commit 'd9b0416fda993c66483ea1ae64390d02352397f3' into HEAD
Commit: c4172f0ef0ea2e5d9746f5bab3143ae498328abf
https://github.com/acl2/acl2/commit/c4172f0ef0ea2e5d9746f5bab3143ae498328abf
Author: Mihir Mehta <mi...@cs.utexas.edu>
Date: 2026-08-16 (Sun, 16 Aug 2026)
Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser-tests.lisp
Log Message:
-----------
[cpp-syntax] Add disambiguation
Commit: 9fe4354715a6beb53a9041cf03ef027d23b48009
https://github.com/acl2/acl2/commit/9fe4354715a6beb53a9041cf03ef027d23b48009
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/package.lsp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/support.lisp
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/booleans/booleans.lisp
M books/kestrel/booleans/boolif.lisp
Log Message:
-----------
Merge commit 'aeb37a331f679c81e15be5dfd17d84eed57a2cbc' into HEAD
Commit: a516e85ca580d7d63d28dcd6376b0d3b52de51e0
https://github.com/acl2/acl2/commit/a516e85ca580d7d63d28dcd6376b0d3b52de51e0
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/support.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv/bvminus.lisp
Log Message:
-----------
Merge commit 'aefd4216019a58a443b7ebedba0ae5673050bd5d' into HEAD
Commit: a4b406f083f1ef6ce0e1a0d09ae496037a121757
https://github.com/acl2/acl2/commit/a4b406f083f1ef6ce0e1a0d09ae496037a121757
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
R books/kestrel/remora/dimension-equivalence-infrules.lisp
A books/kestrel/remora/ispace-equivalence-infrules.lisp
M books/kestrel/remora/static-semantics.lisp
Log Message:
-----------
[Remora] Rename a file and topic.
Commit: 336abd732424d63d5f7ef141cd465df318ca02ae
https://github.com/acl2/acl2/commit/336abd732424d63d5f7ef141cd465df318ca02ae
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/axe/arm/unroller.lisp
A books/kestrel/remora/abstract-syntax-haskell.lisp
M books/kestrel/remora/abstract-syntax.lisp
Log Message:
-----------
Merge commit 'c66e32d196673e45864c37220f463419d8f0ae16' into HEAD
Commit: 2d5a9b32d5790e589a63f715ddb2ac09559b5ed7
https://github.com/acl2/acl2/commit/2d5a9b32d5790e589a63f715ddb2ac09559b5ed7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Improve some predicate names.
Commit: 313fbf5280e12f4c9939fdac1cac0c20fae7abac
https://github.com/acl2/acl2/commit/313fbf5280e12f4c9939fdac1cac0c20fae7abac
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add some explanatory comments.
Commit: 0a336ba3a0c4e0a4d19400417dd9d180d5bd2e10
https://github.com/acl2/acl2/commit/0a336ba3a0c4e0a4d19400417dd9d180d5bd2e10
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Start rules for shape/ispace equivalence.
Commit: 0dcab15ae91d6272b3528f6e2def15066eeac0bf
https://github.com/acl2/acl2/commit/0dcab15ae91d6272b3528f6e2def15066eeac0bf
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add some shape normalization rules.
Commit: 35b9e4c9df71a1ad583a9e38fd679b8f6e3f9ed9
https://github.com/acl2/acl2/commit/35b9e4c9df71a1ad583a9e38fd679b8f6e3f9ed9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Improve some layout and variable names.
Commit: cf06ed65e9aa54d84c06c319b5998ab46fd60fd9
https://github.com/acl2/acl2/commit/cf06ed65e9aa54d84c06c319b5998ab46fd60fd9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add normalization rules for `++`.
Commit: 939355ead356bac5c7f4f27785539b4c7989e9aa
https://github.com/acl2/acl2/commit/939355ead356bac5c7f4f27785539b4c7989e9aa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add rules for splice normalization.
Commit: 8b045d1431e9212b93aff61a0138687576041c83
https://github.com/acl2/acl2/commit/8b045d1431e9212b93aff61a0138687576041c83
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add rules for free monoid properties.
Commit: 27abad2efd5fbf113a4eea1c5b54ef8e530a0fea
https://github.com/acl2/acl2/commit/27abad2efd5fbf113a4eea1c5b54ef8e530a0fea
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/fresh-variable-operations.lisp
M books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/monomorphize.lisp
A books/kestrel/remora/unicode.lisp
M books/kestrel/remora/unique-names-validation.lisp
A books/kestrel/remora/unique-names-well-formedness.lisp
M books/kestrel/utilities/strings/strings-codes.lisp
Log Message:
-----------
Merge commit '219f1a4866012ed0d5ae935431e26ac73329a9ec' into HEAD
Commit: 79fa093d857cd44b38cd1212cca4cca34bc77419
https://github.com/acl2/acl2/commit/79fa093d857cd44b38cd1212cca4cca34bc77419
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Fix some typos and layout.
Commit: 4d97e525ed332d06e15486fc43a598734906f694
https://github.com/acl2/acl2/commit/4d97e525ed332d06e15486fc43a598734906f694
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Simplify two inference rule names.
Commit: db06304e601c62f76ada4c0953ca7d420b848cab
https://github.com/acl2/acl2/commit/db06304e601c62f76ada4c0953ca7d420b848cab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
[definductive] Comment out `-2` events.
Log Message:
-----------
We still calculate those events, but we do not submit them to ACL2, we do not
describe them in the user documentation, and we do not expect them in the tests.
This is a step towards eventual removal, but we keep the code around a little
longer, just in case.
Commit: 7f9c70260afb61b02202fd1ddc16aeda38b911b5
https://github.com/acl2/acl2/commit/7f9c70260afb61b02202fd1ddc16aeda38b911b5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Add mising bridge rule.
Commit: 4a7b4a847b1afc72c9e6a4b249f92858bfd0fe9c
https://github.com/acl2/acl2/commit/4a7b4a847b1afc72c9e6a4b249f92858bfd0fe9c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/x86/tests/ndsu/assembly/support.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv/bvminus.lisp
A books/kestrel/remora/abstract-syntax-haskell.lisp
M books/kestrel/remora/abstract-syntax.lisp
M books/std/util/definductive-doc.lisp
M books/std/util/definductive-tests.lisp
M books/std/util/definductive.lisp
Log Message:
-----------
Merge.
Commit: 9efecef4a446f50c88f471657aa6d077a89b2ed5
Log Message:
-----------
Merge.
https://github.com/acl2/acl2/commit/9efecef4a446f50c88f471657aa6d077a89b2ed5
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Tweak for consistent layout.
Commit: c46375845fb36a54cc0a90f739c37eaec2db7928
https://github.com/acl2/acl2/commit/c46375845fb36a54cc0a90f739c37eaec2db7928
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/ispace-equivalence-infrules.lisp
Log Message:
-----------
[Remora] Simply two inference rules.
Commit: 0179e638c999bee9cf7fec515bd0e7b1e70b87d7
https://github.com/acl2/acl2/commit/0179e638c999bee9cf7fec515bd0e7b1e70b87d7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-08-17 (Mon, 17 Aug 2026)
Changed paths:
M books/kestrel/remora/fresh-variable-operations.lisp
M books/kestrel/remora/identifier-syntax.lisp
M books/kestrel/remora/monomorphize.lisp
A books/kestrel/remora/unicode.lisp
M books/kestrel/remora/unique-names-validation.lisp
A books/kestrel/remora/unique-names-well-formedness.lisp
M books/kestrel/utilities/strings/strings-codes.lisp
Log Message:
-----------
Merge.
Compare: https://github.com/acl2/acl2/compare/219f1a486601...0179e638c999
Reply all
Reply to author
Forward
0 new messages