Fix failing test suite: restore sorry placeholders in example problems#28
Merged
Conversation
PR #27 added tests/test_operational.py, which requires the example problem files to contain unsolved 'sorry' placeholders, but the same PR committed those files with completed proofs (solver output leaked into the working tree). The suite has failed on main ever since: - test_original_content_is_preloaded: expects 'sorry' in every manifest problem - test_intermediate_has_sorry_placeholders: expects >=5 sorries in examples/intermediate.lean Restore test_theorem.lean, basic_algebra.lean, and number_theory.lean to their pre-#27 unsolved versions, and replace the proof bodies in intermediate.lean with sorry while keeping its theorem statements. Solved files also defeat the project's purpose: problems must ship unsolved for the Prover/Critic loop to have anything to prove. Result: 314 passed, 9 skipped (was 14 failed, 300 passed, 9 skipped). https://claude.ai/code/session_01KAKnLjpFZ9oF74GNW9QNtN
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Restores the unsolved (
sorry-placeholder) versions of the four example problem files inexamples/. The test suite onmaincurrently fails with 14 failed / 300 passed; with this change it's 314 passed, 9 skipped.Why
PR #27 added
tests/test_operational.py, which asserts that example problem files containsorryplaceholders (test_original_content_is_preloaded,test_intermediate_has_sorry_placeholders). But the same PR committed the example files with completed proofs — solver output evidently leaked into the working tree before commit. The tests it added have been failing ever since.Solved example files also defeat the project's premise: problems must ship unsolved for the Prover/Critic loop (and the README's mock-mode demo) to have anything to prove.
Changes
examples/test_theorem.lean,examples/basic_algebra.lean,examples/number_theory.lean: restored verbatim to their pre-Fix critical bugs and add comprehensive test suite for Erdos proof system #27 versions (from commit970c3a8).examples/intermediate.lean: this file was introduced by Fix critical bugs and add comprehensive test suite for Erdos proof system #27 already solved, so there's no prior version — its six theorem statements are kept and each proof body replaced withsorry(6 ≥ the 5 the test requires).Verification
python -m pytest tests/ -q→ 314 passed, 9 skipped (the 9 skips are environment-gated and unchanged from before).solution_<id>.json+ ZIP), never back intoexamples/, so the current code won't re-introduce this.Notes for the maintainer
TestGeminiProvider, provider factory) were a brokencffiwheel in my container, not a code issue —google-generativeaiimports fine after reinstallingcffi, and CI installs it cleanly via pyproject deps..github/workflows/ci.ymlbeing configured for pushes/PRs tomainand the README sporting a CI badge. That's why this breakage went unnoticed. Worth checking Settings → Actions to confirm Actions is enabled — once it is, this PR should get a CI run.https://claude.ai/code/session_01KAKnLjpFZ9oF74GNW9QNtN
Generated by Claude Code