[acl2/acl2] 21d540: A formalization of Galois theory (projects/fields/)

[russinoff]

Branch: refs/heads/testing
Home: https://github.com/acl2/acl2
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


Compare: https://github.com/acl2/acl2/compare/3efdc4eaccf4...c61901a64c8a

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

[Eric W. Smith]

Branch: refs/heads/master

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: 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: 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: 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: 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.


Compare: https://github.com/acl2/acl2/compare/6211b25fd42a...349d81cc3b3d

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

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: 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.


Compare: https://github.com/acl2/acl2/compare/81b2d237b87a...60461a4e044f