[acl2/acl2] 69b529: [Remora] Remove essentially-empty file not needed.

0 views
Skip to first unread message

Alessandro Coglio

unread,
May 22, 2026, 11:43:13 PM (10 days ago) May 22
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 69b52901458bdeddee2f80c47debdaeb6d53192d
https://github.com/acl2/acl2/commit/69b52901458bdeddee2f80c47debdaeb6d53192d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-21 (Thu, 21 May 2026)

Changed paths:
R books/kestrel/remora/interpreter.lisp

Log Message:
-----------
[Remora] Remove essentially-empty file not needed.


Commit: 49d5b72737c21a47ead53b7732dcd72b26ed654e
https://github.com/acl2/acl2/commit/49d5b72737c21a47ead53b7732dcd72b26ed654e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/acl2-arrays/compress11.lisp
M books/kestrel/arithmetic-light/floor2.lisp
M books/kestrel/arm/rules.lisp
M books/kestrel/axe/add-and-normalize-expr.lisp
M books/kestrel/axe/axe-rules-mixed.lisp
M books/kestrel/axe/axe-trees.lisp
M books/kestrel/axe/axe-types.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/bv-array-rules.lisp
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/choose-rules.lisp
M books/kestrel/axe/conjunctions-and-disjunctions.lisp
M books/kestrel/axe/dag-array-builders.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dagify0.lisp
M books/kestrel/axe/dags.lisp
M books/kestrel/axe/elim.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/jvm/lifter-utilities3.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/lifter2.lisp
M books/kestrel/axe/jvm/rule-lists-jvm.lisp
M books/kestrel/axe/jvm/tester.lisp
M books/kestrel/axe/jvm/unroller2.lisp
M books/kestrel/axe/make-axe-rules.lisp
M books/kestrel/axe/make-instantiation-code-simple-free-vars.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/merge-dag-into-dag-quick.lisp
M books/kestrel/axe/merge-term-into-dag-array-simple.lisp
M books/kestrel/axe/node-replacement-alist-for-context.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/normalize-xors.lisp
M books/kestrel/axe/prover-common.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/prover2.lisp
M books/kestrel/axe/prune-dag-precisely.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/r1cs/lift-r1cs-rules.lisp
M books/kestrel/axe/r1cs/lift-r1cs.lisp
M books/kestrel/axe/refined-assumption-alists2.lisp
M books/kestrel/axe/replace-node.lisp
M books/kestrel/axe/replace-using-assumptions.lisp
M books/kestrel/axe/rewriter-alt-tests.lisp
M books/kestrel/axe/risc-v/read-and-write.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules1.lisp
M books/kestrel/axe/rules2.lisp
M books/kestrel/axe/rules3.lisp
M books/kestrel/axe/specialize.lisp
M books/kestrel/axe/splitting.lisp
M books/kestrel/axe/substitute-vars.lisp
M books/kestrel/axe/substitute-vars2.lisp
M books/kestrel/axe/supporting-nodes.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/tailtohead.lisp
M books/kestrel/axe/unify-term-and-dag-with-name.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/tester-rules-bv.lisp
M books/kestrel/axe/x86/x86-rules.lisp
M books/kestrel/bv-arrays/bv-array-clear.lisp
M books/kestrel/bv-arrays/bv-arrays.lisp
M books/kestrel/bv-lists/map-packbv.lisp
M books/kestrel/bv/adder.lisp
M books/kestrel/bv/bitnot.lisp
M books/kestrel/bv/bv-syntax.lisp
M books/kestrel/bv/bvcat-rules.lisp
M books/kestrel/bv/bvchop.lisp
M books/kestrel/bv/bvcount.lisp
M books/kestrel/bv/bvlt.lisp
M books/kestrel/bv/bvminus-rules.lisp
M books/kestrel/bv/bvminus.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/bvxor.lisp
M books/kestrel/bv/leftrotate.lisp
M books/kestrel/bv/logext.lisp
M books/kestrel/bv/logior-b.lisp
M books/kestrel/bv/logxor-b.lisp
M books/kestrel/bv/rotate.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules10.lisp
M books/kestrel/bv/rules2.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/rules4.lisp
M books/kestrel/bv/sbvdiv-rules.lisp
M books/kestrel/bv/sbvdivdown-rules.lisp
M books/kestrel/bv/slice2.lisp
M books/kestrel/clause-processors/simplify-after-using-conjunction.lisp
M books/kestrel/ethereum/evm/evm.lisp
M books/kestrel/ethereum/semaphore/blake2s-mixing-proof.lisp
M books/kestrel/helpers/linter.lisp
M books/kestrel/jvm/ads.lisp
M books/kestrel/jvm/ads2.lisp
M books/kestrel/jvm/adstop.lisp
M books/kestrel/jvm/arrays-2d.lisp
M books/kestrel/jvm/arrays.lisp
M books/kestrel/jvm/class-file-parser.lisp
M books/kestrel/jvm/class-tables.lisp
M books/kestrel/jvm/heap-clearing.lisp
M books/kestrel/jvm/heap0.lisp
M books/kestrel/jvm/instructions.lisp
M books/kestrel/jvm/jvm-facts0.lisp
M books/kestrel/jvm/jvm-rules.lisp
M books/kestrel/jvm/jvm.lisp
M books/kestrel/jvm/utilities2.lisp
M books/kestrel/lists-light/rules2.lisp
M books/kestrel/terms-light/simplify-ors-proofs.lisp
M books/kestrel/typed-lists-light/decreasingp.lisp
M books/kestrel/x86/conditions.lisp
M books/kestrel/x86/read-and-write.lisp
M books/kestrel/x86/read-over-write-rules32.lisp
M books/kestrel/x86/support.lisp
M books/kestrel/x86/support32.lisp
M books/kestrel/zcash/gadgets/a-3-3-6-proof.lisp

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


Commit: 5fb1de68d07c558d9ef3eb37249c6cc0effe515e
https://github.com/acl2/acl2/commit/5fb1de68d07c558d9ef3eb37249c6cc0effe515e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/fty/top.lisp

Log Message:
-----------
[FTY] Add result type for integer lists.


Commit: b51c75592fe0de8a0d969b85723482e728cc2d5b
https://github.com/acl2/acl2/commit/b51c75592fe0de8a0d969b85723482e728cc2d5b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Import some symbols.


Commit: 63c30832bdff639801af12322cbe8e9478d99137
https://github.com/acl2/acl2/commit/63c30832bdff639801af12322cbe8e9478d99137
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
A books/kestrel/remora/integer-list-operations.lisp
M books/kestrel/remora/library-extensions.lisp

Log Message:
-----------
[Remora] Add operations on lists of integers.


Commit: 6475013e49b678d29a2d82007438a7d83489ba60
https://github.com/acl2/acl2/commit/6475013e49b678d29a2d82007438a7d83489ba60
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Relax evaluation of dimensions.

Let the results be possibly negative integers, as done in the Haskell
implementation, following a discussion with the team. We will restrict them to
be non-negative at the top level, as in the Haskell implementation.


Commit: 6fb59891fef610429cd40b83e45b0cbc1d07f321
https://github.com/acl2/acl2/commit/6fb59891fef610429cd40b83e45b0cbc1d07f321
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
A books/kestrel/fty/integer-list-result.lisp

Log Message:
-----------
[FTY] Forgot to add the file.


Commit: 2c709a77cf388df7a83566bafea6c4a6c0d97732
https://github.com/acl2/acl2/commit/2c709a77cf388df7a83566bafea6c4a6c0d97732
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-structural-operations.lisp

Log Message:
-----------
[Remora] Add missing doc.


Commit: 5a4c7d385fa40b163385694af20e62383c7cd71f
https://github.com/acl2/acl2/commit/5a4c7d385fa40b163385694af20e62383c7cd71f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/library-extensions.lisp

