Tests real assertions - #18
Draft
dingf3ng wants to merge 27 commits into
Draft
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>
219dbad moved three tests onto temp_example_copy() and left "around a dozen others" pointing at the tracked examples/*.v. This finishes that migration. Why it matters: coqpyt writes every accepted change straight back to the file on disk (coqpyt/coq/base_file.py::_make_change), and nothing puts it back -- CoqInterface.load() alone pops the trailing "Admitted." and the file loses its proof terminator permanently. Reproduced against the tracked file: before: 4a0ceb92 tail: 'Proof.\n\nAdmitted.\n' after load: c0a19927 tail: 'Proof.\n' after close: c0a19927 <- close() does not restore git status: M examples/main_loop_invariant_2_established_Coq.v The tests that guarded this with reset/restore were not safe either. A finally: block only runs while the interpreter unwinds: SIGTERM -> finally block: NOT RUN SIGINT -> finally block: FINALLY RAN SIGKILL -> finally block: NOT RUN SIGTERM is what plain `timeout` sends, what `docker stop` sends, and what CI sends on a step timeout -- and these tests drive coq-lsp, so being killed is how they routinely end. `timeout -s TERM 6 python3 tests/test_coqpyt_simple.py` was enough to leave examples/example.v rewritten with an orphan .backup beside it. temp_example_copy() now also copies examples/_CoqProject next to the copy, so tests driving coqpyt's ProofFile directly still resolve the libframac imports; a CoqInterface with auto_setup_coqproject regenerates the same content. Two follow-ons in the same files: test_proof_tree_step_by_step wrote its PNG output into examples/, and test_coqpyt_svcomp_clean printed "file not available" and carried on; both now use the temp directory and a real pytest.skip respectively. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The agent proves in place. clean_proof_file() strips the existing tactics
from the target .v, and coqpyt then writes every accepted tactic straight
back to disk. Pointed at a real file, a run destroys it: the original
proof is gone and the working tree is dirty. A single benchmark run
rewrites every .v in AutoRocq-bench that way, which is why the standing
advice after test_folder_batch has been
`git -C AutoRocq-bench checkout -- benchmarks`.
ScratchProof (utils/scratch.py) hands the agent a throwaway copy instead.
The copy is created beside the original, so the workspace resolves
exactly as before -- same _CoqProject, same sibling modules, same library
paths -- and it is given a module-safe generated name. When the run ends
the finished proof is saved into the run's output directory, where it
stays available for independent re-checking rather than being clobbered
by the next run, and the scratch file and its build artifacts are
removed.
The copy is made in CoqInterface's constructor, so every one of the 19
construction sites gets it and there is no knob to forget. No read-only
mode would justify an opt-out: load() alone pops the trailing
"Admitted.", clear_all_proof_scripts() rewrites the file, and coqpyt
writes every accepted tactic straight to disk, so any CoqInterface built
on a file the caller cares about would damage it. The file you pass IS
the source, so the interface derives the source path rather than taking
one -- the question "when is source_path None?" never arises.
Two things had to move, because they edited the file before a copy
existed and would otherwise have hit the user's own file: the Hammer
import injection, and proof cleaning. Both now run between construction
and load(), on coq_interface.file_path, with clean_success threaded back
through the components dict. Saving became coq_interface.save_result(),
behind a _harvest_proof() helper that the signal handler and the normal
exit both use, so a Ctrl-C still keeps whatever the run had proved.
ProofRecorder.start_proof_recording takes proof_file_path: records are
grouped by file, and a generated scratch name would scatter them.
Scratch cleanup is registered with atexit rather than done in close(),
because load() calls close() to tear down the previous coq-lsp session
and would otherwise delete the file out from under itself.
ScratchProof.close() only unlinks files, so it is safe at interpreter
exit.
.gitignore covers *_autorocq_*.v so a scratch file left behind by a hard
kill cannot be mistaken for a source file.
Verified end to end against a real run (gpt-4.1):
🎉 Proof completed successfully!
examples/example.v a380c035 -> a380c035 (untouched)
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Proving on a scratch copy changes the behaviour the README documents. The
quickstart still promised
"the proof script is saved in the same example.v file"
which was true, and was the reason example.v arrived in the tree already
proven (a4c1e2f committed the output of running that very command). It is
not true any more: the source file is left untouched and the result is
written into the run's output directory.
The rewritten paragraph names where the proof lands and offers --output-dir
for choosing somewhere else. That flag did not exist: main.py read output_dir
from the config file and nothing else, so the sentence documented something
imaginary. Adding it is the smaller fix, and it is the flag a benchmark run
wants -- without it every run drops its output directory next to the .v file,
which for AutoRocq-bench means inside the submodule.
It wins over the config the way every other command line option here already
does, and the directory is created with parents so a path like
/tmp/runs/today/first works.
Checked: --help lists the flag, and setup_output_directory creates a nested
path that does not exist yet.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Both files reported success without checking anything. test_context_search asserted `successful_searches > 0`, where a "success" was any string coming back from coq.search(). It built its interface as CoqInterface(path) with no workspace and no library_paths, so libframac was never mapped, the goal file's statement did not typecheck, no proof was opened, and load() died in coqpyt with "pop from empty list". The return value of load() was discarded and "CoqInterface loaded successfully" printed regardless. Every one of the 15 queries then returned the string "aux_file not accessible" and was counted as a hit: 15/15, 12/12, exit 0, in 12 seconds. Under pytest it was worse -- both functions `return` a bool, which pytest discards, so they were green unconditionally. test_coq_interface_queries had the same construction and the same scoring, reporting 23/23. Both now build the interface from configs/default_config.json and assert load(). Queries are checked by content, never by size: `Search Z.abs` must contain "Z.abs_0", `Locate mult` must contain "Corelib.Init.Peano.mult", `Check (fun x => x + 1)` must contain "fun x : int => x + 1". Sizes and exact text drift with the Rocq version and with which notations are in scope, so only substrings are asserted. The three searches too large to pin that way assert a size floor instead. One assertion is load-bearing: `Search Z.abs` must contain "Abs.Abs_pos", which lives in libautorocq/int/Abs.v. It fails if the libframac mapping is not actually on the load path, which is the defect that made the file vacuous in the first place. test_context_search additionally splits what it was only claiming to test. Ranking and size reduction are driven directly against ResultReducer with synthetic input, because which band a live query lands in is decided purely by len(content) and real output sits close to the boundaries -- `Search to_sint32` is 503 characters against a 500-char threshold. Three characters of library drift would silently drop that coverage with nothing failing. Driving the reducer directly pins all four bands, both sides of 500/501 and 1000/1001, and the goal-context ranking. Verified by mutation: removing the workspace fails 3 tests with "pop from empty list"; changing an expected fragment fails with the real output printed; changing an expected reduction band fails naming both. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
CoqInterface.search() is the implementation behind every Search, Print, Locate, About, Check and Print Assumptions query. It always returned a str, and encoded its failures as ordinary text: "aux_file not accessible", "Query error: ...", "Empty query", "No search term provided", "Error executing print: ...", "Unsupported query type: ...". _extract_search_results went further and swallowed its exception entirely, returning whatever partial list it had collected -- usually [] -- as if the search had completed. Nothing downstream could tell "found nothing" from "broke". CoqCommandSearch._create_search_result scores a result 1.0 unless its text contains the literal phrase "No results found", so a dead aux_file or an LSP error mid-extraction reached the LLM as a confident, high relevance search hit whose content was an error message. The agent then reasoned over it. search() and _run_aux_query() now return Optional[str]: the output on success, None on failure, with the reason on self.last_error and read back through get_last_error(). That is the signal the class already uses for apply_tactic and reset_by_step, so this adds no new convention. A query that legitimately matches nothing is a success, not a failure, and still returns "No results found.". Keeping those apart in the Search path takes some care, because _extract_search_results is called in a polling loop and has to keep returning its partial list so the retry still works. It now records the exception on last_error instead of dropping it, and the Search branch clears last_error before polling, then distinguishes: results found -> return them; empty with an error recorded -> None; empty with no error -> "No results found.". skip_prefixes is deliberately untouched. It filters proof-goal noise out of legitimate hits, including lines Rocq itself emits starting with "Error:", and is a separate, more ambiguous question. The None case is handled in _create_search_result rather than at each of the eight CoqCommandSearch call sites, since all eight funnel through it. A failed query becomes relevance 0.0 with metadata['failed'] set and content "Query failed: <reason>" -- interactive_session prints that content, so the reason still reaches a human. tests/test_search_failures.py covers the contract without Rocq: an extraction failure returns None with the cause on last_error, a genuinely empty search still returns "No results found." with last_error unset, every malformed-query path returns None with the right reason, and all eight CoqCommandSearch methods score a failure 0.0 while a success stays 1.0. Runs in 2 seconds. The two live test files are adapted to the new contract, and test_coq_interface_queries gains the failure half: an unsupported command returns None naming the command, and the session still answers afterwards. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Its three tests take a `config` argument, supplied by the __main__ block
at the bottom. Under pytest there is no fixture by that name, so all
three error at setup before any test body runs:
E fixture 'config' not found
Adds the fixture. It skips rather than fails when no API key is
configured, because these tests call a live LLM -- an unconfigured
checkout should not go red, and CI should not spend money by default.
with a key: 3 passed
without a key: 3 skipped
__main__ passes config explicitly and is unaffected either way.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Three tests passed enable_context_search= to ProofController, which does
not take it -- the flag belongs to ContextManager, which is where main.py
passes it. ProofController takes max_context_search, a different knob.
Every one of them died at construction:
TypeError: ProofController.__init__() got an unexpected keyword
argument 'enable_context_search'
test_folder_batch is the batch runner over AutoRocq-bench, so it could
not prove a single file. test_controller_prove hid it: the exception is
caught, the function returns False, and pytest discards the return, so it
reported a pass while proving nothing.
Moving the flag to the ContextManager call, matching main.py, is enough.
Driving the batch runner over the first five svcomp goals afterwards:
True 16s array_1-2/main_assert_reachability.v
True 59s array_1-2/main_loop_invariant_2_preserved.v
False 80s base_case/main_assert_reachability.v
False 60s benchmark02_linear/..._inv_i_bounds_established.v
True 11s benchmark02_linear/..._inv_i_bounds_preserved.v
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
ProofController wrote <theorem>_proof_tree_final.png/.json next to the file being proved. The problem is the directory, not the files: the tree is a run artifact, and every other run artifact -- autorocq.log, the resulting .v -- already goes to the output directory main.py builds for the run. Writing it into the source tree left two untracked files per goal in AutoRocq-bench, which is a submodule; only proof-search/examples has *.png and *.json gitignored, so nothing covered them there. _finish_proof now writes the tree into that output directory instead, so it is kept rather than deleted: it lands beside the log and the proof it describes, where the next run cannot overwrite it. main() records the resolved directory on the config, the way it already does for config.log_file, so initialize_components can pass it down. A None default keeps the old behaviour for callers that have no run directory; each test that builds a controller now passes the directory its own run already owns. Checked by driving _finish_proof both ways on a temporary tree: with an output directory both files land there and the source directory stays empty; with None they fall back beside the .v as before. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
test_coq_interface.py, test_state_manager.py and test_tactic_history.py kept all of their code under `if __name__ == "__main__":`, so pytest collected zero tests from each and nothing in them was ever checked by a test run. Rewritten as collected tests with assertions. Three things surfaced: - test_coq_interface.py's tactics had gone stale, introducing two nat variables for a lemma that binds a single bool. - test_state_manager.py passed the raw string from get_hypothesis() where ProofState annotates List[str], which made copy() explode the state into one entry per character. It now passes the lines. - test_tactic_history.py began by unlinking proof-search/data/tactic_history.json, the agent's own accumulated history. Everything now writes under tmp_path. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Every test here ended in `return True` / `return False` with no assertions, usually inside a blanket `except Exception` that printed a traceback and returned False. pytest ignores a test's return value -- it only warns -- so all of these passed whether the code worked, did nothing, or raised. Verified before the rewrite: the eight collected bool-returning tests all returned True, so this is missing enforcement rather than hidden breakage. Four defects the new assertions turned up: - ProofController has no `step_count`; test_controller_prove.py and test_svcomp_llm.py both printed it, and the AttributeError was swallowed by their `except Exception` and reported as a pass. It is `gen_step_count`. - `if not proof_file.current_goals:` can never fire. current_goals is a GoalAnswer that stays truthy once the last goal closes, and str() of it is "No more goals." rather than "". Every "is it finished yet" check now goes through current_goals.goals.goals. - CoqInterface.get_hypothesis() always returns "". get_raw_hypothesis() reads `hypotheses`/`context` off a coqpyt Step, which carries neither, so it falls through to "". Everything the agent stores as hypotheses_before/_after is that empty string. Recorded in test_subgoals.py, not fixed here. - is_proof_complete() flips back to False the moment Qed lands, because it reads unproven_proofs and a closed proof leaves that list. Recorded in test_coq_interface.py and test_svcomp.py. Two tests no longer need Rocq at all: extract_essential_proof_content is pure text processing reached through a ContextManager, and get_similar_history was run against gitignored local history that does not exist on a fresh checkout. Both now run in milliseconds against fixtures they build themselves. The live tests share one module-scoped session, pass use_disk_cache like CoqInterface does, and no longer rewrite the goal file before loading it -- that only changed the content coqpyt's disk cache is keyed on and forced a cold re-elaboration. The suite drops from 7m48s to 2m32s. The LLM-marked tests assert the controller's contract -- the verdict agrees with is_successful, the step budget holds, the bookkeeping matches the script, the run artifacts are written -- rather than that a non-deterministic model succeeds. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
test_coqpyt_svcomp_clean.py needs examples/main_loop_invariant_2_established_Coq_clean.v, which has never existed in this repo -- `git log --all` finds no commit that added it. The file skipped at import on every run since it was written, so it has never checked anything. Its content is the same twelve-tactic proof against the same goal as test_coqpyt_svcomp.py, so nothing is lost: that file now asserts every step is accepted and the proof closes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
SearchResult.relevance_score was never a ranking. Every one of its ten construction sites set 1.0 or 0.0: 1.0 when the reduced content was non-empty and did not contain the literal "No results found", 0.0 everywhere else. The actual ranking of search entries is a separate integer score inside ResultReducer._rank_entries and never touched it. Nothing read the field. The two consumers decide hit from miss on other signals -- context_manager._execute_context_search on result_size, and interactive_session._do_search on content -- so the score reached no prompt, no log and no decision. metadata['failed'] was in the same position: written on the failure path, read by no one. Both are removed. A failed query is still told apart from an empty one the way the malformed-query branches already did it: content reads "Query failed: <reason>" and metadata carries 'error'. That is one convention for reporting a failed search instead of two. The three test files that asserted the score now assert what actually reaches the LLM -- content, result_size and metadata['error'] -- which is the contract worth protecting. Two tests are renamed off the old vocabulary: test_a_search_with_no_hits_reports_no_results and test_a_search_that_matches_nothing_reports_no_results. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
get_proof_completion_status() built its dict by calling is_proof_complete() and then is_ready_for_qed(), and is_ready_for_qed() answered "is this proof ready to close?" by appending Qed and keeping it. So asking for status closed the proof, and the two flags the callers read were measured either side of that write: is_complete saw the proof still open, qed_already_applied saw the terminator that the line above had just added. proof_controller required both to be true, which they only ever were during the single call that did the appending. Reordering those two dict keys -- alphabetizing them -- would have stopped any run from being recorded as successful, silently. The status function also asserted that qed_already_applied == ready_for_qed inside its own try block, so a broken invariant did not raise: the generic handler caught the AssertionError and returned the all-False dict, reporting "there is no proof here" for a proof that had just been finished. is_ready_for_qed() is now a pure predicate: terminator already present, or no goals left and none given up. The append-and-keep-or-pop body it used to carry is apply_qed(), which the two callers that wanted the proof closed -- proof_controller and interactive_session -- now call explicitly once the status says ready. get_proof_completion_status() only reports, so calling it twice gives the same answer, and it no longer asserts. That leaves is_proof_complete(), which read get_unproven_proof() and so went False the instant Qed landed, since coqpyt drops a closed proof out of unproven_proofs. It now resolves the proof through _current_proof() -- the open one, else self.proof, which is the object the Qed was appended to -- and returns True whenever the last step is a terminator. Completion is therefore true after completion. main.py's backup cleaner picks its branch off that flag and had been taking the unproven-steps path on an already-proved file. Three tests recorded the old behaviour with a note to drop them if it ever changed, so they are flipped: test_coq_interface and test_direct_tactics now assert that status leaves the proof alone (and is idempotent), that apply_qed closes it, and that completion survives; test_svcomp asserts is_proof_complete on the closed proof it was asserting the negation of. Full suite: 81 passed, 7 skipped. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Two gaps in the completion fix. A Qed that Rocq refuses. is_ready_for_qed() is now a prediction -- no goals left -- and Rocq can still reject the terminator on a goal-free proof, over unresolved evars or a guard condition it cannot check. apply_qed() already handled that: the append raises, the step is popped back out if one landed, and it returns False. But both callers threw that answer away and re-read the status, so the code read as though closing always worked. They now only re-read when the Qed was actually kept; on a refusal the status they already have still describes the proof, and proof_complete stays False because it needs qed_already_applied. tests/test_coq_interface covers it by making append_step raise: the proof comes back byte-identical and nothing reports a finished proof. A file with more than one proof. _current_proof() asked get_unproven_proof() first, which returns unproven_proofs[0] -- not necessarily the proof this interface is driving. Close the agent's proof in a file where another is still open and that lookup hands back the other one, so qed_already_applied reads False on a proof that just closed. self.proof is the object apply_tactic and apply_qed append to, so it is what the question is about; the unproven lookup is now the fallback for when nothing has been pinned yet. load() and restart_coq_server() set it, close() clears it. apply_qed() also appended to self.proof while testing len(proof.steps) from _current_proof(). Same object today, different ones the moment those two disagree, so it now uses the proof it resolved throughout. The rest of the interface still assumes one proof per file -- twelve call sites reach for get_unproven_proof() directly, and load() takes "the first admitted proof (there should be one)". This makes the completion path consistent, not the whole class. Full suite: 82 passed, 7 skipped. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
apply_qed()'s failure path caught the refusal with a bare `except Exception:`
and dropped it: the proof was restored correctly but the reason went nowhere,
so a run that ended on an unsaveable proof had "not complete" and no cause
anywhere. It now records "Qed refused: <reason>" on last_error, the same
channel apply_tactic uses, and logs it.
tests/test_proof_completion.py covers the contract the previous two commits
established, nine tests against a real coq-lsp session:
- asking for status leaves the proof alone and gives the same answer three
times running -- the regression itself, since status used to append Qed
- is_ready_for_qed() predicts without acting; apply_qed() adds exactly one
step
- completion survives Qed, and stays stable, at the exact moment coqpyt
empties unproven_proofs
- applying Qed twice keeps one terminator
- the three flags are the same whichever order they are computed in, which
is what the old dict quietly depended on
- a refused Qed leaves the proof byte-identical, returns False, and puts the
reason on last_error
- the conjunction proof_controller reads is false before any tactic, false
with the goals closed but unsaved, true only once the proof is saved
- get_proof_status() reports a proved file complete -- the flag main.py picks
its cleanup branch off
- closing one proof in a file that still has an admitted second one, where
unproven_proofs is never empty and a lookup-based answer describes the
wrong proof
They have teeth: against the pre-fix resolution six of the nine fail, and the
multi-proof one fails on the intermediate version too. The refused-Qed test
moves here out of test_coq_interface, where it was a visitor.
Full suite: 90 passed, 7 skipped.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…cture Three of the recorded defects, all of them in how the proof state is read. get_hypothesis() never returned anything. get_raw_hypothesis() looked for `hypotheses` or `context` on proof.steps[-1], and a coqpyt Step carries only text/short_text/ast/diagnostics, so both hasattr branches missed and it fell through to "". Every hypotheses_before and hypotheses_after in the tactic history and the proof tree was that empty string, and the prompt sent after each tactic read "Hypotheses: None" for proof states with a full context. The context lives on the goals: it now renders the focused goal's hyps, one "names : type" line each, with the backgrounded goals left to get_subgoals(). `if not proof_file.current_goals:` could never fire. current_goals is a GoalAnswer and stays truthy after the last goal closes -- str() of it is the sentence "No more goals." -- so the guard in get_subgoals() only ever caught a failed lookup. It says `is None` now, which is what it meant, and the real question has a home: has_open_goals() counts current_goals.goals.goals plus the backgrounded stack. _no_goals_left() asks it first and keeps the string matching as the fallback for when the structure is not available, so completion no longer rests on scraping a sentence. ProofController.step_count did not exist; the counter was gen_step_count. Both LLM tests printed the name that did not exist and test_proof_tree_step_by_step still assigns it. The AttributeError was swallowed by tests that returned bools. One name now: step_count, renamed at all eleven sites. Tests, all showing the behaviour rather than the absence of it: the rendered context matches the focused goal's hyps name for name and type for type and stays distinct from the conclusion; a GoalAnswer with nothing left is asserted truthy next to has_open_goals() returning False, with destruct's two goals in between; step_count exists, starts at zero, and gen_step_count is gone. Full suite: 93 passed, 7 skipped. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The two dead signals in ResultReducer._rank_entries. The standard-library
bonus lowercased the module and then tested it against ['Z', 'Nat', 'List',
'Bool', 'Arith'], so it could never match. The novelty decay counted
retrievals under hash(frozenset(entry.items())) in _structured_summarization
and looked them up under md5(name) in _rank_entries, two key spaces that never
meet, so hit_count was always 0, -2 ** (hit_count - 1) never subtracted
anything, and every search handed back the same top ten -- the agent could
spend its whole query budget re-reading lemmas it had already rejected. Both
now use the entry name, lowercased once, and the local `import hashlib` goes
with them.
Neither signal was reachable from the agent anyway: ranking needs a goal to
score against and _execute_context_search called search(query) without one, so
a summarized result was whatever order Rocq printed. It passes the current
goal now.
Which is the same method as defect 7. Its `except Exception` returned a bare
string where the caller unpacks a pair, so the one path meant to report an
error was the one path that could not -- it would have died on "too many
values to unpack". That handler is gone rather than corrected: ContextSearch.
search() already catches everything and returns a SearchResult whose content
says what went wrong and whose metadata carries 'error', so this was a second
layer inventing its own error text over a first layer that had already done
the work. Worse, it flattened a failed query into "No results found.", telling
the model the opposite of what happened. The reason reaches the model now, and
a genuinely empty result is reported as empty instead of as a hit.
The audit of every `except` in the project (excluding vendored coqpyt) turned
up three more worth changing:
- context_manager.get_action() validated the tool-call thread with five
asserts inside `except AssertionError`. Validation written as a crash and
then caught, which `python -O` removes outright along with the fallback it
guards. It is _tool_role_problem() now, returning the reason as a string.
- coq_interface.get_proof_status() and ensure_admitted() each returned a
plausible value from a handler that logged nothing; ensure_admitted also
left last_error untouched. Both report now.
- context_search.execute_coq_query() built an error SearchResult without
logging it, and main.py's cleanup used a bare `except:`, which swallows
KeyboardInterrupt during a long run.
Left alone deliberately: the seven handlers in utils/coq_utils.py, which are
pure-text helpers falling back to a default; utils/scratch.py's close(), which
is best-effort teardown; and interactive_session's readline setup, where the
feature is optional. tests/test_error_handling.py records the -O behaviour that
motivated the first of these.
Full suite: 106 passed, 7 skipped.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The docstring said a coqpyt Step carries only text/short_text/ast/diagnostics, so neither hasattr branch was ever taken. That is true of Step and wrong about what is in a proof: ProofTerm.steps holds ProofStep, which has no `hypotheses` but does have `context` -- a List[Term] of the definitions and notations that step referenced. The second branch was taken. It returned "" when that list was empty, which is what this goal file gives and what put "Hypotheses: None" in every prompt, and a rendering of unrelated Terms when it was not: on examples/example.v after `reflexivity`, "Class Reflexive (R : A -> A -> Prop) := reflexivity : forall x : A, R x x." would have been handed to the model as the proof context. The fix is unchanged -- hypotheses are on the goals, never on a step -- but the defect was worse than recorded: not always empty, sometimes confidently wrong. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
format_hypotheses() rendered names and type only, so `set (y := true)` reached the model as "y : bool" -- the type of a value it then had no way to recover. coqpyt keeps the body on Hyp.definition (and leaves it out of its own repr, as does str(Goal)), so it has to be put back: "y := true : bool", the way Rocq prints it. tests/test_coq_interface pins both shapes off one proof state: an intro'd hypothesis stays "b : bool" and the let-bound one carries its body. Full suite: 107 passed, 7 skipped. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
61 lines describing a per-step snapshot -- goal, hypotheses, applied tactics, a reward field for "MCTS/search", a parent pointer for rollback -- with no caller anywhere in the agent outside its own copy(). The proof tree the agent actually builds is ProofTreeNode, which carries the same state as strings and is wired into ProofController. tests/test_state_manager.py goes with it. It was the only thing exercising the class, which meant it pinned the contract of code nothing ran: it asserted that hypotheses go in as a list of lines because copy() does list(self.hypothesis), which turns a string into one entry per character. A real defect in code that could not be reached. Full suite: 103 passed, 7 skipped. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
This reverts commit b1bc029.
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.
No description provided.