[acl2/acl2] 3da9e7: [C] Update some doc.

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 3da9e74b0a766269be27b1cfb383f46623eb29f7
https://github.com/acl2/acl2/commit/3da9e74b0a766269be27b1cfb383f46623eb29f7
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp

Log Message:
-----------
[C] Update some doc.


Commit: f3a717c1a3e42181ea7a679665d6c98b3ddaf375
https://github.com/acl2/acl2/commit/f3a717c1a3e42181ea7a679665d6c98b3ddaf375
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/pure-expression-execution.lisp

Log Message:
-----------
[C] Move some code.

Move `exec-expr-list` and `exec-expr-pure-list` away from the main file with the
dynamic semantics, because they are no longer part of the definition.


Commit: fd800b5c930847065d87e7cad0e0be451832cd9f
https://github.com/acl2/acl2/commit/fd800b5c930847065d87e7cad0e0be451832cd9f
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
A books/kestrel/c/atc/pure-expression-execution.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
R books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp

Log Message:
-----------
[C] [ATC] [C2C] Move pure expression execution to ATC.

This is now only used by ATC; see added documentation.

We also eliminate a no-longer-needed book inclusion from C2C.


Compare: https://github.com/acl2/acl2/compare/f7263b2cb69e...fd800b5c9308

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

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing