[humuhumu33]

Fixes #241 on the v0.5 line.

lexlean::surface::module::locate found a module by text search: for each kind in the order semantic, tooling, core, it took the first \begin{<kind>} and the last \end{<kind>}. It now finds the module the structural parser opens. It walks the control atoms the way the scanner reads them, where the escape \\ is one atom. It takes the first environment after \begin{lexlean} and ends the body at the first \end control, which must close that environment. A marker that a string quotes (\\begin{semanticmodule} in the notation) is therefore never a module's marker.

Row (R3)

AU-14 (build, suite authoring, sections §17.21, §21.2, §24.8). It is added in spec/src/IdsAU.lex.tex, with a §17.21 bullet in Chapter17. SPEC.md, model/ids.toml and CONFORMANCE.md are regenerated, and the register now has 444 rows.

A source's module is the environment the structural parser opens: lexlean::surface::module::locate takes the first environment after the header and ends its body at the first end control atom, so a tooling or core module whose strings quote the begin and end markers of another kind is read by the authoring API, formatted, and decoded as its own kind and contributes its data form to the compiler-semantics ID, a module whose body holds an unescaped end marker is refused with LLP2003 and is found as no module, and on every committed source the parser reads the module found is the one it opens.

Scenario and case

The @AU-14 @build scenario is in features/suites/authoring.feature. The conformance_au_14 case does three things:

• Sweeps every committed source. For each .lex.tex the structural parser reads, it checks that locate finds the kind, body and data range the parser opens. The spec/ chapters are in this set: they are semantic modules that quote the tooling and core markers.
• Plants five modules that quote markers. Two are tooling modules (tests/tooling/core with a string quoting the semantic begin marker, or both semantic markers). Three are core modules (the AU-10 small module with a string node quoting the semantic begin marker, both semantic markers, or both tooling markers). Each must read through sdk::read_module and module_kind as its own kind. Each must contribute its data form through identity_bytes, with the expected bytes built from the parser's range, not from locate. Each must have fmt restore its canonical notation from another layout. The tooling plants are linked with with_tooling. The core plants go through the engine, where fmt --check must give LLL1003, and CoreModule::from_source must decode them.
• Plants an unescaped \end{semanticmodule} in a core body. The parser must refuse it with LLP2003, and locate must find no module.

Commit 3497787 (row, scenario, case) fails on the unfixed locate at the first plant:

a tooling module quoting the semantic begin marker: the parser opens a toolingmodule, and no module is located

Callers exercised

These are probe results on release/v0.5 2959a4d, before and after the fix. Full table in VERIFICATION.md.

Caller	Before	After
surface/identity.rs:35	all five plants contribute their own notation bytes, with no diagnostic	the data form
fmt.rs:1050	tooling and core plants are left in another layout; for core, fmt --check passes it	restores the canonical notation; fmt --check is LLL1003
ir/core.rs:747	a native core source holds exactly one core payload	decodes
sdk::read_module	"states no … module", or read as the quoted kind and refused	reads its own kind
calculus/rust/scaffold.rs:481	decodes (a semantic module was never misread)	decodes
lexlean check / fmt --check on an adapter copy	LLT4013	LLT4013 (the CLI refuses tooling outside the embedded projects)

The old and the fixed locate agree on every one of the 881 committed sources, of which 819 hold a module.

Plants (VERIFICATION.md)

Each plant is one edit of the fixed locate, undone before the next, and each turns conformance_au_14 red:

1. The text search restored. The first tooling plant is found as no module.
2. The body ends at the last end marker found by text search. "a module is located whose environment an unescaped end marker closes".
3. The escape read as a lone backslash. The committed sweep fails on spec/src/Chapter16.lex.tex.

Run locally (WSL, Linux x86-64)

• cargo fmt --all -- --check passed.
• cargo xtask validate-model passed.
• cargo xtask validate-spec-links passed with 444 rows.
• cargo xtask check-test-inventory passed.
• cargo clippy -p lexlean -p repo-conformance --all-targets --all-features -- -D warnings passed.
• cargo test -p lexlean --lib passed 211 tests.
• conformance_au_01 to conformance_au_14 passed all 14.
• The bdd meta-gate passed 5 tests.

The rest of just vv was not run locally.

The fix commit also corrects two assertions of the case's own: the expected data form now starts after the opening marker, and the two-marker quote check escapes every backslash. Neither is reached before the red line above.

🤖 Generated with Claude Code

[humuhumu33]

Pushed fe5d927 (README only): the capability table range is now AU-01..AU-14, answering the conformance_rp_11 assertion "the range ends at the register's last AU ID" (left AU-14, right AU-13); the count sentence now reads 444 (it would have failed next). Locally: validate-model clean at 444 ids, conformance_rp_11 passes.

[afflom]

Maintainer: read, and in the release/v0.5 queue. The head is green and mergeable; keep it so. The release/v0.4 landings (#255 in regeneration now, then #259, #262, #264, #265, #293, the bootstrap trio #258/#266/#282, #247, #256, and #261) hold the gate and the review agents first, by the owner's direction. The v0.5 lane is reviewed in this order as agents free up: #285, #290, #286, #287, #288, #289. Read fe5d92707: the AU range and the 444 count are the right answers to conformance_rp_11; the count will need the v0.5 base's value at the time of the merge, so expect one more count-only round then.

---

Generated by Claude Code

[afflom]

Maintainer review of fe5d92707: accepted, one small push before the merge.

locate (surface/module.rs:168-250) now walks control atoms as the scanner does, skips \begin{lexlean}, takes the first \begin{X} of the three kinds and ends the body at the first \end atom, which must close that kind; that is exactly grammar::structural::parse_module (structural.rs:1151-1226). R5: every slice boundary follows an ASCII byte or a find, malformed \begin/\end returns None. R4 clean. AU-14 statement byte-identical in ids.toml, the scenario, §31 and IdsAU.lex.tex; conformance_au_14 sweeps every committed source plus the quoting plants and the unescaped-\end plant; three plants recorded with their red lines. Count sites consistent at 444; identity-neutral (819/881 committed sources locate identically). Merge against 0694c7ca6 is clean.

The push: a CHANGELOG Unreleased bullet for AU-14/#241 ending "Register 444", the line's convention (see the #244 entry). A doc line on module.rs:206 returning None for a header \begin without {…} would be welcome but is not required. Then I merge on green; this PR goes before #288, which takes the register to 445.

---

Generated by Claude Code

[afflom]

Maintainer: merged into release/v0.5 at bde798bd6 (merge commit) and #241 closed by hand. The line is at register 444. The CHANGELOG bullet for AU-14 rides #288's round, which already touches the Unreleased top: add it there ("Register 445" after #288's own row).

---

Generated by Claude Code