Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Demote home unit closure errors to warnings. #3890

Merged
merged 2 commits into from
Dec 12, 2023
Merged

Demote home unit closure errors to warnings. #3890

merged 2 commits into from
Dec 12, 2023

Conversation

wz1000
Copy link
Collaborator

@wz1000 wz1000 commented Dec 5, 2023

Users can't really do anything to fix them until cabal 3.12 is released.
Perhaps they could previously get by despite the unsoundness before we started
throwing these errors.

So demote them to warnings to allow HLS to continue to "function" despite them.

@wz1000 wz1000 force-pushed the wip/multi-warn branch 2 times, most recently from 341b3c7 to ad802da Compare December 5, 2023 12:34
Users can't really do anything to fix them until cabal 3.12 is released.
Perhaps they could previously get by despite the unsoundess before we started
throwing these errors.

So demote them to warnings to allow HLS to continue to "function" despite them.
Copy link
Collaborator

@fendor fendor left a comment

Choose a reason for hiding this comment

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

Looks good to me, but I didn't look at the diff in detail.

@wz1000
Copy link
Collaborator Author

wz1000 commented Dec 11, 2023

Looks good to me, but I didn't look at the diff in detail.

it's quite small if you ignore whitespace changes.

@fendor
Copy link
Collaborator

fendor commented Dec 11, 2023

Yeah, essentially merely the case branch has been removed and you report potential closure property violations as warnings. So LGTM :)

@michaelpj michaelpj added the merge me Label to trigger pull request merge label Dec 12, 2023
@mergify mergify bot merged commit e0a9faf into master Dec 12, 2023
40 of 41 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
merge me Label to trigger pull request merge
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants