Documentation for incremental module definitions#1087
Open
Gustavo2622 wants to merge 1 commit into
Open
Conversation
Gustavo2622
force-pushed
the
doc-module-update
branch
from
July 24, 2026 11:27
c1e8d7b to
108648c
Compare
Gustavo2622
marked this pull request as ready for review
July 24, 2026 11:28
Member
|
Change the target branch to avoid the commit count failure. The target will automatically change when we merge the other PR. |
Gustavo2622
force-pushed
the
fix-module-update-bases
branch
from
July 26, 2026 15:36
2cd9b21 to
ba119b8
Compare
Adds doc/language/module-update.rst, documenting `module M' = M with
{...}`: syntax, the copy/share semantics, restrictions, and worked
examples (ghost-state instrumentation, statement and result rewrites,
loop edits, match-branch collapse, functor and sub-module updates).
The code-position language (shared by the program tactics and by module
updates) is factored out into its own page,
doc/language/code-positions.rst, which module-update.rst references.
The section on sub-module and applied-functor bases documents the
semantics introduced by the parent commit (sound module updates on
sub-module and applied-functor bases); its example is executable and
mirrors the regression tests in tests/module-update-bases.ec. This
change is meant to be merged after that fix.
Both pages are marked :orphan: until a language-reference toctree
lands.
Gustavo2622
force-pushed
the
doc-module-update
branch
from
July 26, 2026 15:37
108648c to
bcab22f
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This adds documentation for the incremental / fine-grained module definition syntax / functionality.
It depends on #1086