[acl2/acl2] 98fe0a: [C$] Add info field to param-declon.

0 views
Skip to first unread message

Grant Jurgensen

unread,
May 29, 2026, 11:09:10 AM (3 days ago) May 29
to acl2-...@googlegroups.com
Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 98fe0a6a24af0d3cdc172d73eb4a254c4060e9c0
https://github.com/acl2/acl2/commit/98fe0a6a24af0d3cdc172d73eb4a254c4060e9c0
Author: Grant Jurgensen <gr...@kestrel.edu>
Date: 2026-05-29 (Fri, 29 May 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/validation-information.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
[C$] Add info field to param-declon.


Commit: 2d7e73659f0f46a49b8cb6871d4998d843146931
https://github.com/acl2/acl2/commit/2d7e73659f0f46a49b8cb6871d4998d843146931
Author: Grant Jurgensen <gr...@kestrel.edu>
Date: 2026-05-29 (Fri, 29 May 2026)

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

Log Message:
-----------
[C$] Modify param-declon annotation info

The type is now optional, to accomodate param-declons that do not
represent actual parameters (i.e. for the special `foo(void)` syntax).


Compare: https://github.com/acl2/acl2/compare/f3de74de64d3...2d7e73659f0f

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

acl2buildserver

unread,
May 29, 2026, 6:08:01 PM (3 days ago) May 29
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: cb108a3ff8f9b603b6180cfb8a66336e47656f71
https://github.com/acl2/acl2/commit/cb108a3ff8f9b603b6180cfb8a66336e47656f71
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-29 (Fri, 29 May 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
Merge commit '2d7e73659f0f46a49b8cb6871d4998d843146931' into HEAD


Compare: https://github.com/acl2/acl2/compare/138259282a81...cb108a3ff8f9

acl2buildserver

unread,
May 29, 2026, 6:08:39 PM (3 days ago) May 29
to acl2-...@googlegroups.com
Branch: refs/heads/testing

Alessandro Coglio

unread,
May 29, 2026, 11:42:04 PM (3 days ago) May 29
to acl2-...@googlegroups.com
Branch: refs/heads/testing-user-01
Commit: 07cd90550d926810d09bbe2e7e97cc6038e612d6
https://github.com/acl2/acl2/commit/07cd90550d926810d09bbe2e7e97cc6038e612d6
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-29 (Fri, 29 May 2026)

Changed paths:
M books/projects/x86isa/utils/segmentation-structures.lisp

Log Message:
-----------
[X86ISA] Improve and update some doc.


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

Changed paths:
A books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/c/syntax/input-files-doc.lisp
A books/kestrel/c/syntax/null-pointer-constants.lisp
M books/kestrel/c/syntax/package.lsp
M books/kestrel/c/syntax/top.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/uid.lisp
A books/kestrel/c/syntax/validation-annotations.lisp
R books/kestrel/c/syntax/validation-information.lisp
A books/kestrel/c/syntax/validation-tables.lisp
M books/kestrel/c/syntax/validation.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/copy-fn.lisp
M books/kestrel/c/transformation/input-processing.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0-doc.lisp
M books/kestrel/c/transformation/split-all-gso-doc.lisp
M books/kestrel/c/transformation/split-gso-doc.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/qualified-ident.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp
M books/kestrel/c/transformation/wrap-fn-doc.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
A books/projects/hol-in-acl2/LICENSE

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


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

Changed paths:
M books/projects/x86isa/utils/segmentation-structures.lisp

Log Message:
-----------
[X86ISA] Move some code to appropriate place.

I.e. after the things that is referenced in its doc.


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

Changed paths:
M books/projects/x86isa/utils/segmentation-structures.lisp

Log Message:
-----------
[X86ISA] Fix and update some doc.


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

Changed paths:
M books/projects/x86isa/utils/utilities.lisp

Log Message:
-----------
[X86ISA] Fix and improve some doc.


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

Changed paths:
M books/projects/x86isa/utils/segmentation-structures.lisp

Log Message:
-----------
[X86ISA] Improve/extend some doc.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp

Log Message:
-----------
Merge commit '2d7e73659f0f46a49b8cb6871d4998d843146931' into HEAD


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

Changed paths:
M books/projects/x86isa/utils/segmentation-structures.lisp

Log Message:
-----------
[X86ISA] Extend and improve some doc.

In particular, eliminate the mention that certain fields are _not_ ignored in
64-bit mode according to the Intel manual, because the Intel manual does not
seem to say that they are in fact used in 64-bit mode.


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

Changed paths:
M books/projects/x86isa/utils/segmentation-structures.lisp

Log Message:
-----------
[X86ISA] Extend/improve documentation.


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

Changed paths:

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


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

Changed paths:
M books/projects/x86isa/utils/paging-structures.lisp

Log Message:
-----------
[X86ISA] Fix typos in doc comments.


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

Changed paths:
M books/projects/x86isa/utils/segmentation-structures.lisp

Log Message:
-----------
[X86ISA] Fix and improve some doc.


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

Changed paths:
M books/projects/x86isa/machine/instructions/bit.lisp

Log Message:
-----------
[X86ISA] Improve some doc and code.


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

Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp

Log Message:
-----------
[X86ISA] Add LZCNT.


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

Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp

Log Message:
-----------
[X86ISA] Make a function name more consistent.


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

Changed paths:
M books/projects/x86isa/machine/instructions/fp/bitscan.lisp

Log Message:
-----------
[X86ISA] Remove unneeded book inclusion.


Commit: f8b0a5bdec74d91a744ca694619b025d8eaba1f1
https://github.com/acl2/acl2/commit/f8b0a5bdec74d91a744ca694619b025d8eaba1f1
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2026-05-29 (Fri, 29 May 2026)

Changed paths:
M books/projects/acl2-in-hol/.acl2holrc.bash

Log Message:
-----------
Fixed a bug in books/projects/acl2-in-hol/.acl2holrc.bash, in the case that the value of environment variable ACL2 is a string that is a symbolic link rather than a filename.

Thanks to Quan Luu for explaining this problem on Zulip and to Grant Jurgensen and Eric Smith for participating in the ensuing discussion.


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

Changed paths:
M books/projects/x86isa/machine/instructions/bit.lisp
R books/projects/x86isa/machine/instructions/fp/bitscan.lisp
M books/projects/x86isa/machine/instructions/fp/top.lisp

Log Message:
-----------
[X86ISA] Move some code to more appropriate place.


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

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/constant-propagation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp
M books/kestrel/c/transformation/wrap-fn.lisp
M books/projects/acl2-in-hol/.acl2holrc.bash

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


Commit: 4f70ba53940690632347c0b04cd02106fd78ca46
https://github.com/acl2/acl2/commit/4f70ba53940690632347c0b04cd02106fd78ca46
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-05-29 (Fri, 29 May 2026)

Changed paths:
M books/kestrel/fty/string-set.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/package.lsp

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


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

Changed paths:
M books/kestrel/fty/string-set.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/package.lsp

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


Compare: https://github.com/acl2/acl2/compare/81ddd786d829...80f0669b60ee
Reply all
Reply to author
Forward
0 new messages