Log Message:
-----------
[Remora] Fix typo in book inclusion.


Commit: f426eec8bcf80f2944cd0d3c8f3b858f1cfad6a0
https://github.com/acl2/acl2/commit/f426eec8bcf80f2944cd0d3c8f3b858f1cfad6a0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/nat-list-operations.lisp

Log Message:
-----------
[Remora] Add an operation on lists of naturals.


Commit: 7b2270e3a6c47ffccc342b54acb09f55b8a2c5fa
https://github.com/acl2/acl2/commit/7b2270e3a6c47ffccc342b54acb09f55b8a2c5fa
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Add evaluation of shapes.


Commit: 476570f6017dce5902c5e755388f6e43a9f8e811
https://github.com/acl2/acl2/commit/476570f6017dce5902c5e755388f6e43a9f8e811
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/dynamic-values.lisp

Log Message:
-----------
[Remora] Add a result fixtype.


Commit: 6552bdb3fe985ed82a9be8a0f6fa7b13203491a0
https://github.com/acl2/acl2/commit/6552bdb3fe985ed82a9be8a0f6fa7b13203491a0
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Add ealuation of ispaces.


Commit: d485f5ec263c8a39db7d18956a25d9d6feff612a
https://github.com/acl2/acl2/commit/d485f5ec263c8a39db7d18956a25d9d6feff612a
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/proofs/utilities/sys-view/paging/gather-paging-structures.lisp
M books/projects/x86isa/utils/paging-structures.lisp
M books/projects/x86isa/utils/records-0.lisp
M books/projects/x86isa/utils/utilities.lisp

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


Commit: a605470a09e9a5856ce261337b9adfa0b99cbd33
https://github.com/acl2/acl2/commit/a605470a09e9a5856ce261337b9adfa0b99cbd33
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp

Log Message:
-----------
[Remora] Add evaluation of lists of ispaces.


Commit: 8c3cf8ced7aadc6a039343be5fbd31f5d448ab28
https://github.com/acl2/acl2/commit/8c3cf8ced7aadc6a039343be5fbd31f5d448ab28
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/fresh-variables.lisp
M books/kestrel/remora/type-equivalence.lisp

Log Message:
-----------
[Remora] Improve fresh variable generation.

Now a prefix can be specified.


Commit: 831c5357530f2be2e290bf79afc986f28de9bdd3
https://github.com/acl2/acl2/commit/831c5357530f2be2e290bf79afc986f28de9bdd3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/remora/type-equivalence.lisp

Log Message:
-----------
[Remora] Improve fresh variables in type equivalence.

Use a prefix conveying that they are fresh variables. This also makes them
legal Remora identifiers.


Compare: https://github.com/acl2/acl2/compare/3efdc4eaccf4...831c5357530f

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

Alessandro Coglio

unread,
May 23, 2026, 12:59:49 AM (10 days ago) May 23
to acl2-...@googlegroups.com
Branch: refs/heads/master

acl2buildserver

unread,
May 23, 2026, 1:00:39 AM (10 days ago) May 23
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Commit: 9d13f67424fd5df0fd2e3c5f120ba6895c23d320
https://github.com/acl2/acl2/commit/9d13f67424fd5df0fd2e3c5f120ba6895c23d320
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
A books/kestrel/fty/integer-list-result.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/fresh-variables.lisp
A books/kestrel/remora/integer-list-operations.lisp
R books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/library-extensions.lisp
M books/kestrel/remora/nat-list-operations.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/type-equivalence.lisp

Log Message:
-----------
Merge commit '831c5357530f2be2e290bf79afc986f28de9bdd3' into HEAD


Compare: https://github.com/acl2/acl2/compare/19301be9bac6...9d13f67424fd

Alessandro Coglio

unread,
May 26, 2026, 10:41:05 PM (6 days ago) May 26
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 69b52901458bdeddee2f80c47debdaeb6d53192d
https://github.com/acl2/acl2/commit/69b52901458bdeddee2f80c47debdaeb6d53192d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-21 (Thu, 21 May 2026)

