Add version support for verifier specs - #4
Merged
Conversation
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 subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
Each spec now declares which verifier versions it supports. formal_lib/version.py adds Version (dotted numeric, compared numerically, trailing zeros normalized so 6.7.0 equals 6.7) and VersionRange (inclusive bounds, a None bound means unbounded on that side). IssueRegexSpec gains a versions list holding exact versions and/or ranges, defaulting to a single unbounded range meaning all versions.
SPECS changes shape from dict[str, IssueRegexSpec] to dict[str, list[IssueRegexSpec]] so one backend name can hold one spec per supported version range, listed newest first. This is a breaking change for any code that indexed SPECS directly. The new resolve_spec(backend, output) picks within a backend by trying each spec's detect pattern and falling back to the first listed, and the CLI uses it for --backend.
hatch run check-specs runs the new conflict checker: within one backend no two specs may support the same version, since backend resolution could no longer tell which spec owns output from that version. The -v flag also lists every spec and the versions it supports. The hatch script definition needs an explicit {args} placeholder in pyproject.toml, otherwise hatch silently swallows flags like -v.
The regression suite understands version categories: a directory component named v6.7.0-v6.10.0, v6.7.0-, -v6.10.0, or exact v6.7.1 constrains the samples beneath it to specs whose versions overlap that range, samples outside a version directory run against every spec of their backend, and a guard test fails if a constrained sample overlaps no spec so samples cannot silently drop out of the suite. The test now parses in-process with IssueSpecOutputParser instead of a subprocess so the version directory, not detect, decides which spec runs, which also cut the suite from about 7s to under a second. Existing samples moved into categories proven by each log's own version banner: cbmc/v6.7.1, kani/v0.67.0, esbmc/v8.1.0 and esbmc/v8.2.0, pytest/v8.4.2. Clang logs carry no version banner and stay unconstrained.
CI runs check-specs -v as a spec-conflicts job in the reusable test workflow, so it gates PRs, pushes to master, and releases. CLAUDE.md and the README document the versioning workflow.