ci: type-check certora_autosetup in pyright#17
Merged
Conversation
certora_autosetup (imported from the AutoSetup repo) wasn't covered by pyright — the existing run scopes only composer/analyzer/sanity_analyzer. Add it via a dedicated pyrightconfig.autosetup.json at the basic bar it was written against in AutoSetup, run as a second pyright step. Kept separate so it need not meet the composer/analyzer standard profile (which would flag 36 now-redundant # type: ignore comments plus 17 pre-existing findings). The main pyrightconfig.json is unchanged. No pyproject/uv.lock change — lockfile-check and pin-sync unaffected. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Replaces the separate lenient pyrightconfig.autosetup.json (basic mode) with folding certora_autosetup into the main standard pyright scope, and fixes the 17 findings it surfaced: - 2 reportIncompatibleMethodOverride: base ProverRunner.submit_jobs was annotated List[SubmissionResult | BaseException], but both impls convert exceptions to SubmissionResult and return List[SubmissionResult] (and the base body is abstract with no callers). Narrow the base annotation to List[SubmissionResult] — matches the docstring and the implementations. - 15 reportPossiblyUnboundVariable: initialize/hoist each local before the branch or loop it's read after (desc_text, config_type, contract_name, current_stripped, enum_members/struct_members, fs/cache_file, output, contracts_added, output_idx). No behavioral change on the real paths — the inits just make boundness provable. pyright.yml now runs `pyright composer/ analyzer sanity_analyzer certora_autosetup`; pyrightconfig.json includes certora_autosetup. No pyproject/uv.lock change. Verified: full-scope pyright 0 errors; AutoSetup's 450 unit tests pass against the modified package. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
jtoman
approved these changes
Jun 25, 2026
jtoman
left a comment
jtoman
left a comment
Contributor
There was a problem hiding this comment.
stamping the pyright config stuff, I'll leave the autosetup stuff to those with more context.
| @@ -1,5 +1,5 @@ | |||
| { | |||
| "include": ["composer", "analyzer"], | |||
| "include": ["composer", "analyzer", "certora_autosetup"], | |||
Contributor
There was a problem hiding this comment.
sanity_analyzer too while we're here.
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.
certora_autosetup(imported from the AutoSetup repo in #2) wasn't covered by pyright — the existing run scopes onlycomposer/analyzer/sanity_analyzer.Change
pyrightconfig.autosetup.json— a dedicated profile forcertora_autosetupat the basic bar it was written against in AutoSetup (reportMissingImports=none, thereportUnknown*/reportPrivateUsage=noneoverrides it originally used).pyright -p pyrightconfig.autosetup.jsonstep inpyright.yml.Why a separate profile
Folding
certora_autosetupinto the main (standard)pyrightconfig.jsonproduces 53 errors: 36 are now-redundant# type: ignorecomments (the suppressed imports resolve here, so they read as "unnecessary"), plus 17 pre-existing findings (15reportPossiblyUnboundVariable, 2reportIncompatibleMethodOverride). Rather than refactor 53 sites in freshly-migrated code, this checks it at its origin bar. Tightening to the fullstandardprofile is a possible later follow-up. The mainpyrightconfig.json(composer/analyzer/sanity_analyzer strict) is unchanged.No
pyproject.toml/uv.lockchange →lockfile-checkandpin-syncunaffected.Verification
Local:
pyright composer/ analyzer sanity_analyzer→ 0 errors (unchanged);pyright -p pyrightconfig.autosetup.json→ 0 errors.🤖 Generated with Claude Code