For discussion: KeY distribution as ZIP

[wadoon]

Related Issue

Current upload to Maven Central reaches 500MB. One of problems are all the shadowJars that are build, and included to the upload.

This PR evaluates the option of building and shipping a zip distribution with multiple start scripts.

Intended Change

Build with gradle :dist:installDist results into a folder dist/build/install/dist that is the ship distribution looking as follows:

C:.
├───bin
│       dist
│       dist.bat
│       key
│       key.bat
│       pm
│       pm.bat
│       removegenerics
│       removegenerics.bat
│       rifltrans
│       rifltrans.bat
│
└───lib
        14312248 lib/icu4j-75.1.jar
        9747289 lib/scalaz-core_2.13-7.3.8.jar
        5924141 lib/scala-library-2.13.14.jar
        5920361 lib/key.core-2.12.4-dev.jar
        5400539 lib/key.ui-2.12.4-dev.jar
        3051356 lib/guava-33.2.1-jre.jar
        2519475 lib/docking-frames-core-1.1.3p1.jar
        925551 lib/flatlaf-3.6.jar
        903296 lib/docking-frames-common-1.1.3p1.jar
        894840 lib/recoder-2.12.4-dev.jar
        657952 lib/commons-lang3-3.14.0.jar
        653817 lib/scala-isabelle_2.13-0.4.3.jar
        627250 lib/logback-core-1.5.18.jar
        508826 lib/commons-io-2.16.1.jar
        478506 lib/key.core.symbolic_execution-2.12.4-dev.jar
        389033 lib/bsh-2.0b6.jar
        331716 lib/backport-util-concurrent-3.1.jar
        326307 lib/antlr4-runtime-4.13.2.jar
        308523 lib/retrotranslator-runtime-1.2.9.jar
        306760 lib/logback-classic-1.5.18.jar
        274294 lib/javacc-4.0.jar
        251227 lib/commons-text-1.12.0.jar
        251081 lib/ST4-4.3.4.jar
        230830 lib/checker-qual-3.42.0.jar
        173831 lib/retrotranslator-transformer-1.2.9.jar
        173220 lib/antlr-runtime-3.5.3.jar
        151546 lib/key.ncore.calculus-2.13.0.jar
        143017 lib/key.util-2.12.4-dev.jar
        138176 lib/keyext.isabelletranslation-2.12.4-dev.jar
        126113 lib/asm-9.8.jar
        120438 lib/miglayout-core-11.4.2.jar
        119210 lib/keyext.slicing-2.12.4-dev.jar
        97648 lib/keyext.proofmanagement-2.12.4-dev.jar
        93618 lib/key.core.testgen-2.12.4-dev.jar
        69908 lib/slf4j-api-2.0.17.jar
        68972 lib/log4s_2.13-1.10.0.jar
        44998 lib/key.ncore-2.12.4-dev.jar
        42266 lib/keyext.caching-2.12.4-dev.jar
        41658 lib/keyext.exploration-2.12.4-dev.jar
        36175 lib/java-patterns-0.1.0.jar
        35434 lib/key.core.rifl-2.12.4-dev.jar
        30570 lib/annotations-24.1.0.jar
        28709 lib/key.removegenerics-2.12.4-dev.jar
        27487 lib/keyext.ui.testgen-2.12.4-dev.jar
        23287 lib/miglayout-swing-11.4.2.jar
        19936 lib/jsr305-3.0.2.jar
        19373 lib/error_prone_annotations-2.26.1.jar
        18049 lib/key.core.proof_references-2.12.4-dev.jar
        15703 lib/slf4j-simple-2.0.13.jar
        4740 lib/failureaccess-1.0.2.jar
        3819 lib/jspecify-1.0.0.jar
        2199 lib/listenablefuture-9999.0-empty-to-avoid-conflict-with-guava.jar
        261 lib/dist.jar

Plan

• @unp1 @mattulbrich Some of the dependencies should not be there: listenablefuture-..., jsr305-3.0.2.jar, javacc, icu4j (unicode library from antlr) , guava, commons-io, antlr3-runtime, ...
• Should we also include third-party apps? ci-tool, interaction-log
• Externalize the taclet-base and JavaRedux?
• Update "How to Release KEY`
• Update nightly.yml

Type of pull request

• New deployment
• Breaking change
  • Removal of shadowJars for side products

[wadoon]

• ST4 (stringtemplate) uses antlr3
• scala-* uses annotations, guava, commons-io, common-text, common-lang, icu4j, java-patterns, slf4j-simple
  • guava uses checker-qual, failureaccess, jsr305, listenablefuture-, log4s
• javacc in runtime? Really needed?

There should never be two slf4j logging backends in the classpath. Now we have slf4j-simple (via scala) and logback-classic. Please repair (@BookWood7th).

SLF4J(W): Class path contains multiple SLF4J providers.
SLF4J(W): Found provider [ch.qos.logback.classic.spi.LogbackServiceProvider@3f8f9dd6]
SLF4J(W): Found provider [org.slf4j.simple.SimpleServiceProvider@aec6354]
SLF4J(W): See https://www.slf4j.org/codes.html#multiple_bindings for an explanation.
SLF4J(I): Actual provider is of type [ch.qos.logback.classic.spi.LogbackServiceProvider@3f8f9dd6]

[BookWood7th]

There should never be two slf4j logging backends in the classpath. Now we have slf4j-simple (via scala) and logback-classic. Please repair (@BookWood7th).

#3639 should fix this by excluding the slf4j-simple module in all configurations of the isabelleTranslation module.

[wadoon]

key-citool is now on Maven Central also as a SNAPSHOT for key-2.12.4.

It is also added to the distribution:

    // third-party plugins
    runtimeOnly("io.github.wadoon.key:key-citool:1.7.0-SNAPSHOT") {
        exclude group: "org.key-project", module: ''
        exclude group: "org.slf4j", module: ''
    }

[wadoon]

On verifaps, I have a distribution which includes also the external tools: