Repository navigation
Phase 5: canonical pedagogy records and Pilot A curriculum path #48
Description
Context
MathOS 1.0 requires canonical pedagogy before release/export projections. RecordKind::LearningUnit and typed pedagogy edges already exist, but learning_unit/1 currently bypasses validation and neither CLI nor MCP exposes the SPEC §21.8 pedagogy actions.
This issue is intentionally limited to the Phase 5 canonical pedagogy layer and Pilot A learning path. Release bundles and RL-task export remain a separate follow-up slice.
Scope
- Define a closed, bounded Rust-owned
learning_unit/1payload and committed JSON Schema for the SPEC learning-unit kinds. - Validate exact target, source, formalization, content-artifact, license, review, and training-policy data through the shared application path.
- Expose one first-class
mcl pedagogyfamily and one MCPpedagogytool family for propose, version, get, validate, review, link, and path operations. - Reuse immutable records and exact version-bound pedagogy edges; preserve the existing hard-prerequisite cycle rejection.
- Build and playtest a deterministic Pilot A path containing explanation, counterexample, misconception, exercise, and mastery check units grounded in canonical claim/evidence artifacts.
Acceptance criteria
-
learning_unit/1denies unknown fields, enforces bounded text/collections and closed enums, and has a committed schema equality test. - Every unit names exactly one claim or concept target, an audience track, entry assumptions, objectives, hard/soft prerequisites, grounded source/formal references, one content artifact, review state, license, and training status.
- Application validation resolves every exact canonical reference and content artifact; stale/missing/wrong-kind references fail closed.
- Public/training eligibility fails closed when license, review, redistribution, or artifact restrictions do not permit it; pedagogy review never grants mathematical authority.
-
propose,version,get,validate,review,link, and deterministic boundedpathuse the same application methods from CLI and MCP. - Links accept only pedagogy edge kinds and exact learning-unit versions where required; hard and soft prerequisites remain distinct; hard cycles are rejected.
- Dry-run, idempotency, compare-and-swap, restart persistence, CLI/MCP parity, malformed input, stale reference, cycle, and training-policy tests pass.
- Pilot A CLI playtest creates and traverses explanation, counterexample, misconception, exercise, and mastery-check units against real canonical Pilot A state.
- Implementation status/checklist documentation records exact tested capability and explicitly leaves release/RL export open.
Verification
cargo fmt --checkcargo clippy --workspace --all-targets --all-features -- -D warningscargo test --workspacePYTHONPATH=src PYTHONWARNINGS=error::ResourceWarning python -m unittest discover -s tests -v- focused CLI/MCP playtest from a fresh root and after restart
git diff --check
Activity
Mnehmos commentedon Jul 21, 2026
Implementation checkpoint on
issue-48-canonical-pedagogy:learning_unit/1contract and committedschemas/pedagogy/learning-unit-1.schema.jsonfor all 13 SPEC unit kinds and every §18.2 field.propose,version,get,validate,review,link, andpathapplication methods. MCP action fields are closed and retain a root object schema.Focused playtest evidence:
Local Windows verification so far:
cargo fmt --check— passcargo test --workspace— 141 unit + 1 Lean + 4 MCP + 13 CLI tests passedmcl doctor— healthy with Lean 4.32.0git diff --check— passRelease bundles and RL/evaluation exports remain explicitly out of scope and unfinished.
Mnehmos commentedon Jul 21, 2026
Final merged-tree evidence for #48:
d85be145666188dfce8c4999015e128a713d7e4bas merge commit6764ac2dc832e6eab0a984be5ccd252a214c5321(tree526159961fd1e22b817f16672d375e115315512c).29875685174passed Linux Rust, Windows Rust, pinned Lean, real-storage smoke, and legacy Python on that exact head; CodeRabbit was green.d85be14added receipt-first preflight for learning-unit propose/version/review and pedagogy links, plus CLI regressions that advance dependency heads and prove exact retries still return their original stored result. The review thread was answered and resolved; zero unresolved threads remained at merge.29875909954passed all five jobs on exact merge6764ac2.29875910000passed and retained artifactpublication-boundary-6764ac2dc832e6eab0a984be5ccd252a214c5321(artifact ID8512988490, 226,131 bytes).not_started -> open -> proved, original claim stilldisproved, and byte-identical original claim/status/counterexample-package/repair-edge state. Proof requestf6511ab5def57f0da240894d96bb92862d6e30d8893e6f0874179220c7504d73, report536bb0a6ab1a035d2c50ac3e8d7a659f641e0d2bbf4139865aa2308fe97330ad, closurebb9b103cff4f92620aafb2252a1e208974222130cd33e25de247c37516f178fa.explanation -> counterexample/misconception -> exercise -> mastery_checkagainst exact Pilot A source019f868e-463d-7103-9cc3-222213939c55@59ef27897c032cab17d1c371f509ab05898a65bef03376e5deb33d18822c8c40, repaired claim019f868e-464e-78e0-9125-035f7fba0e87@288e4ee259fb2f7cb5fd5295c971fec10ee85415601d6ea13d7d09d3103a6ddc, and Lean formalization019f868e-4662-7bc0-ba7b-b1b6d1214e05@527785065de148fc1ba15f4001afcce41a1e4bf10d0fee33c3de157df8b7afc5; claim status stayed unchanged andmcl doctorremained healthy.The protected artifact contains zero pedagogy/learning-unit files. That is expected for this canonical Phase 5 slice and is direct evidence that portable release, MathCorpus/MCIP, and RL/evaluation projections remain unfinished Phase 6 work; #48 does not claim those capabilities.