[acl2/acl2] 9fedd0: [STS safety] Relax checks on structs in arrays.

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 9fedd04b8e4f50e0fb38a84fae835497ccb3f3b8
https://github.com/acl2/acl2/commit/9fedd04b8e4f50e0fb38a84fae835497ccb3f3b8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp

Log Message:
-----------
[STS safety] Relax checks on structs in arrays.

These are now supported by the transformation.


Commit: feb5e40fc34fd5142f6bbb2ebc3d9c49b029bca9
https://github.com/acl2/acl2/commit/feb5e40fc34fd5142f6bbb2ebc3d9c49b029bca9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/json-rpc/struct-type-split.lisp
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

Log Message:
-----------
[STS] `:unsafe t/nil` => `:safety-checks nil/t`.


Commit: 5904d829fce1ab7144e2a06cf5eb739be039308e
https://github.com/acl2/acl2/commit/5904d829fce1ab7144e2a06cf5eb739be039308e
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

Log Message:
-----------
[STS] Enable safety checks in several tests.


Commit: 326e7379260e27037eb4284be147ff48748331f2
https://github.com/acl2/acl2/commit/326e7379260e27037eb4284be147ff48748331f2
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

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

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


Compare: https://github.com/acl2/acl2/compare/ac3c69d27b62...326e7379260e

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

[Alessandro Coglio]

Branch: refs/heads/testing

[acl2buildserver]

Branch: refs/heads/testing-kestrel

Commit: 4c8e4fbfc2adda3605063572f974e32ef7febb7d
https://github.com/acl2/acl2/commit/4c8e4fbfc2adda3605063572f974e32ef7febb7d

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:

M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

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

[STS] Relax a safety check.


Commit: 26cf30dd3eaf07deb2a647b5fbe268a2de25c38a
https://github.com/acl2/acl2/commit/26cf30dd3eaf07deb2a647b5fbe268a2de25c38a

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

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

[STS] Remove comments that no longer apply.


Commit: 7705774e8bc26e95ba31272e03f474bf10a352aa
https://github.com/acl2/acl2/commit/7705774e8bc26e95ba31272e03f474bf10a352aa

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp

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

[STS safety] Pass additional information to some code.

This is so we can look up struct types by tag.


Commit: ddd827ca4320a45d0ba7292a857e3d68b44594d3
https://github.com/acl2/acl2/commit/ddd827ca4320a45d0ba7292a857e3d68b44594d3

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp

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

[STS safety] Add an artificial counter.

In preparation for looking up struct types by tag.


Commit: c6bc8754bb0ffc7d92ceb12526c755c24758fe94
https://github.com/acl2/acl2/commit/c6bc8754bb0ffc7d92ceb12526c755c24758fe94

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp

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

[STS safety] Improve some checks.

When checking types, when encountering a struct or union tag, look it up in the
validation table and in the completions, in order to go on to checking its
members.


Commit: 0657ac055f0239a512f9849c6869fd8a0a914461
https://github.com/acl2/acl2/commit/0657ac055f0239a512f9849c6869fd8a0a914461

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-safety.lisp

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

[STS safety] Relax a check.

This is now covered by our extended check on types. But we may need to add the
latter to some additional type annotations in the ASTs, which we'll look at
next.


Commit: c66dcf92375ef206e25abbc523e00b3b30a42cec
https://github.com/acl2/acl2/commit/c66dcf92375ef206e25abbc523e00b3b30a42cec

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

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

[STS] Enable safety checks in all the remaining tests.


Commit: 566fe539ee37046e76e2a26826cbe4a191b94092
https://github.com/acl2/acl2/commit/566fe539ee37046e76e2a26826cbe4a191b94092
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-07-28 (Tue, 28 Jul 2026)

Changed paths:

M books/kestrel/arm/rules.lisp
M books/kestrel/axe/rules3.lisp
R books/kestrel/bv/.sys/ru...@useless-runes.lsp
M books/kestrel/bv/rules.lisp
M books/kestrel/file-io-light/open-output-channel.lisp
M books/kestrel/file-io-light/read-bytes-from-channel.lisp
M books/kestrel/json-parser/parse-json.lisp

Log Message:
-----------
Merge commit '7e60429435ee0b26527f61f9190a2e84cdec003d' into HEAD


Compare: https://github.com/acl2/acl2/compare/7e60429435ee...566fe539ee37