Store warnings in a set rather than a list #7478
Merged
Conversation
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
8000
andreasabel
commented
Sep 9, 2024
andreasabel
commented
Sep 9, 2024
gallais
reviewed
Sep 11, 2024
andreasabel
commented
Sep 11, 2024
4b7068f to
e2a71db
Compare
andreasabel
commented
Sep 13, 2024
| SafeFlagPragma xs -> fsep $ concat | ||
| [ [ fsep $ pwords "Cannot set OPTIONS" ++ [ pluralS (words =<< xs) "pragma" ] ] | ||
| SafeFlagPragma sset -> vcat $ concat | ||
| [ [ fwords $ singPlural (words =<< xs) id (++ "s") "The --safe mode does not allow OPTIONS pragma" ] |
There was a problem hiding this comment.
Check whether this rewording isn't a regression.
| let sfp = case foldMap pragmas ws of | ||
| (TCWarning loc r w doc str b : _, sfp) -> | ||
| singleton $ TCWarning loc r (SafeFlagPragma sfp) doc str b | ||
| _ -> empty |
There was a problem hiding this comment.
Can we get rid entirely of this special logic for SafeFlagPragma? One of these possibilities:
- Make
SafeFlagPragmatake a single pragma name rather than a Set. - Store the
SafeFlagPragmawarning separately so that in the state these warnings are always properly aggregated.
Seems like 1. would be simplest.
Ad 2: We might want to aggregate other warnings as well (at least those that are deserialized), so we should have a uniform mechanism for that rather than this special case for SafeFlagPragma.
| @@ -1,6 +1,3 @@ | |||
| Issue5029.agda:1,1-45: warning: -W[no]WarningProblem | |||
| You may only turn off benign warnings. The warning TerminationIssue is a non-fatal error and thus cannot be ignored. See --help=warning. | |||
|
|
|||
There was a problem hiding this comment.
Removed duplicate.
Missing newline between warning and error.
There was a problem hiding this comment.
Missing newline between warning and error.
Cannot find the code position where to fix this.
| MdSpanningComment.lagda.md:10,3-16,7: Multi-line comment spans one or more literate text blocks. | ||
| error: [OverlappingTokensWarning] | ||
| MdSpanningComment.lagda.md:2,4-6,19: Multi-line comment spans one or more literate text blocks. |
There was a problem hiding this comment.
Missing range for this error.
There was a problem hiding this comment.
Attempt to fix this in #7492.
If `f` has inverse `g`, then check `g x ∈ s` is often faster then `x ∈ fmap f s`.
e2a71db to
6eaed7a
Compare
f274684 to
6f4715a
Compare
This ensures that warnings we register twice are not printed twice. Also, the warnings are printed in order of their range.
Now they will be printed in order of their Range.
6f4715a to
a387237
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Currently we store warnings in a list and have some hacks to prevent duplicate warnings.
Also, to join warning lists we use
List.unionwhich has a weird semantics.It would be more natural to use a
Setfor warnings.Currently we lack an
Ordinstance forTCWarningsinceDocdoes not have one.So here I cache the rendering of the warning doc as
tcWarningStringto facilitate anOrdinstance.The warnings should be ordered by position so the first component in the ordering is the
Rangeof the warning.WIP: For reasons very unclear to me, this first component is ignored, or the ranges there are mysteriously empty, so the warnings are ordered by the string rendering of their position.Thanks @plt-amy !I already tried to make sure that the ranges are serialized, but to no avail.
I need some help in debugging this.
New features: