Skip to content

Proper output for translation errors in IDE mode#308

Merged
marcoeilers merged 1 commit into
masterfrom
translation_errors_ide_mode
Jul 6, 2026
Merged

Proper output for translation errors in IDE mode#308
marcoeilers merged 1 commit into
masterfrom
translation_errors_ide_mode

Conversation

@marcoeilers

@marcoeilers marcoeilers commented Jul 6, 2026

Copy link
Copy Markdown
Owner

The --ide-mode command line option leads to error output in a fixed form that includes end lines and columns, like this:

Verification failed
Errors:
test_predicate_family_modularity.py:17:5:17:21: error: Fold might fail. Might not be able to satisfy constraints from currently unknown predicate family members.
test_predicate_family_modularity.py:23:5:24:47: error: Predicate state might not be well-formed. Predicate family addition might not be self-framing.
Verification took 9.41 seconds.

Currently, however, this formatting does not apply to translation errors, which look different:

Translation failed
Invalid program: abstract.predicate.fold (tests/functional/translation/test_abstract_pred_1.py@17.11)

This PR fixes that so that the --ide-mode flag applies to all errors:

Translation failed
tests/functional/translation/test_abstract_pred_1.py:17:12:17:33: error: Invalid program: abstract.predicate.fold

That also includes type errors, which requires setting an additional mypy flag:

Translation failed
testmcp.py:10:16:10:20: error: Type error: Incompatible return value type (got "int", expected "bool")  [return-value]
testmcp.py:12:16:12:19: error: Type error: Incompatible return value type (got "int", expected "bool")  [return-value]

This change is Reviewable

@marcoeilers
marcoeilers merged commit ceacbb3 into master Jul 6, 2026
18 checks passed
@marcoeilers
marcoeilers deleted the translation_errors_ide_mode branch July 6, 2026 20:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant