Skip to content

docs: sync live generated theorem path count to thirteen - #109

Merged
AkiraTamai merged 1 commit into
developfrom
devin/1785652847-docs-sync-live-paths
Aug 4, 2026
Merged

docs: sync live generated theorem path count to thirteen#109
AkiraTamai merged 1 commit into
developfrom
devin/1785652847-docs-sync-live-paths

Conversation

@AkiraTamai

Copy link
Copy Markdown
Contributor

Summary

docs-sync only. docs/ROADMAP.md, docs/ARCHITECTURE.md and docs/LEAN_TRANSLATOR_SPEC.md already describe thirteen live generated theorem paths (through predicate_guard_collapse), but docs/LEAN_HARNESS_CONTRACT.md and .agents/skills/testing-mumei-lean-live-generated/SKILL.md still said eleven and stopped at ff_mul_associative. The implementation (tests/test_lean_bridge_e2e.py + the 13 tests/fixtures/*.proof-cert.json live paths) is the single source of truth, so the docs are moved to match it:

  • docs/LEAN_HARNESS_CONTRACT.md: eleven → thirteen, plus per-path entries for ff_mul_add_distributive (12th, tactic search adopts mumei_ff_mod, Generated.Std.Algebra.Finite_field.ff_mul_add_distributive_correct) and predicate_guard_collapse (13th, widened ladder adopts tauto, Generated.Std.Core_predicates.predicate_guard_collapse_correct). Both are tactic-only adoptions, so bridge_lemma_hash is unchanged.
  • .agents/skills/.../SKILL.md: heading (11 total)(13 total) and list items 12/13.
  • docs/CHANGELOG.md: new entry recording the two previously unlogged paths and the count sync.

No code, no vocabulary, and no contract constants change: translator_version = mumei-lean-translator-ir-v2 and bridge_lemma_hash = ee8cd3ba…4347 still match scripts/export_cert.py / scripts/expr_translator.py.

Regression commands

# mumei-lean
PYTHONPATH=scripts MUMEI_LEAN_SKIP_LIVE=1 python -m pytest tests/test_contract_vocabulary.py -q   # 6 passed
PYTHONPATH=scripts MUMEI_LEAN_SKIP_LIVE=1 python -m pytest -q                                    # 306 passed, 11 skipped

# cross-repo docs-sync gates (unchanged, run green on develop)
# mumei:       python3 scripts/check_contract_vocabulary.py
# mumei-agent: uv run pytest tests/test_contract_vocabulary.py -q

Link to Devin session: https://app.devin.ai/sessions/adfa18cdf78948c09b218b54aa5a83b0
Requested by: @AkiraTamai

Co-Authored-By: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com>
@AkiraTamai AkiraTamai self-assigned this Aug 2, 2026
@devin-ai-integration

Copy link
Copy Markdown
Contributor

🤖 Devin AI Engineer

I'll be helping with this pull request! Here's what you should know:

✅ I will automatically:

  • Address comments on this PR. Add '(aside)' to your comment to have me ignore it.
  • Look at CI failures and help fix them

Note: I can only respond to comments from users who have write access to this repository.

⚙️ Control Options:

  • Disable automatic comment, CI, and merge conflict monitoring

@devin-ai-integration devin-ai-integration Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

✅ Devin Review: No Issues Found

Devin Review analyzed this PR and found no potential bugs to report.

View in Devin Review to see 1 additional finding.

Open in Devin Review

@AkiraTamai
AkiraTamai merged commit ff2dcc7 into develop Aug 4, 2026
7 checks passed
@AkiraTamai
AkiraTamai deleted the devin/1785652847-docs-sync-live-paths branch August 4, 2026 06:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant