[acl2/acl2] b6071a: [Remora] Improve some doc.

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: b6071af120d4ba7dedba3b970785d6ab1c203e71
https://github.com/acl2/acl2/commit/b6071af120d4ba7dedba3b970785d6ab1c203e71
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/remora/static-semantics.lisp

Log Message:
-----------
[Remora] Improve some doc.


Commit: 5608ecdac05752549763fa260cd08fb4d6a62f25
https://github.com/acl2/acl2/commit/5608ecdac05752549763fa260cd08fb4d6a62f25
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/remora/package.lsp

Log Message:
-----------
[Remora] Avoid importing two symbols.


Commit: 00696e79111d186a8ad97410e87f78a9b2f1615d
https://github.com/acl2/acl2/commit/00696e79111d186a8ad97410e87f78a9b2f1615d
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
A books/kestrel/remora/dynamic-semantics.lisp
M books/kestrel/remora/top.lisp

Log Message:
-----------
[Remora] Start dynamic semantics.


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

Changed paths:
M books/kestrel/remora/dynamic-semantics.lisp
A books/kestrel/remora/values.lisp

Log Message:
-----------
[Remora] Initial model of values.


Commit: 165158eb3dbf1ef7ac609f6b34d30d300659a466
https://github.com/acl2/acl2/commit/165158eb3dbf1ef7ac609f6b34d30d300659a466
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/fty/deffold-map-doc.lisp
M books/kestrel/fty/deffold-map-tests.lisp
M books/kestrel/fty/deffold-map.lisp
M books/kestrel/fty/deffold-reduce-doc.lisp
M books/kestrel/fty/deffold-reduce-tests.lisp
M books/kestrel/fty/deffold-reduce.lisp

Log Message:
-----------
[FTY] Extend `deffold-reduce` and `deffold-map`.

Add a mandatory `:name` input that specifies the name of the XDOC topic and the
name of the ruleset, where the latter is `<name>-rules`.

This replaces the previously hardwired `abstract-syntax-<suffix>` and
`abstract-syntax-<suffix>-rules` for the XDOC topic and for the ruleset, which
are too specific to abstract syntax, even though the folds work on any kinds of
fixtypes.

All the existing calls of these two macros will be updated, in upcoming commits,
in a way that does not change the previous names, but authors of those calls
might want to take advantage of the new capability to generate better names.


Commit: 064f50bd3590f5e846a254842c01851849378bf9
https://github.com/acl2/acl2/commit/064f50bd3590f5e846a254842c01851849378bf9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/remora/abstract-syntax-core.lisp
M books/kestrel/remora/abstract-syntax-variable-operations.lisp
M books/kestrel/remora/abstract-syntax-well-formed.lisp
M books/kestrel/remora/desugaring.lisp
A books/kestrel/remora/interpreter.lisp
M books/kestrel/remora/ispace-equivalence.lisp
M books/kestrel/remora/printer.lisp

Log Message:
-----------
[Remora] Adapt to changes to `deffold-...`.


Commit: 39891202e77579d2cf4746bb5341c8f53181f95b
https://github.com/acl2/acl2/commit/39891202e77579d2cf4746bb5341c8f53181f95b
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
M books/kestrel/c/language/decimal-0-to-octal-0.lisp

Log Message:
-----------
[C] Adapt to changes to `deffole-...`.


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

Changed paths:
M books/kestrel/c/syntax/ascii-identifiers.lisp
M books/kestrel/c/syntax/purity.lisp
M books/kestrel/c/syntax/standard.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/unambiguity.lisp
M books/kestrel/c/syntax/validation-information.lisp

Log Message:
-----------
[C$] Adapt to changes to `deffold-...`.


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

Changed paths:
M books/kestrel/c/transformation/rename.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/utilities/add-attributes.lisp
M books/kestrel/c/transformation/utilities/collect-idents.lisp
M books/kestrel/c/transformation/utilities/rename-fn.lisp

Log Message:
-----------
[C2C] Adapt to changes to `deffold-...`.


Commit: 606dcae2f7b4ca694c1a3551b1cc4cfbe4a5b3ab
https://github.com/acl2/acl2/commit/606dcae2f7b4ca694c1a3551b1cc4cfbe4a5b3ab
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-05-04 (Mon, 04 May 2026)

