module-info.java, 2nd attempt#3623
Conversation
wadoon
force-pushed
the
weigl/module
branch
2 times, most recently
from
ef482fd to
a10effd
Compare
|
Is this really ready for review? |
A review should wait for #3621. This PR builds upon it (removal of ST4). |
# Conflicts: # keyext.proofmanagement/build.gradle
error in docking frames version, cannot find resource bundle � Conflicts: � key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java � key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java � key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestGenerationSettings.java � key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/SemanticsBlastingMacro.java � key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/TestGenerationSettings.java � key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/AbstractTestGenerator.java � key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/MemoryTestGenerationLog.java � key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/TestGenerationLog.java � key.ui/src/main/java/de/uka/ilkd/key/ui/util/CommandLine.java � keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/Main.java � keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java � keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java � keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenExtension.java � keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java
# Conflicts: # build.gradle # key.core.example/src/main/java/org/key_project/Main.java
unp1
left a comment
unp1
left a comment
There was a problem hiding this comment.
The Proof Caching extension is no longer there, when I start it via ./gradlew :key.ui:run
- we need most likely a mainModule in addition/instead of mainClass
But the problem then could be that ServiceLoader.load(...) for proof macros, scrips, PO, etc. have no declared uses in module-infos no opens, which means the on the module path ...util.reflection thorws InaccessibleObjectExceptions which is aproblem when the application is run via classpath
Shoul dwe expose in key-core the requires directives as transitive, so that depending modules don;t have to redeclare them?
|
We should rather give up on modules. In KaKeY, the predecessor PR #3845 was also not favoured. |
4 participants
Second run for module-info in KeY after the drop of ST4. Builds-upon #3621, should merged afterwards.
This pull request adds module support in KeY by adding
module-info.javaand doing the necessary stuff. There are three main issues with modules in KeY:clashing Java packages (packages are sealed)
(solved by renaming some packages)
Docking Frames is not-modularized
(Baked a new version, with renamed packages. **This version is on central snapshot repo, and should then be deployed to Maven central)
Caching extension in wrong service file
Additional:
Hint:
Type of pull request