A JavaFX UI for KeY

.github/workflows/code_quality.yml

@@ -13,10 +13,10 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v7
-      - name: Set up JDK 21
+      - name: Set up JDK 25
         uses: actions/[email protected]
         with:
-          java-version: 21
+          java-version: 25
           distribution: 'corretto'
           cache: 'gradle'
       - name: Setup Gradle
@@ -31,7 +31,7 @@ jobs:
       - uses: actions/[email protected]
         with:
           distribution: 'corretto'
-          java-version: '21'
+          java-version: 25
           cache: 'gradle'
       - name: Build with Gradle
         run: ./gradlew --parallel --continue spotlessCheck

.github/workflows/nightlydeploy.yml

@@ -10,7 +10,7 @@ permissions:
   id-token: write
 
 env:
-  JAVA_VERSION: 21
+  JAVA_VERSION: 25
 
 
 jobs:

.github/workflows/release-tests.yml

@@ -15,7 +15,7 @@ jobs:
       fail-fast: false
       matrix:
         os: [ macos-latest, ubuntu-latest, windows-latest ]
-        java: [ 21, 25 ]
+        java: [ 25 ]
     continue-on-error: false
     runs-on: ${{ matrix.os }}
     env:
@@ -72,7 +72,7 @@ jobs:
       matrix:
         test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testRunAllWdProofs, testProveSMTLemmas ]
         os: [ macos-latest, ubuntu-latest, windows-latest ]
-        java: [ 21, 25 ]
+        java: [ 25 ]
         z3: [ '4.15.4' ]
         cvc5: [ '1.3.2' ]
 
@@ -119,7 +119,7 @@ jobs:
       matrix:
         test: [ testProveSMTLemmas, testStrictSMT ]
         os: [ macos-latest, ubuntu-latest, windows-latest ]
-        java: [ 21 ]
+        java: [ 25 ]
         z3: [ '4.13.4', '4.14.1', '4.15.4' ]
         cvc5: [ '1.3.2', '1.2.1' ]
     runs-on: ${{ matrix.os }}

.github/workflows/tests.yml

@@ -24,12 +24,17 @@ jobs:
       fail-fast: false
       matrix:
         os: [ ubuntu-latest, windows-latest ]
-        java: [ 21 ]
+        java: [ 25 ]
         modules: [
           keyext.exploration, keyext.slicing, key.ncore, key.ui, key.core,
           key.core.testgen, keyext.isabelletranslation,  keyext.ui.testgen,  key.ncore.calculus,
           key.util, key.core.example, keyext.caching, key.core.wd, key.core.infflow,
-          keyext.proofmanagement]
+          keyext.proofmanagement,
+          # JavaFX UI module and its six keyext ports (MP9.x): the unit tests are toolkit-free
+          # and headless-safe (the one panel test that needs the FX toolkit skips on
+          # display-less runners), see the per-module READMEs.
+          key.ui.fx, keyext.caching.fx, keyext.exploration.fx, keyext.isabelletranslation.fx,
+          keyext.slicing.fx, keyext.ui.testgen.fx, keyext.proofmanagement.fx]
     continue-on-error: true
     runs-on: ${{ matrix.os }}
     env:
@@ -51,7 +56,7 @@ jobs:
       - name: cvc5 version
         run: cvc5 --version
 
-      - name: Set up JDK 21
+      - name: Set up JDK 25
         uses: actions/[email protected]
         with:
           java-version: ${{ matrix.java }}
@@ -86,11 +91,11 @@ jobs:
       matrix:
         test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testRunAllWdProofs, testMtStress, testMt2w, testMt4w ]
         os: [ ubuntu-latest ]
-        java: [ 21 ]
+        java: [ 25 ]
     runs-on: ${{ matrix.os }}
     steps:
       - uses: actions/checkout@v7
-      - name: Set up JDK 21
+      - name: Set up JDK 25
         uses: actions/[email protected]
         with:
           java-version: ${{ matrix.java }}

.github/workflows/ui-verify.yml

