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

Fix for #3501: Decrease log level of duplicate sort warnings #3505

Merged
merged 4 commits into from
Aug 22, 2024

Conversation

WolframPfeifer
Copy link
Member

Description

This pull request addresses #3501. Since this a warning (or better, lots of them) that potentially confuses the users, this very minor PR decreases the log level from INFO to DEBUG.

These duplicate sort declarations in the taclet base have been there for quite a long time and do not break anything. The purpose of the warning is to indicate that we should finally get rid of the duplicate declarations. However, at the moment this is difficult due to the lack of local namespaces for generic sorts.

See also the discussion here: #3302

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@wadoon
Copy link
Member

wadoon commented Aug 13, 2024

I am not sure whether this should be info or debug. The namespaces for matching stuff seems to be file local, but nobody says this.

In the FM tutorial we have different solution by muting the category.

@WolframPfeifer
Copy link
Member Author

I am not sure whether this should be info or debug. The namespaces for matching stuff seems to be file local, but nobody says this.

In the FM tutorial we have different solution by muting the category.

I think the messages are confusing (or, at least, distracting from the more important CLI output) even for the developers of KeY, and we should mute them (i.e., move them to log level "DEBUG" such that they are not shown by default), at least as long the majority of those is there without a fix in sight. In my opinion, this is also a good idea for the main branch, not only for the FM tutorial.

About the namespaces: I have no idea about the current status (I think you are the expert there), but it would make sense to have a global namespace for the sorts (and fix the declarations such that there are no duplicates), but for schema variables it should be per file imo.

@WolframPfeifer
Copy link
Member Author

@wadoon Can we merge this (see explanation above)?

@wadoon wadoon enabled auto-merge August 22, 2024 12:03
@wadoon
Copy link
Member

wadoon commented Aug 22, 2024

Is the error in the checkerFramework consistent? Should we remove checkerFramework from the required checks?

@wadoon wadoon added this pull request to the merge queue Aug 22, 2024
@WolframPfeifer
Copy link
Member Author

What do you mean by consistent? The issue seems to exist on main for a while now.

I would not disable the check, but rather fix the issue if possible. However, I can not reproduce it on my local machine (tried on main) ...

@wadoon
Copy link
Member

wadoon commented Aug 22, 2024

It seems to be a heisenbug. You may notice that somehow, it was queued in the merge queue. I do not understand it and therefore I can't fix it.

Merged via the queue into main with commit 8077951 Aug 22, 2024
11 of 13 checks passed
@wadoon wadoon deleted the pfeifer/duplicateSortLogLevel branch August 22, 2024 13:51
@mattulbrich
Copy link
Member

I found out sth about the "Heisenbug". I could not reproduce it on my machine too. However, if I change the order of projects to be compiled, I can reproduce the error messages:

./gradlew -DENABLE_NULLNESS=true :key.ncore:compileTest :key.util:compileTest

@wadoon @WolframPfeifer

btw: ENABLE_NULLNESS is highly misleading. It should read ENABLE_NULLNESS_CHECKER or nonnull-checker or something.

@wadoon
Copy link
Member

wadoon commented Aug 23, 2024

This would be solved by clean.

The questions is: does Gradle compile or skip it this step?

But I would guess that the annotation processor is part of the incremental check.

@mattulbrich
Copy link
Member

It might also be that the settings are changed in ncore and these changed settings are used in other subprojects as well. I do not see that this subproject has individual settings for the checkerframework. so: depending on the order in which projects are compiled the problem may or may not arise ...

@wadoon
Copy link
Member

wadoon commented Aug 24, 2024

Look, ncore depends on util. The order should also not matter as util should be compiled before ncore always. The only difference is the -AonlyDefs=^org\\.key_project\\.util in the config, which limits the scope of checking.

Nonetheless, is the error from the checker framework spurious or not? I have no clue. At this point, we reached the same state with all the other tools we kicked out.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants