[acl2/acl2] 214ba4: Made modifications so that "make regression" passe...

0 views
Skip to first unread message

MattKaufmann

unread,
Feb 28, 2026, 10:33:13 AM (5 days ago) Feb 28
to acl2-...@googlegroups.com
Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 214ba4dd6983ec5db14827b7a337063e041bfa26
https://github.com/acl2/acl2/commit/214ba4dd6983ec5db14827b7a337063e041bfa26
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-02-27 (Fri, 27 Feb 2026)

Changed paths:
M books/kestrel/arm/state.lisp
M books/kestrel/utilities/defstobj-plus-tests.lisp
M books/workshops/2025/kwan/rv-state.lisp

Log Message:
-----------
Made modifications so that "make regression" passes for ACL2 built on 32-bit CMUCL.


Commit: 4f5a4b2c30ed4b3ae7071bde7e3bb7a87fb22a59
https://github.com/acl2/acl2/commit/4f5a4b2c30ed4b3ae7071bde7e3bb7a87fb22a59
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
A books/projects/x86isa/machine/instructions/pmadd.lisp
A books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/top.lisp

Log Message:
-----------
Merge remote-tracking branch 'remotes/origin/master'


Compare: https://github.com/acl2/acl2/compare/c0d3f5729fae...4f5a4b2c30ed

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

MattKaufmann

unread,
Feb 28, 2026, 10:33:42 AM (5 days ago) Feb 28
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
Feb 28, 2026, 5:29:06 PM (4 days ago) Feb 28
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: ba50224ead363fdf6edc019ce6daf2fb4b1ac781
https://github.com/acl2/acl2/commit/ba50224ead363fdf6edc019ce6daf2fb4b1ac781
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp

Log Message:
-----------
[C$] Fix XDOC parent.


Commit: df49650d8f546c81ae6d414f351ba98d99cf564b
https://github.com/acl2/acl2/commit/df49650d8f546c81ae6d414f351ba98d99cf564b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-28 (Sat, 28 Feb 2026)

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

Log Message:
-----------
[C$] Fix XDOC topic name.


Commit: 526c52e406a8ffce7e1ebfcb0e8ebe4b337918b3
https://github.com/acl2/acl2/commit/526c52e406a8ffce7e1ebfcb0e8ebe4b337918b3
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/kestrel/crypto/primes/koala-bear.lisp

Log Message:
-----------
[primes] Fix XDOC parent.


Commit: dcea093618baebab911ebd5f2035222bdcec1cbd
https://github.com/acl2/acl2/commit/dcea093618baebab911ebd5f2035222bdcec1cbd
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M README.md
M all-files.txt
M books/doc/more-topics.lisp
M books/doc/publications.acl2
A books/kestrel/air/acl2-customization.lsp
A books/kestrel/air/cert.acl2
A books/kestrel/air/model-0/acl2-customization.lsp
A books/kestrel/air/model-0/air/acl2-customization.lsp
A books/kestrel/air/model-0/air/correctness.lisp
A books/kestrel/air/model-0/air/example.lisp
A books/kestrel/air/model-0/air/field-encoding.lisp
A books/kestrel/air/model-0/air/field.lisp
A books/kestrel/air/model-0/air/pfcs-constraints.lisp
A books/kestrel/air/model-0/air/pfcs-lifting.lisp
A books/kestrel/air/model-0/air/traces.lisp
A books/kestrel/air/model-0/cert.acl2
A books/kestrel/air/model-0/language/abstract-syntax.lisp
A books/kestrel/air/model-0/language/acl2-customization.lsp
A books/kestrel/air/model-0/language/dynamic-semantics.lisp
A books/kestrel/air/model-0/language/example.lisp
A books/kestrel/air/model-0/language/input-output-semantics.lisp
A books/kestrel/air/model-0/language/static-semantics.lisp
A books/kestrel/air/model-0/library-extensions.lisp
A books/kestrel/air/model-0/package.lsp
A books/kestrel/air/model-0/portcullis.acl2
A books/kestrel/air/model-0/portcullis.lisp
A books/kestrel/air/model-0/top.lisp
A books/kestrel/air/package.lsp
A books/kestrel/air/portcullis.acl2
A books/kestrel/air/portcullis.lisp
A books/kestrel/air/top.lisp
M books/kestrel/arm/def-inst.lisp
M books/kestrel/arm/instructions.lisp
M books/kestrel/arm/memory.lisp
M books/kestrel/arm/pseudocode.lisp
M books/kestrel/arm/state.lisp
M books/kestrel/arm/tests/simple.lisp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/arm/unroller.lisp
M books/kestrel/axe/bv-rules-axe.lisp
M books/kestrel/axe/imported-symbols.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/risc-v/unroller.lisp
M books/kestrel/axe/rule-lists.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/bvnot.lisp
M books/kestrel/bv/bvuminus.lisp
M books/kestrel/bv/logext.lisp
M books/kestrel/bv/rules.lisp
M books/kestrel/bv/rules3.lisp
M books/kestrel/bv/sbvlt.lisp
M books/kestrel/c/syntax/langdef-mapping-inverse.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/top-doc.lisp
M books/kestrel/top.lisp
M books/kestrel/utilities/defstobj-plus-tests.lisp
M books/kestrel/utilities/ensure-rules-known.lisp
M books/misc/check-acl2-exports.lisp
M books/projects/abnf/parsing-tools/defdefparse.lisp
M books/projects/pfcs/.sys/le...@useless-runes.lsp
M books/projects/pfcs/.sys/par...@useless-runes.lsp
M books/projects/pfcs/.sys/syntax-ab...@useless-runes.lsp
M books/projects/pfcs/abstract-syntax-operations.lisp
M books/projects/pfcs/abstract-syntax-trees.lisp
M books/projects/pfcs/abstract-syntax.lisp
M books/projects/pfcs/convenience-constructors.lisp
M books/projects/pfcs/grammar.lisp
M books/projects/pfcs/lexer.lisp
M books/projects/pfcs/parser.lisp
M books/projects/pfcs/syntax-abstraction.lisp
M books/projects/pfcs/tokenizer.lisp
M books/projects/set-theory/restrict.lisp
M books/projects/x86isa/machine/catalogue-data.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/padd.lisp
A books/projects/x86isa/machine/instructions/pmadd.lisp
A books/projects/x86isa/machine/instructions/pmul.lisp
M books/projects/x86isa/machine/instructions/psub.lisp
M books/projects/x86isa/machine/instructions/top.lisp
M books/system/apply/apply-prim.lisp
M books/system/doc/acl2-doc.lisp
M books/system/to-do.txt
M books/workshops/2025/kwan/rv-state.lisp
M defpkgs.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M interface-raw.lisp

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


