Update Intellij project files for Java17

[daniel-raffler]

Hello,

this PR tries to update the Intellij project files for Java17. It's a draft for now, as I'm not sure if more changes that will be needed

@baierd
i believe you're also using Intellij? Could you please give it a try to see if it's working?

[kfriedberger]

JavaSMT does not depend on the package androidx. We might want to remove these line.

[daniel-raffler]

Hello Karlheinz,
thanks for the hint! I've now removed some of the nullable annotations we're not using. For the rest the "remove" button is greyed out in the GUI, maybe because they're used by one of our dependencies?

From what I understand, this is just a list of annotations that Intellij will recognize for its own nullable analysis. So having some additional ones in there shouldn't cause too many problems

[kfriedberger]

The entry for JDK is a good catch. CPAchecker does not use the JDK-entry, see https://github.com/sosy-lab/cpachecker/blob/main/.idea/ , and seems to work well, too.

Overall, if that helps someone, ok for me.

[baierd]

I reworked the IntelliJ configs of CPAchecker last year and can take a look or even do it myself quickly on the bases of CPAchecker. But we can't just re-use them from other projects, as the setup needs to be specific. (It took me quite a while to understand how this works, as the documentation of IntelliJ IDEA was very incomplete on several issues. The behavior of a IntelliJ configuration that is only partially correct, as every IntelliJ user knowns, is that things (e.g. dependencies) are not automatically updated or pulled, licenses are removed/added in config files all the time randomly, the configs are changed constantly by IntelliJ despite settings that it should not etc.)

[baierd]

@daniel-raffler Review here instead of the code:
(I think it is a good idea to have someone in the team that understands how this works besides me, so I'll provide a review for you to work on.)

In CPAchecker i used Ant to get all information about classpaths etc. by adding the flag -verbose.
Then i transfered the information to the sections relevant in the IntelliJ IDEA configs. This ensures that both do (roughly) the same.

You can get the classpath info by searching for the string classpath in the output for example.
Other relevant parts for dependencies are sources and native libraries. This is specified in IntelliJ IDEAs Project Settings -> Modules.
Important: we may only load dependencies that are loaded when compiling using Ant! Many projects are present multiple times and with distinct source-locations. This can cause conflicts in IntelliJ IDEA!

If we want to do this properly, we need to define modules for all solvers and their dependencies. Since i don't know how this works if we can't load a solver, we need to test this thoroughly!

Running Ant in verbose mode seems to indicate a problem with OptionCollector by the way.

Further, a default copyright header can be defined in Settings -> Copyright -> Formatting -> Java. This should be done as in CPAchecker.

Also, we can get rid of many edits of IntelliJ IDEA on its own configuration files by extracting the licenses in them into a file, for example like this.

Also, we should define which nullness annotations we actually want to use. This is defined in our Ant configs and IntelliJ should not diverge. Example from CPAchecker here. This can be set in the settings (no need to touch the config code directly). I also don't see a reason to load all annotation frameworks. It is sufficient to load only the ones we need (see lines following this).

We should set all flags that stop IntelliJ from editing itself all the time. That's not perfect, but helps a lot (or i did not find all flags? But it is a common problem reported online, so i don't know....). I don't remember where you can set this in the settings, but the config change in CPAchecker can be seen here for example.

I don't see a reason to change the compiler or compiler settings in JavaSMT. That was only needed in CPAchecker due to problems that are not present in JavaSMT!

You can find the MR from CPAchecker here. Some things are not optimal there, and some are not applicable for JavaSMT. E.g. i used a single module dependency for CPAchecker, but JavaSMT should define multiple.

[daniel-raffler]

@baierd Thanks for the summary!

I've already split off the license headers and cleaned up the @Nullable annotations. The project now uses a separate library dependency for each solver backend that has a *.jar file. Solvers that only bundle native code don't need a dependency as we use NativeLibrary for loading anyway. (It would be possible to still add one, but we would have to pick a CPU architecture)

Whenever possible I also included the *-sources.jar in the library dependencies, so that it can be found when running the debugger. However, we're currently missing sources for some solvers, and I wasn't able to step into the OpenSMT jar (maybe we compiled without debugging info?)

Important: we may only load dependencies that are loaded when compiling using Ant! Many projects are present multiple times and with distinct source-locations. This can cause conflicts in IntelliJ IDEA!

Hmm.. I'm not sure, but shouldn't Ivy already have taken care of these conflicts?