Repository navigation
feat(schema): standardize dependency manifests and retrieval evidence #3
Description
Problem
The current packet dependencies object is too shallow and author_packet.py does not reliably populate actual theorem dependencies from Proof Search. Retrieval candidates, unused retrieved lemmas, obligation dependencies, transitive depth, and verified module-item dependencies are lost.
Scope
Add a versioned DependencyManifest child record with:
- declared theorem dependencies
- actually used theorem dependencies
- Proof Search obligation dependencies
- verified module-item dependencies
- transitive dependency count and depth
- retrieval candidates
- retrieved-but-unused candidates
- kits, tactic tags, and prerequisite concepts
- source of each dependency claim
Acceptance criteria
- Kernel-verified formal packets generated through Proof Search must reference a dependency manifest.
- Actual dependency evidence is imported from verifier-backed records, not manually guessed.
- Declared, retrieved, and used dependencies remain distinct.
- Dependency identifiers can resolve to Mathlib declarations, MathCorpus packets, or Proof Search verified artifacts.
- Validation catches dangling, cyclic, or environment-mismatched references.
- Corpus manifests can aggregate dependency frequency and depth.
Activity
Mnehmos commentedon Jul 12, 2026
Implemented (local commit
bcdb683, stacked on8c74201/7f1ac10— not yet pushed, see notes on #1/#2):packet.schema.jsongainsdependency_manifest($defs.dependency_manifest/dependency_claim_source), mirroring MCIP'sDependencyManifestfrom feat(schema): define MathCorpus Interchange Protocol v1 for Proof Search enrichment #1. Six distinct categories —declared,used,obligation,verified_module_item,retrieval_candidate,retrieved_unused— instead of one merged list, plus per-claim source attribution (manual/proof_search_import/verifier_export).policy.check_dependency_manifestrejects a dependency claimed bothusedandretrieved_unused(direct contradiction), anenvironment_hashmismatch against the packet's ownverification.environment_hash, and anyclaim_sourcesentry not actually present in the array itscategorynames.policy.check_dependency_manifest_refsresolves any dependency id shaped like a MathCorpuspacket_idagainst the loaded corpus (Mathlib declaration names aren't resolvable this way — no local Mathlib index) and detects cycles through other packets' manifests, deduplicated by edge-set so the same cycle isn't reported once per rotation.tools/build_manifests.py'sdependency_graph.jsongains adependency_manifest_summary— frequency per dependency id per category, plus min/max/avg transitive depth.author_packet.pyfixed: it was silently droppingtheorem_depsfrom spec input entirely (exactly the issue's own complaint) — now populated. Added optionaldependency_manifestspec support so new Proof-Search-authored packets can carry this from the start..leanproof bodies (not fabricated).One deliberate scope note: the acceptance criterion "kernel-verified Proof-Search packets must reference a dependency manifest" is not implemented as a hard
validate_packets.pygate yet. Making it one today would fail all ~350 packets authored before this field existed, breaking CI for the whole corpus on an unrelated PR. It's deferred to the #6 corpus-wide backfill (when it becomes safe to enforce universally) and documented explicitly inschema/ENUMS.mdso it isn't silently dropped from the roadmap.Tracked in
agents/github_issues/DONE.md,FEATURES.md,HANDOFF.md.feat(schema): standardize dependency manifests and retrieval evidence (…
feat(metrics): add multi-model empirical difficulty and native analyt…