[acl2/acl2] 9fb9f7: [ATC] Update some file references in the tutorial.

[Alessandro Coglio]

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

Changed paths:
M books/kestrel/c/atc/tutorial.lisp

Log Message:
-----------
[ATC] Update some file references in the tutorial.

Thank you for Eric McCarthy for noticing the stale references.



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

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

Home: https://github.com/acl2/acl2
Commit: 9fb9f75c893e1a00edb61615ccd342dcb9f36277
https://github.com/acl2/acl2/commit/9fb9f75c893e1a00edb61615ccd342dcb9f36277
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-03 (Wed, 03 Dec 2025)

Changed paths:
M books/kestrel/c/atc/tutorial.lisp

Log Message:
-----------
[ATC] Update some file references in the tutorial.

Thank you for Eric McCarthy for noticing the stale references.

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

Date: 2025-12-03 (Wed, 03 Dec 2025)

Changed paths:

M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/parsers/pe-tools.lisp

Log Message:
-----------
Merge commit 'f3fec20eedc3601c6a18e07edb844ee60021d4bd' into HEAD


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

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/execution-without-function-calls.lisp
M books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp

Log Message:
-----------
[C] Improve dynamic semantics.

Add and use `exec-expr-list`, mutually recursive with the other execution
functions. This eliminates the use of `exec-expr-pure-list` from those
functions.

Extend and adapt theorems about dynamic semantics.

Extend notion of limit for pure expression execution to lists of expressions,
and add theorems relating `exec-expr-list` to `exec-expr-pure-list`, similar to
the ones relating `exec-expr` and `exec-expr-pure`.


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

Changed paths:
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp

Log Message:
-----------
[ATC] Adapt to changes to dynamic semantics.


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

Changed paths:
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/parsers/pe-tools.lisp

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


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/f3fec20eedc3...fd800b5c9308