From 9e2f95fd9124f555f8521976efaa7efd4bb007e5 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Tue, 18 Aug 2026 19:42:46 +0200 Subject: [PATCH] add key-tau into one runnable thing --- gradle/libs.versions.toml | 7 +++ keyext.api/build.gradle.kts | 6 +- .../org/keyproject/key/api/KeyApiImpl.java | 6 +- .../keyproject/key/api/TermActionUtil.java | 3 +- keyext.web/build.gradle.kts | 17 ++++++ .../key/webui/JsonRpcWebSocketEndpoint.java | 56 ++++++++++++++++++ .../java/org/key_project/key/webui/WebUi.java | 48 +++++++++++++++ .../src/main/resources/static/favicon.png | Bin 0 -> 1571 bytes .../src/main/resources/static/index.html | 52 ++++++++++++++++ settings.gradle.kts | 1 + 10 files changed, 188 insertions(+), 8 deletions(-) create mode 100644 keyext.web/build.gradle.kts create mode 100644 keyext.web/src/main/java/org/key_project/key/webui/JsonRpcWebSocketEndpoint.java create mode 100644 keyext.web/src/main/java/org/key_project/key/webui/WebUi.java create mode 100644 keyext.web/src/main/resources/static/favicon.png create mode 100644 keyext.web/src/main/resources/static/index.html diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index 3825ef30c72..c7f51fa081f 100644 --- a/gradle/libs.versions.toml +++ b/gradle/libs.versions.toml @@ -11,6 +11,8 @@ therapi = "0.15.0" kotlin-gradle-plugin = "2.4.0" dokka = "2.2.0" spotless = "8.7.0" +shadow = "9.4.1" +jetty = "12.1.10" [libraries] kotlin-gradle-plugin = { module = "org.jetbrains.kotlin:kotlin-gradle-plugin", version.ref = "kotlin-gradle-plugin" } @@ -30,3 +32,8 @@ therapi-runtime-javadoc-scribe = { module = "com.github.therapi:therapi-runtime- therapi-runtime-javadoc = { module = "com.github.therapi:therapi-runtime-javadoc", version.ref = "therapi" } clickt = { module = "com.github.ajalt.clikt:clikt", version = "5.1.0" } vanniktech-maven = { module = "com.vanniktech.maven.publish:com.vanniktech.maven.publish.gradle.plugin", version = "0.37.0" } +jetty-server = { module = "org.eclipse.jetty:jetty-server", version.ref = "jetty" } +jetty-ee11-websocket-jakarta-server = { module = "org.eclipse.jetty.ee11.websocket:jetty-ee11-websocket-jakarta-server", version.ref = "jetty" } + +[plugins] +shadow = { id = "com.gradleup.shadow", version.ref = "shadow" } diff --git a/keyext.api/build.gradle.kts b/keyext.api/build.gradle.kts index b4c668779c2..2b461dc61f0 100644 --- a/keyext.api/build.gradle.kts +++ b/keyext.api/build.gradle.kts @@ -17,9 +17,9 @@ dependencies { } api(libs.lsp4j.jsonrpc) - implementation(libs.lsp4j.websocket.jakarta) - implementation(libs.jetty.websocket.javax.server) - implementation(libs.picocli) + api(libs.lsp4j.websocket.jakarta) + api(libs.jetty.websocket.javax.server) + api(libs.picocli) implementation(libs.guava) annotationProcessor(libs.therapi.runtime.javadoc.scribe) api(libs.therapi.runtime.javadoc) diff --git a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java index 68bee186cea..a88df53f4d0 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java @@ -164,12 +164,12 @@ public CompletableFuture script(ProofId proofId, String scriptLi var proof = data.find(proofId); var env = data.find(proofId.env()); var script = ParsingFacade.parseScript(scriptLine); - var pe = new ProofScriptEngine(script); + var pe = new ProofScriptEngine(proof); try { - pe.execute((AbstractUserInterfaceControl) env.getProofControl(), proof); + pe.execute((AbstractUserInterfaceControl) env.getProofControl(), script); return new MacroStatistic(proofId, scriptLine, -1, -1); - } catch (IOException | InterruptedException | ScriptException e) { + } catch (InterruptedException | ScriptException e) { throw new RuntimeException(e); } }); diff --git a/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java b/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java index a5def30d5bb..45ef0dfa81c 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java @@ -21,7 +21,6 @@ import org.key_project.prover.proof.rulefilter.TacletFilter; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; -import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.reflection.ClassLoaderUtil; import org.jspecify.annotations.NonNull; @@ -142,7 +141,7 @@ private int add(TermActionDesc ta) { */ private static ImmutableList removeRewrites( ImmutableList list) { - ImmutableList result = ImmutableSLList.nil(); + ImmutableList result = ImmutableList.nil(); for (TacletApp tacletApp : list) { Taclet taclet = tacletApp.taclet(); result = (taclet instanceof RewriteTaclet ? result : result.prepend(tacletApp)); diff --git a/keyext.web/build.gradle.kts b/keyext.web/build.gradle.kts new file mode 100644 index 00000000000..c083e39f32e --- /dev/null +++ b/keyext.web/build.gradle.kts @@ -0,0 +1,17 @@ +plugins { + id("buildlogic.java-library-conventions") + application + alias(libs.plugins.shadow) +} + +description = "A web interface for KeY" + +application { + mainClass.set("org.key_project.key.webui.WebUi") +} + +dependencies { + implementation(project(":keyext.api")) + implementation(libs.jetty.server) + implementation(libs.jetty.ee11.websocket.jakarta.server) +} \ No newline at end of file diff --git a/keyext.web/src/main/java/org/key_project/key/webui/JsonRpcWebSocketEndpoint.java b/keyext.web/src/main/java/org/key_project/key/webui/JsonRpcWebSocketEndpoint.java new file mode 100644 index 00000000000..295979c3dd1 --- /dev/null +++ b/keyext.web/src/main/java/org/key_project/key/webui/JsonRpcWebSocketEndpoint.java @@ -0,0 +1,56 @@ +package org.key_project.key.webui; + +import jakarta.websocket.OnClose; +import jakarta.websocket.OnError; +import jakarta.websocket.OnOpen; +import jakarta.websocket.Session; +import jakarta.websocket.server.ServerEndpoint; +import org.eclipse.lsp4j.websocket.jakarta.WebSocketLauncherBuilder; +import org.keyproject.key.api.KeyApiImpl; +import org.keyproject.key.api.StartServer; +import org.keyproject.key.api.remoteclient.ClientApi; + +import java.io.IOException; +import java.io.PrintWriter; +import java.util.concurrent.ExecutionException; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Executors; +import java.util.concurrent.TimeUnit; + +/** + * + * @author Alexander Weigl + * @version 1 (11.06.26) + */ +@ServerEndpoint("/ws/jsonrpc") +public class JsonRpcWebSocketEndpoint { + private static final ExecutorService threadPool = Executors.newCachedThreadPool(); + private static final KeyApiImpl keyApi = new KeyApiImpl(); + + @OnOpen + public void onOpen(Session session) throws IOException, ExecutionException, InterruptedException { + session.setMaxIdleTimeout(TimeUnit.HOURS.toMillis(24)); + var launcherBuilder = new WebSocketLauncherBuilder() + .setSession(session) + .traceMessages(new PrintWriter(System.err)) + .validateMessages(true); + + launcherBuilder.configureGson(StartServer::configureJson); + launcherBuilder.setLocalService(keyApi); + launcherBuilder.setRemoteInterface(ClientApi.class); + + final var clientApiLauncher = launcherBuilder.create(); + keyApi.setClientApi(clientApiLauncher.getRemoteProxy()); + //clientApiLauncher.startListening(); + } + + @OnClose + public void onClose(Session session) { + + } + + @OnError + public void onError(Session session, Throwable throwable) { + throwable.printStackTrace(); + } +} diff --git a/keyext.web/src/main/java/org/key_project/key/webui/WebUi.java b/keyext.web/src/main/java/org/key_project/key/webui/WebUi.java new file mode 100644 index 00000000000..95baadd1e55 --- /dev/null +++ b/keyext.web/src/main/java/org/key_project/key/webui/WebUi.java @@ -0,0 +1,48 @@ +package org.key_project.key.webui; + +import org.eclipse.jetty.ee11.servlet.DefaultServlet; +import org.eclipse.jetty.ee11.servlet.ServletContextHandler; +import org.eclipse.jetty.ee11.websocket.jakarta.server.config.JakartaWebSocketServletContainerInitializer; +import org.eclipse.jetty.server.Server; +import org.eclipse.jetty.util.resource.Resource; +import org.eclipse.jetty.util.resource.ResourceFactory; + +public class WebUi { + public static void main(String[] args) throws Exception { + startNetty(); + } + + private static void startNetty() throws Exception { + Server server = new Server(8080); + ServletContextHandler context = new ServletContextHandler(); + context.setContextPath("/"); + + // Static files from classpath + ResourceFactory resourceFactory = ResourceFactory.of(context); + Resource staticResources = resourceFactory.newClassLoaderResource("static"); + if (staticResources == null || !staticResources.exists()) { + throw new IllegalStateException("Classpath resource 'static' not found"); + } + context.setBaseResource(staticResources); + + // Enable Jakarta WebSocket + JakartaWebSocketServletContainerInitializer.configure(context, (servletContext, wsContainer) -> { + wsContainer.setDefaultMaxTextMessageBufferSize(128 * 1024); + wsContainer.addEndpoint(JsonRpcWebSocketEndpoint.class); + }); + + // Serve static files + context.addServlet(DefaultServlet.class, "/"); + server.setHandler(context); + server.start(); + + System.out.println("Server running at http://localhost:8080"); + System.out.println("WebSocket endpoint available at ws://localhost:8080/ws/jsonrpc"); + + var pb = new ProcessBuilder("google-chrome", "--app=http://localhost:8080") + .start(); + System.out.println("You can use: google-chrome --app=http://localhost:8080"); + + server.join(); + } +} diff --git a/keyext.web/src/main/resources/static/favicon.png b/keyext.web/src/main/resources/static/favicon.png new file mode 100644 index 0000000000000000000000000000000000000000..825b9e65af7c104cfb07089bb28659393b4f2097 GIT binary patch literal 1571 zcmV+;2Hg3HP)Px)-AP12RCwC$UE6KzI1p6{F2N z1VK2vi|pOpn{~#djwYcWXTI_im_u^TJgMZ4JMOsSj!0ma>B?-(Hr@X&W@|R-$}W@Z zgj#$x=!~7LGqHW?IO8+*oE1MyDp!G=L0#^lUx?;!fXv@l^6SvTnf^ac{5OurzC#ZMYc20lI%HhX816AYVs1T3heS1*WaWH z%;x>)-J}YB5#CLzU@GBR6sXYrD>Vw(Fmt#|JP;+}<#6b63Ike{Fuo!?M{yEffez;| zp!PfsuaC)>h>-AdbnwN13g*1LowNjT5?+lFVd#9$!8Z9HA|$*6dQ8EHLu}U|obW6f z2%uGv?vr=KNq7YYa2Roj;|zooo<)lf=&2yxM@e`kM$CmCR#x>gI>I|*Ubr({5Y^rb zghxQU22N}F51}^yfDSt786oMTc!W&V;d?76)9KXX1 z+6Okem(d}YXmmOiZq$!IPk5t8nnS{%?+vDFz3BevmFNgpIod~R{>@#@5x9zJKEHLHv!gHeK~n)Ld!M8DB|Kfe%~123&Hz1Z(86nU7*G5chmyDe ziV7$pB7pJ=96hpxHv9rCR29%bLOXlKU<_13_M8x)6;P8E1Kz6G<&P?$P^%c!M5`2` zfY2zg;VK5~^>TJGQzc+33-n~gKt{{of8GzUkWmU110IgI0DLxRIM>0US|TsM=L|@F z0Bun8U!cRB7-2apz=y-7*UxOxz@Z0)@QM)9wSGki1AZ38ceG7Q72z5`i;i=J`ILzL z@iUO?SBBG-0cQuo+an4TsLy-g-x;8P4UVwk|D8{W@U1Zi z!M)+jqy@nQ$p?5tsHp-6J304Q={v-B>66$P0IDx&YT(`IcZ~bZfmn11#rXd7<5s}y zBi9eim&zQc0Dk|2>$bs0PnLmDfMP5lcXRY&cvJ=zKxI^f0%-d$tD!`LBf9^jMSYUA zI8U?CWdY@}cRq6{5~y+)#h1!*-HcGW@+gZ4B};0OnC~`xQOyH19z*TA!!BJ%9s0V3F?CAJ{hTd#*tf+ur-W9MOURF-@B77_-OshsY}6 zOXRY=5%C^*26z?l)1=$bz30!so5tfABdSYzO+H=CpV~aaUefmjvfZ3Ttu9W&W3Iu6 zROlh0MFA5h;my}8lB0tAV-Rvc2Zs_CCSJnx@d`**$idgy-iMob4dJWWw|21b4NB=LfsYp0Aeh{Ov)yztQi;eL4y5 zMi>8^SzKqk8~k?UiQK^^-5d8c%bV?$F8%X~czyiaKCI2=UH + + + + + + + KeY-τ + + + + + + + + + + + + + + + +
+ +
+ + + + diff --git a/settings.gradle.kts b/settings.gradle.kts index ac0d126294a..ff873a57c32 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -4,3 +4,4 @@ plugins { rootProject.name = "key-rpc" include("keyext.api.app", "keyext.api", "keyext.api.doc", "keyext.api.client") +include("keyext.web") \ No newline at end of file