Changed paths:
R books/kestrel/remora/interpreter.lisp

Log Message:
-----------
[Remora] Remove essentially-empty file not needed.


Commit: 353caf549b664a07480efee051f45545610c7a0d
https://github.com/acl2/acl2/commit/353caf549b664a07480efee051f45545610c7a0d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/bv/bitops.lisp

Log Message:
-----------
[bv] Add rule to replace b-not.


Commit: 814da4f2b60a8169161118377216f5cde281cc58
https://github.com/acl2/acl2/commit/814da4f2b60a8169161118377216f5cde281cc58
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/bv/bvshl.lisp
M books/kestrel/bv/single-bit.lisp

Log Message:
-----------
[bv] Add misc rules.


Commit: 7cb941c97efd69c4f4685137440a241801358e1a
https://github.com/acl2/acl2/commit/7cb941c97efd69c4f4685137440a241801358e1a
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/x86/package.lsp

Log Message:
-----------
[x86] Extend package.


Commit: 74d87547d622ab48db79fd01bdbd28d8416597c9
https://github.com/acl2/acl2/commit/74d87547d622ab48db79fd01bdbd28d8416597c9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/x86/alt-defs.lisp

Log Message:
-----------
[x86] Add rule to replace blsi.


Commit: 1ecf4c3957895f8af3c8620a217601e2baecf38d
https://github.com/acl2/acl2/commit/1ecf4c3957895f8af3c8620a217601e2baecf38d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/axe/arm/unroller.lisp
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] Clarify.


Commit: 3f890e3a03092c0d80557fe8c255b166d1820ab9
https://github.com/acl2/acl2/commit/3f890e3a03092c0d80557fe8c255b166d1820ab9
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

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

Log Message:
-----------
[axe/x86] Improve rule-lists.


Commit: cd23b3dfca518aaf613a2a9ccfdaa79641a30114
https://github.com/acl2/acl2/commit/cd23b3dfca518aaf613a2a9ccfdaa79641a30114
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/make-axe-rules.lisp

Log Message:
-----------
[axe] Drop package prefixes.


Commit: 813799d5e031eff48228e00b10dfb9aa2b233e53
https://github.com/acl2/acl2/commit/813799d5e031eff48228e00b10dfb9aa2b233e53
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp

Log Message:
-----------
[bv-lists] Drop package prefixes.


Commit: c70ce59293dda83bbe2d094a85b31ecafd5a8f04
https://github.com/acl2/acl2/commit/c70ce59293dda83bbe2d094a85b31ecafd5a8f04
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/bv/bvmult-rules.lisp
M books/kestrel/bv/bvplus.lisp
M books/kestrel/bv/rules12.lisp

Log Message:
-----------
[bv] Clean up a bit.


Commit: b3d63d23349cf77fded920546e8e1ca5adfd4bbc
https://github.com/acl2/acl2/commit/b3d63d23349cf77fded920546e8e1ca5adfd4bbc
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/axe-trees.lisp
M books/kestrel/axe/darg-trees.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/step-increments.lisp

Log Message:
-----------
[axe] Clean up a bit.
Commit: 21d5404de4d0ce9aae690e38bc9b21ae57daea40
https://github.com/acl2/acl2/commit/21d5404de4d0ce9aae690e38bc9b21ae57daea40
Author: David Russinoff <da...@russinoff.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
A books/projects/fields/README
A books/projects/fields/embeddings.lisp
M books/projects/fields/extensions.lisp
A books/projects/fields/galois.lisp
A books/projects/fields/support/embeddings.lisp
M books/projects/fields/support/extensions.lisp
A books/projects/fields/support/galois.lisp
M books/projects/linear/README

Log Message:
-----------
A formalization of Galois theory (projects/fields/)


