A tale of two fixes#24
Merged
Merged
Conversation
shellygr
commented
Jun 28, 2026
shellygr
commented
Contributor
- For code without user-defined data types, the summary resolver would crash since it would send an empty block to the LLM. Handle this case to avoid it triggering. Point to consider: make a more global fix in graphcore?
- Autosetup failed on a second run on the same project when parsing *_call_resolution.spec due to ASTExtraction output mishandling, trying to parse non-json as json. Context: It is part of the code that comments out irrelevant auto-injected summaries.
… deal with Warnings and Errors prepended before the actual json in stdout. We drop the non-json messages and handle with proper logging any remaining json decode errors
The pure _parse_ast_payload parser is unit-tested in the cheap pytest CI job, which installs deps without the prover extra (no certora_cli). The module-level `from certora_cli... import find_jar` made importing the module — and thus collecting tests/test_summary_resolver.py — fail with ModuleNotFoundError. find_jar is the only certora_cli symbol in this module's import chain, so defer it into _ast_extraction (matching existing lazy-import patterns in the package). The module now imports without certora_cli; the parser test runs in fast CI. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
The cheap pytest job synced deps without certora_cli, so collecting tests/test_summary_resolver.py (which imports certora_autosetup.setup. summary_resolver -> certora_cli find_jar) failed with ModuleNotFoundError. Provide the dependency in CI (`uv sync --group test --extra prover`) rather than contorting the module to import without it. Reverts the lazy-import change from 17953ef; summary_resolver keeps its top-level find_jar import. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
jtoman
approved these changes
Jun 30, 2026
jtoman
left a comment
jtoman
left a comment
Contributor
There was a problem hiding this comment.
approving the AIC parts, leaving AS parts to my betters
| curr_spec=None, | ||
| input=[ | ||
| "The following types are available for use in your spec", | ||
| udts, |
Contributor
There was a problem hiding this comment.
I know that sending an empty string as the entire message payload could cause an error, but an empty string in the messages array is a new one. agreed on the fix at the graphcore level, something we can fold into the "invoke" wrappers I've added in Certora/graphcore#21
Contributor
Author
There was a problem hiding this comment.
have you applied this in graphcore#21? it seems not?
Contributor
There was a problem hiding this comment.
not yet, since I didn't want to make this PR rely on a fix that hasn't landed yet. But there's no reason not to do it now anyway...
naftali-g
approved these changes
Jun 30, 2026
naftali-g
left a comment
naftali-g
left a comment
Contributor
There was a problem hiding this comment.
a nit and a comment, but approving to not block
| except json.JSONDecodeError as exc: | ||
| raise RuntimeError( | ||
| f"{_AST_EXTRACTION_JAR} output was not JSON after stripping diagnostics " | ||
| f"(exit {returncode}): {exc}; stdout_head={stdout[:300]!r} stderr={stderr.strip()[:500]!r}" |
Contributor
There was a problem hiding this comment.
just print all stdout and stderr, no?
Co-authored-by: Naftali Goldstein <44599898+naftali-g@users.noreply.github.com>
…a/AutoProver into shelly/autoprover-summaries-fixes
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
3 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.