module-info.java

[wadoon]

This pull request adds module support in KeY by adding module-info.java and doing the necessary stuff. Modules for key.util and key.ncore have already been added by @Drodt on main. This is dangerous situation where some jars are modules, some are not.

There are two main issues with modules in KeY:

• clashing Java packages (packages are sealed)
• Docking Frames is not-modularized

This PR does not change the package names, when not necessary.

Benefits: Along with adding the Java modules, various errors appeared and got repaired.
For examples, the slicing extension was added in the META-INF in KeY

Status

• In general this PR is ready!

• Except for one thing: We have a problem with ST4 library added by keyext.proofmanagement, due to the lack of module in ST4. There is a very old issue on antlr/stringtemplate4 open.
  There are two solutions:

  1. externalize proof management
  2. Add a Gradle dependencies transformer thingy

• This PR also removes the JUnit 4 libraries and support of all key submodules.
  This is one origin of errors when test cases can not be found. (There was only one JUnit test class left). JUnit 4 is still present in module recoder.

• There was a new version of docking frames needed, which I have build and added as a SNAPSHOT. This version will be publish to maven central when this PR is accepted.

• sun.misc.Signal: The signal handling for SIGTERM is dropped. On some (linux) computer, this does not work properly all times (you can not abort KeY anymore). On Windows, gradle prompts a compile error. In the end, Signal class is part of the jdk.unsupported module. At this point you should recognise that is more luck that it works.

• Note: Spotless format is terrible broken on module-info.java.

Plan

• Modularized Docking Frames (wip)
• key.ext libraries
• Code cleanup

Type of pull request

• Refactoring (behaviour should not change or only minimally change)

[codecov]

Codecov Report

Attention: Patch coverage is 0% with 2 lines in your changes are missing coverage. Please review.

Project coverage is 37.88%. Comparing base (7254776) to head (6b70371).
Report is 26 commits behind head on main.

❗ Current head 6b70371 differs from pull request most recent head dc253d7. Consider uploading reports for the commit dc253d7 to get more accurate results

Files	Patch %	Lines
...uka/ilkd/key/java/visitor/ProgramContextAdder.java	0.00%	1 Missing ⚠️
...e/uka/ilkd/key/nparser/builder/TacletPBuilder.java	0.00%	1 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3451      +/-   ##
============================================
+ Coverage     37.86%   37.88%   +0.01%     
- Complexity    17079    17083       +4     
============================================
  Files          2092     2091       -1     
  Lines        127596   127489     -107     
  Branches      21478    21460      -18     
============================================
- Hits          48316    48297      -19     
+ Misses        73355    73286      -69     
+ Partials       5925     5906      -19     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[Drodt]

I think using modules makes sense. But if there is a demand to remove the module-info files we added, I would not oppose it.

[wadoon]

I think using modules makes sense. But if there is a demand to remove the module-info files we added, I would not oppose it.

The JPMS is a very complicated thingy. It depends whether your Jars are in the classpath or module-path. The later one are recognised as modules. the first one is put into the unnamed module. But also Gradle and Maven have implemented some module magic to detect the suitable "path" for a Jar file.

I think we should do it right, and for this, I need to update and release the Docking Frames library, as this library also has package clashes.

[wadoon]

@WolframPfeifer Your extension is not JPMS-ready due to ST4.

[wadoon]

@Drodt On the Checkerframework PR we received compiler errors due to the partial introduction of modules.

Removal of module-info.java helped.

@flo2702

[wadoon]

closed in favor #3473