Commit: c61901a64c8a855cf85b13878f327efdc192d509
https://github.com/acl2/acl2/commit/c61901a64c8a855cf85b13878f327efdc192d509
Author: David Russinoff <da...@russinoff.com>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/proofs/utilities/sys-view/paging/gather-paging-structures.lisp
M books/projects/x86isa/utils/paging-structures.lisp
M books/projects/x86isa/utils/records-0.lisp
M books/projects/x86isa/utils/utilities.lisp

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


Commit: 19301be9bac6d62ac03bfeb669b542170f688302
https://github.com/acl2/acl2/commit/19301be9bac6d62ac03bfeb669b542170f688302
Author: Mihir Mehta <mi...@cs.utexas.edu>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/cpp-abstract-syntax.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-member-full.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-parser-tests.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-top-level-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/top.lisp

Log Message:
-----------
Update books


Commit: 15ddbfaa3c477c93beb211e36d22d7ea9dd35a69
https://github.com/acl2/acl2/commit/15ddbfaa3c477c93beb211e36d22d7ea9dd35a69
Author: Eric McCarthy <mcca...@kestrel.edu>
Date: 2026-05-22 (Fri, 22 May 2026)

Changed paths:
A books/kestrel/remora/check-keywords.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp

Log Message:
-----------
[remora] Add keyword rule to grammar for clarity and check against constant to keep in sync. Change keywords in rules to be case sensitive and update parser consistently.


Commit: 9d13f67424fd5df0fd2e3c5f120ba6895c23d320
https://github.com/acl2/acl2/commit/9d13f67424fd5df0fd2e3c5f120ba6895c23d320
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
A books/kestrel/fty/integer-list-result.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/fresh-variables.lisp
A books/kestrel/remora/integer-list-operations.lisp
R books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/library-extensions.lisp
M books/kestrel/remora/nat-list-operations.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/type-equivalence.lisp

Log Message:
-----------
Merge commit '831c5357530f2be2e290bf79afc986f28de9bdd3' into HEAD


Commit: 61f8929f259d4e06aacc1718fa7b7efb9d241822
https://github.com/acl2/acl2/commit/61f8929f259d4e06aacc1718fa7b7efb9d241822
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
A books/kestrel/remora/check-keywords.lisp
M books/kestrel/remora/grammar.abnf
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp

Log Message:
-----------
Merge commit '15ddbfaa3c477c93beb211e36d22d7ea9dd35a69' into HEAD


Commit: 16efe20ffdc2a5da43e93d92b64c913c711488f1
https://github.com/acl2/acl2/commit/16efe20ffdc2a5da43e93d92b64c913c711488f1
Author: David Russinoff <da...@russinoff.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
M books/projects/fields/README
A books/projects/linear/support/vectors.lisp
A books/projects/linear/vectors.lisp

Log Message:
-----------
added projects/linear/vectors.lisp


Commit: 350e43926d5a2a0976533e52b0923df05838d335
https://github.com/acl2/acl2/commit/350e43926d5a2a0976533e52b0923df05838d335
Author: David Russinoff <da...@russinoff.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
A books/kestrel/fty/integer-list-result.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
A books/kestrel/remora/check-keywords.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/fresh-variables.lisp
M books/kestrel/remora/grammar.abnf
A books/kestrel/remora/integer-list-operations.lisp
R books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/library-extensions.lisp
M books/kestrel/remora/nat-list-operations.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/type-equivalence.lisp

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


Commit: cc7b1c131261320dfe06dff7b3d016c2b07541a7
https://github.com/acl2/acl2/commit/cc7b1c131261320dfe06dff7b3d016c2b07541a7
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
A books/kestrel/fty/integer-list-result.lisp
M books/kestrel/fty/top.lisp
M books/kestrel/remora/abstract-syntax-structural-operations.lisp
A books/kestrel/remora/check-keywords.lisp
M books/kestrel/remora/dynamic-values.lisp
M books/kestrel/remora/evaluation.lisp
M books/kestrel/remora/fresh-variables.lisp
M books/kestrel/remora/grammar.abnf
A books/kestrel/remora/integer-list-operations.lisp
R books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/library-extensions.lisp
M books/kestrel/remora/nat-list-operations.lisp
M books/kestrel/remora/package.lsp
M books/kestrel/remora/parser.lisp
M books/kestrel/remora/post-parsing.lisp
M books/kestrel/remora/type-equivalence.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/move-sse.lisp
M books/projects/x86isa/machine/instructions/move-vex.lisp
M books/projects/x86isa/machine/register-readers-and-writers.lisp
M books/projects/x86isa/proofs/utilities/sys-view/paging/gather-paging-structures.lisp
M books/projects/x86isa/utils/paging-structures.lisp
M books/projects/x86isa/utils/records-0.lisp
M books/projects/x86isa/utils/utilities.lisp

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