@@ -0,0 +1,76 @@
+name: UI verify sweep (key.ui.fx)
+
+# Full per-flag regression sweep of the JavaFX UI (WP-11 deliverable): every
+# -Dkey.fx.verify.* hook of key.ui.fx runs headlessly against real example proofs inside an
+# Xvfb display (software rendering). Maximum parallelization: ONE matrix job per flag
+# (recipes in key.ui.fx/ci/verify-sweep.sh); the themepersist save+restore pair and the
+# special runs (xdotool key dismissal, real-z3 SMT, natural-exit loadingexit) are single
+# matrix entries with multiple runs inside. Logs are uploaded per flag.
+on:
+  push:
+    branches: [ "main", "weigl/ocfx", "weigl/ocfx-wp11-endgame" ]
+    paths:
+      - "key.ui.fx/**"
+      - "keyext.caching.fx/**"
+      - "keyext.exploration.fx/**"
+      - "keyext.isabelletranslation.fx/**"
+      - "keyext.proofmanagement.fx/**"
+      - "keyext.slicing.fx/**"
+      - "keyext.ui.testgen.fx/**"
+      - ".github/workflows/ui-verify.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  sweep:
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    strategy:
+      fail-fast: false
+      matrix:
+        flag: [ sequent, tree, goallist, notifications, docking, help, soundiness,
+                profileloading, javacsettings, termmenu, colors, shortcuts, sequentmenu,
+                dialogs, search, sequentsearch, sequentsearchmodes, treefilters,
+                tacletmatch, inputfreeze, updatehighlight, lemmaorigin, joinmerge,
+                joinmerge-gcd, proofmgmt-all, extensions, exploration, caching, prooftree,
+                slicing, testgen, heatmap, isabelle, sourceconsistency, autosave,
+                minimizeinteraction, themepersist, profileloadingdialog, smt, loadingexit,
+                proofdiff, drawer, drawerlayout, rightclickmacro ]
+    steps:
+      - uses: actions/checkout@v7
+
+      - name: Setup SMT solvers
+        uses: keyproject/setup-smt@v0
+        with:
+          z3Version: 4.13.0
+
+      - name: Set up JDK 25
+        uses: actions/[email protected]
+        with:
+          java-version: 25
+          distribution: 'corretto'
+          cache: 'gradle'
+
+      - name: Setup Gradle
+        uses: gradle/actions/setup-gradle@v6
+
+      - name: Install Xvfb, xdotool (key dismissal), graphviz (slicing DOT render)
+        run: |
+          sudo apt-get update
+          sudo apt-get install -y --no-install-recommends xvfb xdotool graphviz
+
+      - name: Run the UI verify sweep (${{ matrix.flag }})
+        run: bash key.ui.fx/ci/verify-sweep.sh ${{ matrix.flag }}
+
+      - name: Upload sweep logs (${{ matrix.flag }})
+        uses: actions/upload-artifact@v7
+        if: always()
+        with:
+          name: ui-verify-${{ matrix.flag }}
+          path: |
+            build/ui-verify/*.log
+            build/ui-verify/RESULTS.md
+            build/ui-verify/failed-flags.txt
+          if-no-files-found: error

.gitignore

@@ -78,3 +78,6 @@ checkstyle-diff.txt
 
 # Java Flight Recorder output (e.g. runJfrProbe default mt-jfr-probe.jfr)
 *.jfr
+
+# Hermes tool cache (agent/tooling state; never version-controlled)
+.hermes/

README.md

@@ -47,15 +47,35 @@ Additional and optional components are in `keyext.*/` folders. The file `build.g
 describing the dependencies and common build tasks for all subprojects.
 
 `key.util`, `key.core` and `key.ui` are the base for the product "KeY Prover". Special care is needed
-if you plan to make changes here.
+if you plan to make changes here. `key.ui.fx` is the JavaFX re-implementation of the user
+interface and the **default entry point** of the application
+(see [key.ui.fx/README.md](key.ui.fx/README.md)); the legacy Swing UI in `key.ui` stays
+available until its retirement decision ([key.ui.fx/SWING-RETIREMENT.md](key.ui.fx/SWING-RETIREMENT.md)).
 
 
 ## Compile and Run KeY
 
 Assuming you are in the directory of this README file, you can create a runnable and deployable version with one of these commands:
 
-1. With `./gradlew key.ui:run` you can run the user interface of KeY directly from the repository. 
-   Use `./gradlew key.ui:run --args='--experimental'` to enable experimental features.
+1. The JavaFX UI is the default way to run KeY's user interface directly from the repository:
+   ```sh
+   ./gradlew :key.ui.fx:run
+   ```
+   This starts `de.uka.ilkd.key.core.fx.MainEx`. Use `./gradlew :key.ui.fx:runExperimental`
+   to enable experimental features. The `key.fx.*` demo/verification system properties,
+   the headless run recipe and the full documentation of the FX UI are in
+   [key.ui.fx/README.md](key.ui.fx/README.md).
+
+   The legacy Swing UI remains available (documented as *legacy*) until its retirement
+   decision ([key.ui.fx/SWING-RETIREMENT.md](key.ui.fx/SWING-RETIREMENT.md)):
+   ```sh
+   ./gradlew key.ui:run --args='--experimental'
+   ```
+   Generic `-DmainClass` ergonomics: the root project's `execute`/`executeInTests` tasks run
+   any main class, e.g. `-DmainClass=de.uka.ilkd.key.core.fx.MainEx ./gradlew :key.ui.fx:execute`
+   (FX) or `-DmainClass=de.uka.ilkd.key.core.Main ./gradlew :key.ui:execute` (legacy Swing).
+   The dedicated `run` tasks are preferred: they set `key.examples.dir` and (for `key.ui.fx`)
+   forward the whitelisted `key.fx.*` properties.
 
 2. Use `./gradlew classes` to compile KeY, which includes running JavaCC and Antlr.
    Likewise, use `./gradlew testClasses` if you also want to compile the JUnit test classes.
