From 961eb32fd8a0ab5ab78ce1a814fac69bf96abf34 Mon Sep 17 00:00:00 2001
From: Alexander Weigl <weigl@kit.edu>
Date: Sat, 26 Sep 2026 20:31:50 +0200
Subject: [PATCH] Add slim shadowJar variant for key.ui and fix dist build

Add a slimRuntimeClasspath configuration and a slimJar ShadowJar task
that produce a minimal executable jar (key-*-slim-exe.jar) without the
optional keyext extensions, alongside the existing fat shadowJar
(key-*-exe.jar). Both jars are built as part of assemble, and the weekly
build/release workflow deploy script upload the slim jar, too.

Also fix the dist project which referenced the removed key.core.rifl and
key.removegenerics modules and was missing a description, which broke
Gradle configuration of every build.
---
 .github/workflows/nightlydeploy.yml |  6 ++++-
 README.md                           |  6 +++++
 key.ui/build.gradle                 | 41 +++++++++++++++++++++++++++++
 scripts/jenkins/deployAll.sh        |  2 +-
 4 files changed, 53 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml
index 0c0bd5cd7c1..953ee83037a 100644
--- a/.github/workflows/nightlydeploy.yml
+++ b/.github/workflows/nightlydeploy.yml
@@ -31,10 +31,12 @@ jobs:
       - name: Build with Gradle
         run: ./gradlew --parallel assemble javadoc alldoc
 
-      - name: Upload ShadowJar
+      - name: Upload ShadowJars (fat and slim)
         uses: actions/upload-artifact@v7
         with:
           name: shadowjars
+          # matches the fat jar (key-*-exe.jar) and the slim jar
+          # (key-*-slim-exe.jar) of key.ui, plus any other module artifacts
           path: "*/build/libs/*-exe.jar"
           retention-days: 1
 
@@ -61,6 +63,8 @@ jobs:
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         run: |
+          # key-*-exe.jar matches both the fat jar (key-*-exe.jar) and the
+          # slim jar (key-*-slim-exe.jar) built by :key.ui:shadowJar / :key.ui:slimJar.
           gh release create --generate-notes --title "Nightly Release" \
              --prerelease --notes-start-tag KEY-3.0.0-rc \
              nightly key.ui/build/libs/key-*-exe.jar key-javadoc.tar.xz
diff --git a/README.md b/README.md
index afefe0b4eff..537267bd233 100644
--- a/README.md
+++ b/README.md
@@ -75,6 +75,12 @@ Assuming you are in the directory of this README file, you can create a runnable
    ./gradlew :key.ui:shadowJar
    ```
    The file is generated in `key.ui/build/libs/key-*-exe.jar`.
+   A slim variant without the optional keyext extensions and the bundled examples is created with
+   ```sh
+   ./gradlew :key.ui:slimJar
+   ```
+   The file is generated in `key.ui/build/libs/key-*-slim-exe.jar`.
+   Both jars are also built as part of `./gradlew assemble`.
 
 5. A distribution is build with
    ```sh
diff --git a/key.ui/build.gradle b/key.ui/build.gradle
index a380ab55e48..a08d51ef0e7 100644
--- a/key.ui/build.gradle
+++ b/key.ui/build.gradle
@@ -1,3 +1,5 @@
+import com.github.jengelman.gradle.plugins.shadow.tasks.ShadowJar
+
 import java.nio.file.Files
 import java.nio.file.Paths
 
@@ -40,6 +42,20 @@ dependencies {
     runtimeOnly project(":keyext.isabelletranslation")
 }
 
+// Slim runtime classpath: the full runtimeClasspath minus the optional keyext
+// extension modules. Used to produce the slim shadowJar (see task "slimJar").
+configurations {
+    slimRuntimeClasspath {
+        extendsFrom runtimeClasspath
+        exclude group: 'org.key-project', module: 'keyext.ui.testgen'
+        exclude group: 'org.key-project', module: 'keyext.caching'
+        exclude group: 'org.key-project', module: 'keyext.exploration'
+        exclude group: 'org.key-project', module: 'keyext.slicing'
+        exclude group: 'org.key-project', module: 'keyext.proofmanagement'
+        exclude group: 'org.key-project', module: 'keyext.isabelletranslation'
+    }
+}
+
 tasks.register('createExamplesZip', Zip) {
     description = 'Create "examples.zip" containing all KeY examples'
     destinationDirectory = layout.buildDirectory.dir("resources/main/").getOrNull()
@@ -60,6 +76,31 @@ shadowJar {
     mergeServiceFiles()
 }
 
+// A slim variant of the shadowJar that omits the optional KeY extension
+// modules and the bundled examples.zip. Produces "key-slim-exe.jar".
+tasks.register('slimJar', ShadowJar) {
+    group = "shadow"
+    description = "Create a slim executable jar 'key-slim-exe.jar' without the KeY extensions"
+    archiveClassifier.set("slim-exe")
+    archiveBaseName.set("key")
+
+    from(sourceSets.named('main').map { it.output })
+    configurations = project.configurations.named('slimRuntimeClasspath').map { [it] }
+
+    manifest {
+        attributes 'Main-Class': 'de.uka.ilkd.key.core.Main'
+    }
+
+    filesMatching("META-INF/services/**") {
+        duplicatesStrategy = DuplicatesStrategy.INCLUDE // needed for mergeServices
+    }
+    mergeServiceFiles()
+}
+
+tasks.named('assemble') {
+    dependsOn tasks.named('slimJar')
+}
+
 distZip {
     archiveBaseName.set("key")
 }
diff --git a/scripts/jenkins/deployAll.sh b/scripts/jenkins/deployAll.sh
index 6d68d70bbd0..e2186e8668f 100755
--- a/scripts/jenkins/deployAll.sh
+++ b/scripts/jenkins/deployAll.sh
@@ -1,5 +1,5 @@
 #!/bin/sh
-./gradlew --parallel clean compileTest :key.ui:shadowJar :key.ui:distZip
+./gradlew --parallel clean compileTest :key.ui:shadowJar :key.ui:slimJar :key.ui:distZip
 
 if [ $? -gt 0 ]; then
   exit $?