Commit: 77b5a16e6d7fa56c14c17d157dc8605e5078f7c8
https://github.com/acl2/acl2/commit/77b5a16e6d7fa56c14c17d157dc8605e5078f7c8
Author: David Russinoff <da...@russinoff.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/cpp-abstract-syntax.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-member-full.lisp
A books/projects/filesystems/utilities/cpp-syntax/cpp-parser-tests.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-top-level-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/top.lisp

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


Commit: e6ed2b305c5d1779b3fe51f58c4f401e2b80d9bf
https://github.com/acl2/acl2/commit/e6ed2b305c5d1779b3fe51f58c4f401e2b80d9bf
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
M books/kestrel/bv/bvshl.lisp

Log Message:
-----------
[bv] Improve rule.


Commit: 853faf044022fb039c06d2c7c50e0ae046bd5720
https://github.com/acl2/acl2/commit/853faf044022fb039c06d2c7c50e0ae046bd5720
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/axe-trees.lisp
M books/kestrel/axe/bv-array-rules-axe.lisp
M books/kestrel/axe/dag-printing.lisp
M books/kestrel/axe/darg-trees.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/lifter-common.lisp
M books/kestrel/axe/make-axe-rules.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/step-increments.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/bv-lists/bv-list-read-chunk-little.lisp
M books/kestrel/bv/bitops.lisp
M books/kestrel/bv/bvmult-rules.lisp
M books/kestrel/bv/bvplus.lisp
M books/kestrel/bv/bvshl.lisp
M books/kestrel/bv/rules12.lisp
M books/kestrel/bv/single-bit.lisp
M books/kestrel/x86/alt-defs.lisp
M books/kestrel/x86/package.lsp

Log Message:
-----------
Merge commit 'e6ed2b305c5d1779b3fe51f58c4f401e2b80d9bf' into HEAD


Commit: 6211b25fd42a193da151bcc3ce076b6a93a97315
https://github.com/acl2/acl2/commit/6211b25fd42a193da151bcc3ce076b6a93a97315
Author: Matt Kaufmann <matthew.j...@gmail.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
M books/projects/set-theory/base.lisp
M books/projects/set-theory/doc.lisp
M books/projects/set-theory/logic.txt
M books/xdoc/parse-xml.lisp
M doc/home-page.html

Log Message:
-----------
Tweaked :DOC topics zfc and zfc-model and file books/projects/set-theory/logic.txt. Fixed text rendering of &isin; (to \in instead of to \isin).


Commit: f35e15a37877b2c2831e8133be6256f26bb3e96e
https://github.com/acl2/acl2/commit/f35e15a37877b2c2831e8133be6256f26bb3e96e
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-23 (Sat, 23 May 2026)

Changed paths:
M books/projects/set-theory/base.lisp
M books/projects/set-theory/doc.lisp
M books/projects/set-theory/logic.txt
M books/xdoc/parse-xml.lisp
M doc/home-page.html

Log Message:
-----------
Merge commit '6211b25fd42a193da151bcc3ce076b6a93a97315' into HEAD


Commit: 349d81cc3b3d88ca0ff9fb0576cb0976c961bc79
https://github.com/acl2/acl2/commit/349d81cc3b3d88ca0ff9fb0576cb0976c961bc79
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-24 (Sun, 24 May 2026)

Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser-tests.lisp

