Conversation
WrappedProverRunner.run is the ProverRunner a plugin gets through CVLAuthorState. setup_prover_config_in requires exclude_rule, so every plugin prover call raised a TypeError before anything was staged. The runner and the ProverRunner protocol now take exclude_rules next to rules, the way verify_spec scopes its own runs, and a unit test drives the runner against a mocked run_prover. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01CMrKc9bciyU9yKag4wH4Ev
jtoman
approved these changes
Sep 16, 2026
| callbacks: ProverCallbacks, | ||
| tool_call_id: str, | ||
| rules: list[str] | None = None, | ||
| exclude_rules: list[str] | None = None, |
Contributor
There was a problem hiding this comment.
I was going to ask why the typechecker didn't help us here. Answer: **config means that the typechecker just sort of assumes that any required kwargs that aren't provided explicitly come through that **config. that's disappointing and the only way to fix it is to change the calling convention which is a "whole thing".
sigh. Alright then.
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.
WrappedProverRunner.runis theProverRunnera plugin receives throughCVLAuthorState. It calledsetup_prover_config_inwithoutexclude_rule, a required keyword-only argument, so every plugin prover call raisedTypeError: setup_prover_config_in() missing 1 required keyword-only argument: 'exclude_rule'before it staged anything. The dz-strategy plugin'slemma_provertool is the caller that hit this.The runner and the
ProverRunnerprotocol now takeexclude_rulesnext torules, the wayverify_specscopes its own runs, and pass it through.tests/test_wrapped_prover_runner.pydrives the runner against a mockedrun_prover: all four cases fail on master with the error above and pass with this change. Pyright reports no errors.