Commit: 96925c12cb8f12d593c2992cf33a3c0c7eeaebab
https://github.com/acl2/acl2/commit/96925c12cb8f12d593c2992cf33a3c0c7eeaebab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/kestrel/ethereum/rlp/top.lisp

Log Message:
-----------
[Ethereum] Fix XDOC references.


Commit: 3a6790217185957df4513568c20563b1709dd070
https://github.com/acl2/acl2/commit/3a6790217185957df4513568c20563b1709dd070
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/kestrel/air/model-0/top.lisp

Log Message:
-----------
[AIR] Fix XDOC reference.


Commit: 551bc59a3cb3c0e8f9e692ad4d1bf49ec619f8ba
https://github.com/acl2/acl2/commit/551bc59a3cb3c0e8f9e692ad4d1bf49ec619f8ba
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/validation-information.lisp

Log Message:
-----------
[C$] Fix predicate name (was causing an XDOC issue).


Commit: 305131d550f7508ee828bd41b82ddd065d587bc9
https://github.com/acl2/acl2/commit/305131d550f7508ee828bd41b82ddd065d587bc9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-28 (Sat, 28 Feb 2026)

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

Log Message:
-----------
[C$] Fix XDOC parent.


Commit: 6bb038dd1a9240573a310a15102b40c9f41585e1
https://github.com/acl2/acl2/commit/6bb038dd1a9240573a310a15102b40c9f41585e1
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/kestrel/c/syntax/concrete-syntax.lisp

Log Message:
-----------
[C$] Remove obsolete XDOC reference.


Commit: 2363e5af0455e852ac034d32f3e76ed21fb11c07
https://github.com/acl2/acl2/commit/2363e5af0455e852ac034d32f3e76ed21fb11c07
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-02-28 (Sat, 28 Feb 2026)

Changed paths:
M books/projects/aleo/leo/early-version/definition/concrete-syntax.lisp
M books/projects/aleo/leo/early-version/definition/format-strings.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-and.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-all.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert-true.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-assert.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-if.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-nand.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-nor.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-not.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-or.lisp
M books/projects/aleo/vm/circuits/pfcs/boolean-xor.lisp
M books/projects/aleo/vm/circuits/pfcs/field-add.lisp
M books/projects/aleo/vm/circuits/pfcs/field-assert-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-assert-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-checked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-flagged.lisp
M books/projects/aleo/vm/circuits/pfcs/field-div-unchecked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-double.lisp
M books/projects/aleo/vm/circuits/pfcs/field-eq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-if.lisp
M books/projects/aleo/vm/circuits/pfcs/field-inv-checked.lisp
M books/projects/aleo/vm/circuits/pfcs/field-inv-flagged.lisp
M books/projects/aleo/vm/circuits/pfcs/field-mul.lisp
M books/projects/aleo/vm/circuits/pfcs/field-neg.lisp
M books/projects/aleo/vm/circuits/pfcs/field-neq.lisp
M books/projects/aleo/vm/circuits/pfcs/field-square.lisp
M books/projects/aleo/vm/circuits/pfcs/field-sub.lisp
M books/projects/aleo/vm/circuits/top.lisp
M books/projects/aleo/vm/language/grammar.lisp

Log Message:
-----------
[Aleo] Fix XDOC parents.


Compare: https://github.com/acl2/acl2/compare/c0d3f5729fae...2363e5af0455
Reply all
Reply to author
Forward
0 new messages