Log Message:
-----------
Comment out failing tests.

This is an attempt to get the testing branch working again.


Commit: ffb49dc961a305b1212fdc725fd3e592be4eade7
https://github.com/acl2/acl2/commit/ffb49dc961a305b1212fdc725fd3e592be4eade7
Author: Mihir Mehta <mi...@cs.utexas.edu>
Date: 2026-05-24 (Sun, 24 May 2026)

Changed paths:
M books/projects/filesystems/utilities/cpp-syntax/cpp-abstract-syntax.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-expr-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-keywords.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-member-full.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser-tests.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-parser.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-token-utilities.lisp
M books/projects/filesystems/utilities/cpp-syntax/cpp-top-level-parser.lisp

Log Message:
-----------
Update books

A note in response to the email by @ericwhitmansmith : thanks for
letting me know about the broken build! Sorry it took me a few hours -
but I do have a fix though that disables failing assertions in the
book that broke the build.. Thanks also for your commit that commented
out the failing tests - I'm rebasing on top of it and believe, based
on certifying books on my machine, that the testing branch should get
back to normal now.


Commit: 26910551e408e158afebee9fa616d812d7bbd495
https://github.com/acl2/acl2/commit/26910551e408e158afebee9fa616d812d7bbd495
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp

Log Message:
-----------
[axe/x86] Add theorem to test file.

Based on one proved by the NDSU folks.


Commit: 059d94baaeef13fbf1accca67b58bf2965c21e6b
https://github.com/acl2/acl2/commit/059d94baaeef13fbf1accca67b58bf2965c21e6b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp

Log Message:
-----------
[axe/x86] Add theorem to test file.

Based on one proved by the NDSU folks.


Commit: 837f965c96ee505b83339a5f5e887b3ede47b5a6
https://github.com/acl2/acl2/commit/837f965c96ee505b83339a5f5e887b3ede47b5a6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/bv/bvcount.lisp

Log Message:
-----------
[bv] Add rule connecting bvcount to logcount.


Commit: 2273caf64208f18bd1b587fff95bbf547d9fcdb6
https://github.com/acl2/acl2/commit/2273caf64208f18bd1b587fff95bbf547d9fcdb6
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/bv/bvchop.lisp

Log Message:
-----------
[bv] Improve a rule.


Commit: bcb3dc6579f4d7a211b1198d61b39a9d9c1db745
https://github.com/acl2/acl2/commit/bcb3dc6579f4d7a211b1198d61b39a9d9c1db745
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/bv/getbit.lisp

Log Message:
-----------
[bv] Add a rule about evenp.


Commit: d68cdca76840027334835954181ec7a765ffba2b
https://github.com/acl2/acl2/commit/d68cdca76840027334835954181ec7a765ffba2b
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/bv/bvcount.lisp

Log Message:
-----------
[bv] Remove subsumed rule.


Commit: 81b2d237b87a26903588da68ce3928e0959755fd
https://github.com/acl2/acl2/commit/81b2d237b87a26903588da68ce3928e0959755fd
Author: Eric Smith <ews...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp

Log Message:
-----------
[axe/x86] Improve test.

Add proofs about the other flags.


Commit: a857b4866be2e38b5c8ea4af9b571b0288985ba1
https://github.com/acl2/acl2/commit/a857b4866be2e38b5c8ea4af9b571b0288985ba1
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-25 (Mon, 25 May 2026)

Changed paths:
M books/kestrel/axe/x86/tests/kestrel/assembly/add.lisp
M books/kestrel/bv/bvchop.lisp
M books/kestrel/bv/bvcount.lisp
M books/kestrel/bv/getbit.lisp

Log Message:
-----------
Merge commit '81b2d237b87a26903588da68ce3928e0959755fd' into HEAD


Commit: 60461a4e044f72cb82d291af0b8df8f6dbf486f3
https://github.com/acl2/acl2/commit/60461a4e044f72cb82d291af0b8df8f6dbf486f3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)

Changed paths:
M books/kestrel/c/atc/statement-generation.lisp

Log Message:
-----------
[ATC] Add some rules to a generated theorem.

Without these, an example was failing.


Commit: 73dca0056b442bbfbd1b67e0ceaa2774447ccec9
https://github.com/acl2/acl2/commit/73dca0056b442bbfbd1b67e0ceaa2774447ccec9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)

Changed paths:
M books/kestrel/c/syntax/grammar/grammar-rest.abnf

Log Message:
-----------
[C$] Add some comments about GCC/MSVC extensions.

As suggested by Grant Jurgensen.


Commit: 461c3aa999028359736925437a0d318c981331b8
https://github.com/acl2/acl2/commit/461c3aa999028359736925437a0d318c981331b8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)

Changed paths:
M books/kestrel/c/syntax/input-files.lisp
M books/kestrel/c/syntax/preprocessor-options.lisp
M books/kestrel/c/syntax/preprocessor.lisp
M books/kestrel/c/syntax/tests/preprocessor-lexer.lisp
M books/kestrel/c/syntax/tests/preprocessor-testing-macros.lisp

Log Message:
-----------
[C$] Improve preprocessor.

When the stand-alone re-preprocessing of an included file fails, in particular
for encountering a `#error` directive that is instead skipped when the included
file is preprocessed in the context of the including file, we should regard that
`#include` directive as not being preservable, instead of ignoring errors.


Commit: 0b063f85de99aa8b5f57c06b0d9bc1085e6c4a62
https://github.com/acl2/acl2/commit/0b063f85de99aa8b5f57c06b0d9bc1085e6c4a62
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)

Changed paths:
M books/kestrel/c/atc/statement-generation.lisp

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


Commit: 25896c02fb1fc4e3186ef8c3edaeefd39b8f6597
https://github.com/acl2/acl2/commit/25896c02fb1fc4e3186ef8c3edaeefd39b8f6597
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)

Changed paths:
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/tokens.abnf

Log Message:
-----------
[C$] Factor out grammar rules for tokens.


Commit: 3678e5d23c118787155d0101bea57ddbc1e968ff
https://github.com/acl2/acl2/commit/3678e5d23c118787155d0101bea57ddbc1e968ff
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)

Changed paths:
M books/kestrel/c/syntax/grammar.lisp
M books/kestrel/c/syntax/grammar/grammar-rest.abnf
A books/kestrel/c/syntax/grammar/lexemes.abnf

Log Message:
-----------
[C$] Factor out grammar rule for lexemes.


Commit: 643fbfad801672e5375eaae071956a61f7c6943c
https://github.com/acl2/acl2/commit/643fbfad801672e5375eaae071956a61f7c6943c
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/stringization.lisp

Log Message:
-----------
[C$] Improve fixtype of preprocessor lexemes.

Use a more precise type for the `:other` summand.


Commit: df36aedd9234c53070ee144b0120fb667109fb78
https://github.com/acl2/acl2/commit/df36aedd9234c53070ee144b0120fb667109fb78
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)

Changed paths:
M books/kestrel/c/syntax/preprocessor-lexemes.lisp
M books/kestrel/c/syntax/preprocessor-printer.lisp
M books/kestrel/c/syntax/stringization.lisp

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


Commit: 9bfa39df33992ea198bdcb6471b8f485d3e444c1
https://github.com/acl2/acl2/commit/9bfa39df33992ea198bdcb6471b8f485d3e444c1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-26 (Tue, 26 May 2026)

Changed paths:
M books/kestrel/c/syntax/disambiguator.lisp

Log Message:
-----------
[C$] Add and populate a disambiguator state component.

This tracks the identifiers that follow `goto`s that are re-classified from
label identifiers to expression identifiers. The set stays empty unless GCC or
Clang extensions are enabled (and some re-classification happens).


Compare: https://github.com/acl2/acl2/compare/3efdc4eaccf4...9bfa39df3399
Reply all
Reply to author
Forward
0 new messages