examples: restore example.v to its unproven state - #12
Open
dingf3ng wants to merge 1 commit into
Open
Conversation
example.v ships as the README's quickstart target:
python3 -m main examples/example.v --config ./configs/minimal.json
and the README says, correctly, that "the proof script is saved in the
same example.v file". a4c1e2f ("update readme") ran that command while
writing those instructions, and committed the resulting file: the lemma
arrived proven, with the exact tactic body the agent had just found.
That breaks the quickstart it was documenting. With no unproven proof in
the file, get_unproven_proof() returns None, load() logs "No unproven
proof found in file" and returns False, and main.py:219 turns that into
`raise Exception("Failed to load Coq file")` -- after logging the empty
last_error as the reason. A new clone cannot run the first command in
the README.
Restores the Proof./Admitted. body the file had at dab2b56. Nothing in
the tree depends on it being proven: test_coqpyt.py and
test_coqpyt_simple.py reset it themselves, and run_tests.py resets it
before the suite.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
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
1 participant
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.
Why
examples/example.vis the README's quickstart target:The README also says, correctly, that "the proof script is saved in the same
example.vfile".Commit
a4c1e2f("update readme") ran that command while writing those instructions — and committed the result. The lemma arrived already proven, carrying the exact tactic body the agent had just found.The consequence
That breaks the quickstart it was documenting. With no unproven proof left in the file:
main.py:219turns thatFalseintoraise Exception("Failed to load Coq file")— after logging the emptylast_erroras the reason. A fresh clone cannot run the first command in the README.What changed
One file. Restores the
Proof./Admitted.body it had atdab2b56.Is anything depending on it being proven?
No — checked all consumers.
test_coqpyt.pyandtest_coqpyt_simple.pyreset it themselves, andrun_tests.pyresets it before the suite.