Changed paths:
R books/kestrel/acl2-arrays/.sys/make-emp...@useless-runes.lsp
M books/kestrel/acl2-arrays/.sys/make-into-ar...@useless-runes.lsp
A books/kestrel/acl2-arrays/.sys/new-a...@useless-runes.lsp
M books/kestrel/acl2-arrays/acl2-arrays.lisp
A books/kestrel/acl2-arrays/alist-to-array1-with-len.lisp
A books/kestrel/acl2-arrays/alist-to-array1.lisp
M books/kestrel/acl2-arrays/aref1.lisp
M books/kestrel/acl2-arrays/array-to-alist.lisp
M books/kestrel/acl2-arrays/compress1.lisp
R books/kestrel/acl2-arrays/make-empty-array.lisp
R books/kestrel/acl2-arrays/make-into-array-with-len.lisp
R books/kestrel/acl2-arrays/make-into-array.lisp
A books/kestrel/acl2-arrays/new-array1.lisp
M books/kestrel/acl2-arrays/top.lisp
M books/kestrel/acl2-arrays/typed-acl2-arrays-tests.lisp
M books/kestrel/acl2-arrays/typed-acl2-arrays.lisp
M books/kestrel/axe/.sys/get-di...@useless-runes.lsp
M books/kestrel/axe/arm/rule-lists.lisp
M books/kestrel/axe/bounded-dag-parent-arrayp.lisp
M books/kestrel/axe/concretize-with-contexts.lisp
M books/kestrel/axe/contexts.lisp
M books/kestrel/axe/contexts2.lisp
M books/kestrel/axe/crunch-dag.lisp
M books/kestrel/axe/crunch-dag2.lisp
M books/kestrel/axe/dag-array-builders.lisp
M books/kestrel/axe/dag-array-builders2.lisp
M books/kestrel/axe/dag-arrays.lisp
M books/kestrel/axe/dag-parent-array-with-name.lisp
M books/kestrel/axe/dag-parent-arrayp.lisp
M books/kestrel/axe/dag-size-fast.lisp
M books/kestrel/axe/dag-size-sparse-tests.lisp
M books/kestrel/axe/dag-size-sparse.lisp
M books/kestrel/axe/dag-size.lisp
M books/kestrel/axe/dag-to-term-with-lets.lisp
M books/kestrel/axe/dagify.lisp
M books/kestrel/axe/dagify0.lisp
M books/kestrel/axe/depth-array.lisp
M books/kestrel/axe/elim.lisp
M books/kestrel/axe/equivalence-checker.lisp
M books/kestrel/axe/evaluate-test-case.lisp
M books/kestrel/axe/evaluator-tests.lisp
M books/kestrel/axe/extract-dag-array.lisp
M books/kestrel/axe/find-probable-facts-simple.lisp
M books/kestrel/axe/find-probable-facts.lisp
M books/kestrel/axe/get-disjuncts.lisp
M books/kestrel/axe/jvm/lifter.lisp
M books/kestrel/axe/jvm/rules-in-rule-lists-jvm.lisp
M books/kestrel/axe/make-assumption-array.lisp
M books/kestrel/axe/make-dag-indices.lisp
M books/kestrel/axe/make-evaluator-tests.lisp
M books/kestrel/axe/make-evaluator.lisp
M books/kestrel/axe/make-prover-simple.lisp
M books/kestrel/axe/make-rewriter-simple.lisp
M books/kestrel/axe/make-term-into-dag-array-basic.lisp
M books/kestrel/axe/make-term-into-dag-array-simple.lisp
M books/kestrel/axe/memoization.lisp
M books/kestrel/axe/merge-dag-into-dag-quick.lisp
M books/kestrel/axe/node-replacement-array.lisp
M books/kestrel/axe/normalize-xors.lisp
A books/kestrel/axe/pre-stp-rules.lisp
M books/kestrel/axe/prove-with-stp.lisp
M books/kestrel/axe/prove-with-stp2.lisp
M books/kestrel/axe/prover-common.lisp
M books/kestrel/axe/prover.lisp
M books/kestrel/axe/prune-dag-approximately.lisp
M books/kestrel/axe/prune-with-contexts.lisp
M books/kestrel/axe/rebuild-literals.lisp
M books/kestrel/axe/rebuild-nodes.lisp
M books/kestrel/axe/rebuild-nodes2.lisp
M books/kestrel/axe/remove-gaps.lisp
M books/kestrel/axe/renaming-array.lisp
M books/kestrel/axe/rewriter-alt.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/risc-v/rule-lists.lisp
M books/kestrel/axe/rule-lists.lisp
M books/kestrel/axe/rules-in-rule-lists.lisp
M books/kestrel/axe/splitting.lisp
M books/kestrel/axe/substitute-vars2.lisp
M books/kestrel/axe/supporting-nodes.lisp
M books/kestrel/axe/supporting-vars.lisp
M books/kestrel/axe/tactic-prover.lisp
M books/kestrel/axe/top.lisp
M books/kestrel/axe/translate-dag-to-stp.lisp
M books/kestrel/axe/translation-array.lisp
M books/kestrel/axe/wf-dagp.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/jvm/call-stacks.lisp
M books/kestrel/jvm/frames.lisp
M books/kestrel/jvm/operand-stacks.lisp
M books/kestrel/x86/support32.lisp

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


Compare: https://github.com/acl2/acl2/compare/bc3f887116f8...606dcae2f7b4

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