@@ -81,6 +101,9 @@ Assuming you are in the directory of this README file, you can create a runnable
    ```
    The file is generated in `key.ui/build/libs/key-*-slim-exe.jar`.
    Both jars are also built as part of `./gradlew assemble`.
+   Note: these tasks package the **legacy Swing** product. The JavaFX UI currently runs via
+   `./gradlew :key.ui.fx:run`; its jlink/jpackage packaging is a later milestone (see the
+   packaging note in [key.ui.fx/README.md](key.ui.fx/README.md)).
 
 5. A distribution is build with
    ```sh

build.gradle

@@ -69,8 +69,8 @@ subprojects {
     version = rootProject.version
 
     java {
-        sourceCompatibility = 21
-        targetCompatibility = 21
+        sourceCompatibility = 25
+        targetCompatibility = 25
     }
 
     repositories {
@@ -109,8 +109,9 @@ subprojects {
     tasks.withType(JavaCompile).configureEach {
         // Setting UTF-8 as the java source encoding.
         options.encoding = "UTF-8"
-        // Setting the release to Java 21
-        options.release = 21
+        // Setting the release to Java 25 (also required by the JavaFX 25 jars, which are
+        // class-file version 67 = JDK 23+)
+        options.release = 25
     }
 
     tasks.withType(Javadoc).configureEach {
@@ -379,9 +380,9 @@ subprojects {
 
 
 tasks.register('start'){
-    description = "Use :key.ui:run instead"
+    description = "Use :key.ui.fx:run (JavaFX UI, default) or :key.ui:run (legacy Swing UI) instead"
     doFirst {
-        println "Use :key.ui:run instead"
+        println "Use :key.ui.fx:run (JavaFX UI, default) or :key.ui:run (legacy Swing UI) instead"
     }
 }
 

gradle/libs.versions.toml

@@ -32,6 +32,14 @@ miglayout = "11.4.3"
 picocli = "4.7.7"
 docking-frames = "1.1.3p1"
 
+# JavaFX user interface (key.ui.fx)
+javafx = "25.0.4"
+richtextfx = "0.11.7"
+openjfx-plugin = "0.1.0"
+
+# Icon fonts (ikonli, kordamp.org/ikonli) — FontAwesome glyphs for the keyext FX ports
+ikonli = "12.4.0"
+
 # External tools
 scala-isabelle = "0.4.5"
 
@@ -80,6 +88,17 @@ miglayout-swing = { module = "com.miglayout:miglayout-swing", version.ref = "mig
 docking-frames-common = { module = "org.key-project:docking-frames-common", version.ref = "docking-frames" }
 docking-frames-core = { module = "org.key-project:docking-frames-core", version.ref = "docking-frames" }
 
+# JavaFX UI components (key.ui.fx)
+richtextfx = { module = "org.fxmisc.richtext:richtextfx", version.ref = "richtextfx" }
+javafx-base = { module = "org.openjfx:javafx-base", version.ref = "javafx" }
+javafx-controls = { module = "org.openjfx:javafx-controls", version.ref = "javafx" }
+javafx-graphics = { module = "org.openjfx:javafx-graphics", version.ref = "javafx" }
+javafx-web = { module = "org.openjfx:javafx-web", version.ref = "javafx" }
+
+# ikonli — FontAwesome icon fonts (see kordamp.org/ikonli), used by the keyext FX ports
+ikonli-javafx = { module = "org.kordamp.ikonli:ikonli-javafx", version.ref = "ikonli" }
+ikonli-fontawesome6 = { module = "org.kordamp.ikonli:ikonli-fontawesome6-pack", version.ref = "ikonli" }
+
 # CLI
 picocli = { module = "info.picocli:picocli", version.ref = "picocli" }
 
@@ -98,4 +117,5 @@ spotless = { id = "com.diffplug.spotless", version.ref = "spotless" }
 checkerframework = { id = "org.checkerframework", version.ref = "checkerframework-gradle" }
 maven-publish = { id = "com.vanniktech.maven.publish", version.ref = "maven-publish" }
 shadow = { id = "com.gradleup.shadow", version.ref = "shadow" }
-license-report = { id = "com.github.jk1.dependency-license-report", version = "3.1.4" }
+license-report = { id = "com.github.jk1.dependency-license-report", version = "3.1.4" }
+openjfx = { id = "org.openjfx.javafxplugin", version.ref = "openjfx-plugin" }