Repository navigation
feat(import): add MCIP importer, packet enrichment workflow, and 190-packet backfill #6
Description
Goal
Make enriched Proof Search output the default MathCorpus population path and recover all available evidence for the existing corpus.
Scope
- Add an MCIP bundle importer with dry-run, validation, conflict detection, and resumable batch operation.
- Update
author_packet.pyso it can consume verifier exports rather than requiring most metadata to be manually copied into a batch spec. - Require Proof Search provenance claims to resolve to trajectory and artifact records when policy allows.
- Backfill existing packets from Lean source, packet metadata, and retained Proof Search databases/artifacts.
- Produce a machine-readable loss report for fields that cannot be recovered.
Recoverable targets
- tactics and proof shape
- proof profile
- explicit dependencies
- episode and trajectory linkage
- attempts and diagnostics where retained
- model hashes, tokens, cost, and timing where retained
- proof variants and repair chains where reconstructable
Acceptance criteria
- Import is idempotent and does not mutate canonical packet identity.
- Conflicting evidence is quarantined rather than silently selected.
- Existing 190 packets receive a backfill status report.
- Unrecoverable successful tactic text, observations, rewards, or candidate bodies are explicitly marked missing.
- CI validates imported bundles and regenerated manifests.
- New Proof Search-generated packets use the enriched path by default.
Activity
Mnehmos commentedon Jul 12, 2026
Implemented (local commit
928b2be, stacked oned2e1a7/b3bfa63/bcdb683/8c74201/7f1ac10— not yet pushed, see notes on #1-#5). This one is genuinely different in kind from #2-#5 (a real tool, not a schema embed), so a more detailed accounting than usual:MCIP bundle importer (
tools/import_mcip.py+ sharedtools/mathcorpus/mcip_import.py):proof_variants,dependency_manifest,attempts,negative_examples,repair_trajectories,model_runs,empirical_difficulty_aggregates). Never creates a new packet; never mutates canonical identity fields (packet_id,title,theorem_name,formal_statement_pp,hashes,trust,training, ...) — verified directly by diffing before/after on a real packet.--applyto write. Validation: a structurally invalid bundle (schema or hash failure) is rejected outright, nothing written. Conflict detection: a bundle whose target packet is missing, or whoseformal_statement_sha256disagrees with the target's own, is quarantined whole; within an otherwise-valid bundle, each record conflicting with existing differently-shaped content is quarantined individually — everything else still applies.--quarantine-reportgives a machine-readable list. Resumable: re-running the same bundle is a verified no-op (byte-identical output on re-run, confirmed by test).restriction_profilerecords go to the sharedrestriction_profiles/catalog (same conflict/idempotency semantics), not into a packet.author_packet.pyconsumes verifier exports: new optionalverifier_export_bundlespec field uses the same fold logic, so a freshly authored packet and a backfilled one populate identically. Manual spec fields win on conflict (reported, never silently overwritten) — this is the "new Proof-Search-generated packets use the enriched path by default" criterion.Backfill status report (
tools/backfill_report.py): every packet gets a per-field status across the issue's 7 recoverable-target categories (recovered/not_yet_backfilled/unrecoverable_missing/not_applicable). Run against the current 357-packet corpus, committed asmanifests/backfill_report.json(a point-in-time snapshot, like the othermanifests/*.jsonfiles — not kept in sync per-commit).Honest limitation, stated plainly: this environment has no access to a retained Proof Search trajectory database or artifact store — only what's already in this repo.
attempts_and_diagnosticsandmodel_hashes_tokens_cost_timingareunrecoverable_missingfor ~355 of 357 packets as a direct result, and will stay that way unless a real MCIP export from Proof Search's actual retained data is produced and imported. This is documented explicitly indocs/mcip-import.md, not silently glossed over — the acceptance criterion "unrecoverable fields are explicitly marked missing" is satisfied by being honest about the gap, not by pretending it's smaller than it is."Provenance resolves to trajectory/artifact records when policy allows": implemented as an opt-in
validate_packets.py --artifact-index <path>+policy.check_trajectory_artifact_resolution, off by default since no real artifact index exists yet. This is the mechanism, ready for whichever process eventually has access to Proof Search's real store.CI: gains an importer dry-run step (against the real corpus + MCIP fixtures) and a backfill-report generation step.
Cross-cutting fixes found via this integration work (the kind of thing this issue was supposed to surface): MCIP's
empirical_difficulty_aggregate.schema.jsonwas missingcalibration_version(present on the packet-embedded version since #5) — fixed, fixtures regenerated using the real formula instead of hand-picked values.packet.schema.json'sproof_variantwas missingmodel_run_id(present in MCIP's own version since #1) — fixed. A misleading importer summary message and a real tuple-unpacking bug inauthor_packet.py's new conflict path were both caught by testing and fixed.Extensive smoke-testing: dry-run, apply+validate (0 errors), idempotent re-run (byte-identical), canonical-identity preservation, all 3 bundle-level quarantine paths, restriction-profile conflict,
author_packet.py's manual-field-wins-on-conflict path. Full corpus (357 packets) + full CI-equivalent pipeline verified locally, 0 errors.Tracked in
agents/github_issues/DONE.md,FEATURES.md,HANDOFF.md.feat(schema): define MathCorpus Interchange Protocol v1 (closes #1)
feat(schema): standardize dependency manifests and retrieval evidence (…
feat(import): add MCIP importer, packet enrichment workflow, and back…
feat(schema): add literature-lineage, idea-attribution, and prior-art…
feat(policy): require contribution, citation, and novelty review for …