Skip to content

Fix Refinement Declaration Positions - #331

Merged
rcosta358 merged 2 commits into
codex/smt-unknown-errorfrom
codex/refinement-declaration-position
Oct 6, 2026
Merged

rcosta358 merged 2 commits into
codex/smt-unknown-errorfrom
codex/refinement-declaration-position

Conversation

@rcosta358

@rcosta358 rcosta358 commented Oct 5, 2026 •

Copy link
Copy Markdown
Collaborator

Description

Highlight the predicate in “Refinement declared here” diagnostics by reading its annotation position directly, removing the dependency on parsing order.

Example

Before

image

After

image

Validation: 206 tests passed, including declaration-position regression tests.

Related Issues

Stacked on #330. Merge it first, then retarget to main.

🤖 Generated with Codex

@rcosta358 rcosta358 added bug Something isn't working error messages Related to error messages labels Oct 5, 2026
@rcosta358 rcosta358 changed the title Highlight predicates in refinement declaration diagnostics Fix Refinement Declaration Positions Oct 5, 2026
@rcosta358
rcosta358 added this pull request to stack #332 October 5, 2026 14:10

@CatarinaGamboa CatarinaGamboa left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

testing is a bit tricky, left a message

}
}

private static void assertPredicatePosition(SourcePosition position, Path file, String source, String predicate)

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we should be careful with these string checks cause we might decide change the erro message and then we have to change all these tests. Do you think theres a way to make it less dependendt?

@rcosta358
rcosta358 force-pushed the codex/refinement-declaration-position branch 3 times, most recently from cd8510a to ce7a2b7 Compare October 6, 2026 15:12
rcosta358 and others added 2 commits October 6, 2026 16:18
Co-authored-by: Codex <noreply@openai.com>
@rcosta358
rcosta358 force-pushed the codex/refinement-declaration-position branch from ce7a2b7 to a9e7e28 Compare October 6, 2026 15:18
@rcosta358
rcosta358 merged commit be47cb6 into main Oct 6, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug Something isn't working error messages Related to error messages

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants