KeYProject
Fix for #3501: Decrease log level of duplicate sort warnings
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.
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 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.
Is the error in the checkerFramework consistent? Should we remove checkerFramework from the required checks?
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) ...
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.
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.
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.
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 ...
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.