From 29e471e83fd61acf01cc566b5d448a8b427ffdd2 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 19 Jul 2025 02:03:46 +0200 Subject: [PATCH 1/4] first mvp --- build.gradle | 9 +++++++-- settings.gradle | 3 +++ 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/build.gradle b/build.gradle index b6a7211b062..d936942b2f6 100644 --- a/build.gradle +++ b/build.gradle @@ -53,6 +53,8 @@ group = "org.key-project" version = "3.1.0$build" subprojects { + if (it.name == 'dist') return + apply plugin: "java" apply plugin: "java-library" apply plugin: "idea" @@ -391,8 +393,11 @@ tasks.register('alldoc', Javadoc){ description = "Generate a JavaDoc across sub projects" def projects = subprojects //key.ui javadoc is broken - source projects.collect { it.sourceSets.main.allJava } - classpath = files(projects.collect { it.sourceSets.main.compileClasspath }) + source projects.findAll { it.name != "dist" }.collect { it.sourceSets.main.allJava } + classpath = files(projects + .findAll { it.name != "dist" } + .collect { it.sourceSets.main.compileClasspath } + ) destinationDir = layout.buildDirectory.dir("docs/javadoc").getOrNull().getAsFile() diff --git a/settings.gradle b/settings.gradle index 91c91de2d1e..6f32ac0b580 100644 --- a/settings.gradle +++ b/settings.gradle @@ -32,6 +32,9 @@ include "keyext.slicing" include "keyext.caching" include "keyext.isabelletranslation" + +include 'dist' + // ENABLE NULLNESS here or on the CLI // This flag is activated to enable the checker framework. // System.setProperty("ENABLE_NULLNESS", "true") From c9749d3df7806a4b652e71a992e0f5f83a2d3a63 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 19 Jul 2025 02:18:43 +0200 Subject: [PATCH 2/4] fix --- build.gradle | 5 +---- dist/build.gradle | 33 +++++++++++++++++++++++++++++++++ 2 files changed, 34 insertions(+), 4 deletions(-) create mode 100644 dist/build.gradle diff --git a/build.gradle b/build.gradle index d936942b2f6..9b46c6d2c67 100644 --- a/build.gradle +++ b/build.gradle @@ -53,8 +53,6 @@ group = "org.key-project" version = "3.1.0$build" subprojects { - if (it.name == 'dist') return - apply plugin: "java" apply plugin: "java-library" apply plugin: "idea" @@ -393,9 +391,8 @@ tasks.register('alldoc', Javadoc){ description = "Generate a JavaDoc across sub projects" def projects = subprojects //key.ui javadoc is broken - source projects.findAll { it.name != "dist" }.collect { it.sourceSets.main.allJava } + source projects.collect { it.sourceSets.main.allJava } classpath = files(projects - .findAll { it.name != "dist" } .collect { it.sourceSets.main.compileClasspath } ) destinationDir = layout.buildDirectory.dir("docs/javadoc").getOrNull().getAsFile() diff --git a/dist/build.gradle b/dist/build.gradle new file mode 100644 index 00000000000..ce21baa7624 --- /dev/null +++ b/dist/build.gradle @@ -0,0 +1,33 @@ +plugins { + id 'application' + id 'java-library' + id 'com.gradleup.shadow' version "8.3.8" +} + +def mainClasses = [ + removegenerics: 'de.uka.ilkd.key.util.removegenerics.Main', + key : "de.uka.ilkd.key.core.Main", + pm : "org.key_project.proofmanagement.Main", + rifltrans : "de.uka.ilkd.key.util.rifl.RIFLTransformer", +] + +mainClasses.each { name, mainClass -> + def task = tasks.register("create${name.capitalize()}StartScripts", CreateStartScripts) { + mainClassName = mainClass + applicationName = name + outputDir = file("$buildDir/scripts") + classpath = sourceSets.main.runtimeClasspath + } + installDist.dependsOn(task) +} + +repositories { + mavenCentral() +} + +dependencies { + implementation(project(":key.ui")) + implementation(project(":key.core.rifl")) + implementation(project(":key.removegenerics")) + implementation(project(":keyext.proofmanagement")) +} \ No newline at end of file From 71f42918f02284ce8d4dde68d4353b622032bbe9 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 26 Jul 2025 21:39:22 +0200 Subject: [PATCH 3/4] adding key-citool --- dist/build.gradle | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/dist/build.gradle b/dist/build.gradle index ce21baa7624..bf2165f187e 100644 --- a/dist/build.gradle +++ b/dist/build.gradle @@ -9,6 +9,7 @@ def mainClasses = [ key : "de.uka.ilkd.key.core.Main", pm : "org.key_project.proofmanagement.Main", rifltrans : "de.uka.ilkd.key.util.rifl.RIFLTransformer", + "ci-tool" : "io.github.wadoon.keycitool.CheckerKt", ] mainClasses.each { name, mainClass -> @@ -23,6 +24,9 @@ mainClasses.each { name, mainClass -> repositories { mavenCentral() + maven { + url = uri("https://central.sonatype.com/repository/maven-snapshots/") + } } dependencies { @@ -30,4 +34,21 @@ dependencies { implementation(project(":key.core.rifl")) implementation(project(":key.removegenerics")) implementation(project(":keyext.proofmanagement")) + + // 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: '' + } +} + + +distributions { + main { + distributionBaseName = "key" + contents { + from("$rootDir/README.md") + from("$rootDir/LICENSE.TXT") + } + } } \ No newline at end of file From ffdde35fcb5aa0cbbf353732df33da3505019b17 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 26 Sep 2026 20:31:50 +0200 Subject: [PATCH 4/4] 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 and without the bundled examples, alongside the existing fat shadowJar (key-*-exe.jar). Both jars are built as part of assemble, and the weekly build/release workflow as well as the Jenkins 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 ++++ dist/build.gradle | 6 ++-- key.ui/build.gradle | 44 +++++++++++++++++++++++++++++ scripts/jenkins/deployAll.sh | 2 +- 5 files changed, 58 insertions(+), 6 deletions(-) diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index 5a49ffa612d..388010ea6ca 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/dist/build.gradle b/dist/build.gradle index bf2165f187e..a7846fe220b 100644 --- a/dist/build.gradle +++ b/dist/build.gradle @@ -4,11 +4,11 @@ plugins { id 'com.gradleup.shadow' version "8.3.8" } +description = "KeY distribution with start scripts for the standalone command line tools" + def mainClasses = [ - removegenerics: 'de.uka.ilkd.key.util.removegenerics.Main', key : "de.uka.ilkd.key.core.Main", pm : "org.key_project.proofmanagement.Main", - rifltrans : "de.uka.ilkd.key.util.rifl.RIFLTransformer", "ci-tool" : "io.github.wadoon.keycitool.CheckerKt", ] @@ -31,8 +31,6 @@ repositories { dependencies { implementation(project(":key.ui")) - implementation(project(":key.core.rifl")) - implementation(project(":key.removegenerics")) implementation(project(":keyext.proofmanagement")) // third-party plugins diff --git a/key.ui/build.gradle b/key.ui/build.gradle index a380ab55e48..ddf6382d425 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,34 @@ shadowJar { mergeServiceFiles() } +// A slim variant of the shadowJar that omits the optional keyext 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 keyext extensions and without examples.zip" + 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() + + // no examples.zip in the slim distribution + exclude 'examples.zip' +} + +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 $?