feat(language): a file says what it reads under one given key

[FabianHofmann]

Prompt: implement dev/composition/plan.md

Note

The following content was generated by AI.

PR 1 of 4 of the composition plan, rebuilt on main (alpha.105) from the functional coverage of the stack #505 → #520. A file names the columns and row families it reads and does not build under one closed key given:, with two kinds: variables: (dims, description) and constraints: (dims, description).

• A given name is in the namespace, has a frame for the dimension check, and dual() may name a given row family. A name given and built in one file is refused; the message names the rewrite.
• The file typesets alone: a Given legend group lists both kinds, a given column prints italic like any variable and gets no domain line, a given row family prints under its dual symbol.
• Program.given.variables / .constraints carry GivenDeclaration(dims). Lowering does not refuse. A given column counts as a linking column in Program.separability.
• advice gains the kind given, one note per declaration a consumer must bind. A dimension only a given declaration indexes counts as reached.
• Spec.variable_frames / Spec.constraint_frames are the one home of "built or given" for every lookup.
• sos: and piecewise: activity: still refuse a given column, and the message now says why and names the rewrite.

Decisions to flag

• limits.md gains a fourth kind of construct under How a new construct enters: a declaration of what the file reads. The composition section is swept from templates to fragments.
• Eleven declaration keys. file.md, index.md rule 1 and the Spec docstring say so.
• domain is not a field of a given variable, though the plan's F1 lists it. Nothing in the language read it: lowering dropped it and no consumer could see it. The owner holds domain like bounds and where. Three reviewers found this independently.
• advice's given kind is a note, not a refusal. reading.md tells a consumer with no host to refuse. Both open points from the plan stay as the plan states them.

Departures from the plan

• boundedness.py gained a guard: the unboundedness pass raised KeyError on an objective over a given column named by no constraint. A given column is excluded from that pass, since its bounds are the owner's.
• tests/test_reading_page.py pins the claim count on reading.md; it moved from 12 to 15 for the three executed lines in the new section. The plan said "no test change".
• mkdocs.yml changes: the nav label of the declarations page names given. The plan said "Nav unchanged".
• errors.md's advice-kind table gains the given row; it is the one home of the kind list.

Verified: pixi run ci (lint, 1346 tests, mkdocs build --strict, compile-tex, 30 documents) green on this tree. Schema regenerated with tools.schema and the diff read: three new $defs, the given property, ten → eleven. Golden typesetter output regenerated: no diff. Not run: pixi run test-coverage.

Mutation table: each guard deleted in turn, suite run, guard restored

Guard removed	File	Failures
_names_are_names reaches given:	model.py	2
given constraint also under constraints: refused	model.py	1
given variable joins _name_collisions	model.py	1
given variable frame joins _frame_dimensions	model.py	1
given constraint frame joins _frame_dimensions	model.py	2
given frames count as reached (never-an-axis)	advice.py	1
_given() notes emitted	advice.py	4
boundedness skips a given column	boundedness.py	1
dual refusal names given: constraints:	resolution.py	1
a given column is a linking column	separability.py	1
given variables are chosen (italic)	symbols.py	1
symbol table knows given variables	symbols.py	1
symbol table knows given constraints	symbols.py	1
Glossary('Given', …)	walk.py	2
lowering fills given.variables	lowering.py	7
lowering fills given.constraints	lowering.py	4

The plan flagged the never-an-axis row as green in the stack; it is red here without its guard (test_a_dimension_only_a_given_declaration_indexes_is_in_use).

Review and coverage moves

Four reviewers (correctness, quality, types, tests) read the diff; twelve findings were applied, three declined: renaming GivenTargets, removing __bool__ (PR 2 and 3 call it), and rewording Footprint.domains (true once domain is gone).

Coverage moved: "every advice kind is produced" moved from test_both_kinds_of_note_come_through_the_one_door to test_every_kind_a_consumer_can_pin_against_is_produced_here in tests/test_advice.py, reading across two fixtures.

Not in this PR, by plan: composition.py, merge, override, examples/library, the fixtures.override → varied rename (PR 2), the folding sentences on declarations.md#given (PR 3).

[read-the-docs-community]

Documentation build overview

📚 math-spec | 🛠️ Build #34650858 | 📁 Comparing c88a8a8 against latest (3317ecf)

  🔍 Preview build  

16 files changed · ± 16 modified

± Modified

• about/limits/index.html
• reference/language/index.html
• reference/reading/index.html
• reference/language/declarations/index.html
• reference/language/errors/index.html
• reference/language/file/index.html
• reference/math_spec/advice/index.html
• reference/math_spec/boundedness/index.html
• reference/math_spec/errors/index.html
• reference/math_spec/lowering/index.html
• and 6 more...