You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
Rename the UNPROVABLE error category to UNKNOWN - #431
Renames the C4.2 error category from UNPROVABLE to UNKNOWN. Every refinement error means the verifier could not prove something, so "unprovable" does not set this case apart. What does is that nothing is known about the value or state.
ErrorCategory: UNPROVABLE → UNKNOWN, title now starts with "Unknown:"
RefinementError, StateErrorCategories and StateHints use the new name
Test case ErrorUnprovableArgument.java → ErrorUnknownArgument.java, test methods in TestErrorCategories renamed
No behaviour change in verification. The codebook ID (C4.2) is unchanged.
API break:ErrorCategory is public and returned by LJDiagnostic.getCategory(), so clients that reference ErrorCategory.UNPROVABLE no longer compile, and serialized enum names change from UNPROVABLE to UNKNOWN. No client in the organisation (vscode-liquidjava, liquidjava-mcp) uses the old name. Releases after 0.0.36 carry this change.
[Codex review] The internal rename is consistent: the category ID stays C4.2, the diagnostic and hint branches use UNKNOWN, and the full verifier suite passes locally at this head (./mvnw -q -pl liquidjava-verifier -am test). One compatibility detail missing from “No behaviour change”: ErrorCategory is public and returned by LJDiagnostic.getCategory(). External clients that reference ErrorCategory.UNPROVABLE will fail to compile against this version (and enum-name serialization changes). Please document this as an API break, or retain a compatibility path if consumers rely on that constant.
[Claude] Good point. The PR description now documents this as an API break: ErrorCategory.UNPROVABLE no longer compiles and serialized names change to UNKNOWN. I did not add a compatibility alias. No client in the organisation (vscode-liquidjava, liquidjava-mcp) references the old constant, 0.0.36 does not include the rename, and a deprecated duplicate constant would be a second category rather than an alias.
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
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.
Renames the C4.2 error category from
UNPROVABLEtoUNKNOWN. Every refinement error means the verifier could not prove something, so "unprovable" does not set this case apart. What does is that nothing is known about the value or state.ErrorCategory:UNPROVABLE→UNKNOWN, title now starts with "Unknown:"RefinementError,StateErrorCategoriesandStateHintsuse the new nameErrorUnprovableArgument.java→ErrorUnknownArgument.java, test methods inTestErrorCategoriesrenamedNo behaviour change in verification. The codebook ID (C4.2) is unchanged.
API break:
ErrorCategoryis public and returned byLJDiagnostic.getCategory(), so clients that referenceErrorCategory.UNPROVABLEno longer compile, and serialized enum names change fromUNPROVABLEtoUNKNOWN. No client in the organisation (vscode-liquidjava, liquidjava-mcp) uses the old name. Releases after 0.0.36 carry this change.Tests:
mvn -pl liquidjava-verifier -am testpasses (496 tests, 0 failures).🤖 Generated with Claude Code