Skip to content

Conversation

@Alidra
Copy link
Member

@Alidra Alidra commented Oct 8, 2025

This PR fixes the issue #1299 .
The new solution checks the error is located in the same file.
If not, the error is reported on the import command displaying the location in the imported file

@Alidra Alidra requested a review from fblanqui October 9, 2025 08:34
@Alidra
Copy link
Member Author

Alidra commented Oct 9, 2025

@nicomarg can you try this fix on your initial file please?

@Alidra Alidra marked this pull request as ready for review October 9, 2025 13:30
@Alidra Alidra linked an issue Oct 9, 2025 that may be closed by this pull request
@Alidra Alidra linked an issue Oct 15, 2025 that may be closed by this pull request
@fblanqui
Copy link
Member

@Alidra is this PR ready to be merged?

@Alidra
Copy link
Member Author

Alidra commented Oct 24, 2025

@fblanqui, I revert the last commit that removes all the OK diagnistics.
We can merge this PR to fix the location error and create a new one the better handle the diagnostics (we still need to discuss what a typical LP user want to see in terms of message and location)

@fblanqui fblanqui merged commit 1db22dc into Deducteam:master Oct 24, 2025
4 checks passed
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.

Wrong error location when reporting errors in another file

2 participants