LLM support in key.ui

# Conflicts:
#	settings.gradle

Author: wadoon

key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java

@@ -4,26 +4,25 @@
 package de.uka.ilkd.key.gui.settings;
 
 
-import java.awt.*;
-import java.awt.event.ActionListener;
-import java.io.File;
-import java.util.Arrays;
-import java.util.Collections;
-import java.util.List;
-import java.util.function.Function;
-import javax.swing.*;
-
 import de.uka.ilkd.key.gui.KeYFileChooser;
 import de.uka.ilkd.key.gui.fonticons.FontAwesomeSolid;
 import de.uka.ilkd.key.gui.fonticons.IconFactory;
 import de.uka.ilkd.key.gui.fonticons.IconFontSwing;
-
 import net.miginfocom.layout.AC;
 import net.miginfocom.layout.CC;
 import net.miginfocom.layout.LC;
 import net.miginfocom.swing.MigLayout;
 import org.jspecify.annotations.Nullable;
 
+import javax.swing.*;
+import java.awt.*;
+import java.awt.event.ActionListener;
+import java.io.File;
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.List;
+import java.util.function.Function;
+
 /**
  * Extension of {@link SimpleSettingsPanel} which uses {@link MigLayout} to create a nice
  * three-column view.
@@ -40,19 +39,19 @@ public abstract class SettingsPanel extends SimpleSettingsPanel {
 
     protected SettingsPanel() {
         pCenter.setLayout(new MigLayout(
-            // set up rows:
-            new LC().fillX()
-                    // remove the padding after the help icon
-                    .insets(null, null, null, "0").wrapAfter(3),
-            // set up columns:
-            new AC().count(3).fill(1)
-                    // label column does not grow
-                    .grow(0f, 0)
-                    // input area does grow
-                    .grow(1000f, 1)
-                    // help icon always has the same size
-                    .size("16px", 2)
-                    .align("right", 0)));
+                // set up rows:
+                new LC().fillX()
+                        // remove the padding after the help icon
+                        .insets(null, null, null, "0").wrapAfter(3),
+                // set up columns:
+                new AC().count(3).fill(1)
+                        // label column does not grow
+                        .grow(0f, 0)
+                        // input area does grow
+                        .grow(1000f, 1)
+                        // help icon always has the same size
+                        .size("16px", 2)
+                        .align("right", 0)));
     }
 
     /**
@@ -123,7 +122,7 @@ protected <T> JComboBox<T> createSelection(T[] elements, Validator<T> validator)
      * @return
      */
     protected JCheckBox addCheckBox(String title, String info, boolean value,
-            final Validator<Boolean> validator) {
+                                    final Validator<Boolean> validator) {
         JCheckBox checkBox = createCheckBox(title, value, validator);
         addRowWithHelp(info, new JLabel(), checkBox);
         return checkBox;
@@ -139,7 +138,7 @@ protected JCheckBox addCheckBox(String title, String info, boolean value,
      * @return
      */
     protected JTextField addFileChooserPanel(String title, String file, String info, boolean isSave,
-            final Validator<String> validator) {
+                                             final Validator<String> validator) {
         JTextField textField = new JTextField(file);
         textField.addActionListener(e -> {
             try {
@@ -168,7 +167,7 @@ protected JTextField addFileChooserPanel(String title, String file, String info,
                 fileChooser = KeYFileChooser.getFileChooser("Save file");
                 fileChooser.setFileFilter(fileChooser.getAcceptAllFileFilter());
                 result = fileChooser.showSaveDialog((Component) e.getSource(),
-                    new File(textField.getText()));
+                        new File(textField.getText()));
             } else {
                 fileChooser = KeYFileChooser.getFileChooser("Open file");
                 fileChooser.setFileFilter(fileChooser.getAcceptAllFileFilter());
@@ -188,16 +187,16 @@ protected JTextField addFileChooserPanel(String title, String file, String info,
     /**
      * Adds a new combobox to the panel.
      *
-     * @param title label of the combo box
-     * @param info help text
+     * @param title          label of the combo box
+     * @param info           help text
      * @param selectionIndex which item to initially select
-     * @param validator validator
-     * @param items the items
-     * @param <T> the type of the items
+     * @param validator      validator
+     * @param items          the items
+     * @param <T>            the type of the items
      * @return the combo box
      */
     protected <T> JComboBox<T> addComboBox(String title, String info, int selectionIndex,
-            @Nullable Validator<T> validator, T... items) {
+                                           @Nullable Validator<T> validator, T... items) {
         JComboBox<T> comboBox = new JComboBox<>(items);
         comboBox.setSelectedIndex(selectionIndex);
         comboBox.addActionListener(e -> {
@@ -237,8 +236,8 @@ protected void addTitledComponent(String title, JComponent component, String hel
     }
 
     protected <T> JList<T> addListBox(String title, String info,
-            final Validator<List<T>> validator,
-            List<T> seq, Function<String, T> converter) {
+                                      final Validator<List<T>> validator,
+                                      List<T> seq, Function<String, T> converter) {
         var model = new DefaultListModel<T>();
         model.addAll(seq);
 
@@ -287,7 +286,7 @@ protected <T> JList<T> addListBox(String title, String info,
         btnAdd.addActionListener(addItem);
 
         ActionListener removeItem = e -> {
-            if (list.getSelectedIndex() != -1) {
+            if(list.getSelectedIndex() != -1) {
                 model.removeElementAt(list.getSelectedIndex());
             }
         };
@@ -297,14 +296,14 @@ protected <T> JList<T> addListBox(String title, String info,
     }
 
     protected JTextArea addTextArea(String title, String text, String info,
-            final Validator<String> validator) {
+                                    final Validator<String> validator) {
         JScrollPane field = createTextArea(text, validator);
         addTitledComponent(title, field, info);
         return (JTextArea) field.getViewport().getView();
     }
 
     protected JTextArea addTextAreaWithoutScroll(String title, String text, String info,
-            final Validator<String> validator) {
+                                                 final Validator<String> validator) {
         JTextArea field = createTextAreaWithoutScroll(text, validator);
         addTitledComponent(title, field, info);
         return field;
@@ -319,15 +318,15 @@ protected JTextArea addTextAreaWithoutScroll(String title, String text, String i
      * @return
      */
     protected JTextField addTextField(String title, String text, String info,
-            final Validator<String> validator) {
+                                      final Validator<String> validator) {
         JTextField field = createTextField(text, validator);
         addTitledComponent(title, field, info);
         return field;
     }
 
 
     protected JTextField addTextField(String title, String text, String info,
-            final Validator<String> validator, JComponent additionalActions) {
+                                      final Validator<String> validator, JComponent additionalActions) {
         JTextField field = createTextField(text, validator);
         JLabel label = new JLabel(title);
         label.setLabelFor(field);
@@ -350,18 +349,18 @@ protected JTextField addTextField(String title, String text, String info,
      * text
      * field), otherwise the {@link Validator} will fail.
      *
-     * @param title the title of the text field
-     * @param min the minimum value that can be entered
-     * @param max the maximum value that can be entered
-     * @param step the step size used when changing the entered value using the JSpinner's arrow
-     *        buttons
-     * @param info arbitrary information about the text field
+     * @param title     the title of the text field
+     * @param min       the minimum value that can be entered
+     * @param max       the maximum value that can be entered
+     * @param step      the step size used when changing the entered value using the JSpinner's arrow
+     *                  buttons
+     * @param info      arbitrary information about the text field
      * @param validator a validator for checking the entered values
-     * @param <T> the class of the minimum value
+     * @param <T>       the class of the minimum value
      * @return the created JSpinner
      */
     protected <T extends Number & Comparable<T>> JSpinner addNumberField(String title, T min,
-            Comparable<T> max, Number step, String info, final Validator<Number> validator) {
+                                                                         Comparable<T> max, Number step, String info, final Validator<Number> validator) {
         JSpinner field = createNumberTextField(min, max, step, validator);
         addTitledComponent(title, field, info);
         return field;

keyext.llm/src/main/java/org/key_project/key/llm/LlmClient.java

@@ -1,21 +1,21 @@
-/* This file is part of KeY - https://key-project.org
- * KeY is licensed under the GNU General Public License Version 2
- * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.key.llm;
 
-import java.io.IOException;
-import java.util.ArrayList;
-import java.util.Map;
-import java.util.concurrent.Callable;
-
 import com.google.gson.GsonBuilder;
+import org.apache.hc.client5.http.classic.methods.HttpGet;
 import org.apache.hc.client5.http.classic.methods.HttpPost;
 import org.apache.hc.client5.http.impl.classic.AbstractHttpClientResponseHandler;
 import org.apache.hc.client5.http.impl.classic.HttpClients;
 import org.apache.hc.core5.http.HttpEntity;
 import org.apache.hc.core5.http.ParseException;
 import org.apache.hc.core5.http.io.entity.EntityUtils;
 import org.apache.hc.core5.http.io.entity.StringEntity;
+import org.key_project.util.java.IOUtil;
+import org.slf4j.LoggerFactory;
+
+import java.io.IOException;
+import java.util.List;
+import java.util.Map;
+import java.util.concurrent.Callable;
 
 /**
  *
@@ -24,13 +24,9 @@
  */
 public class LlmClient implements Callable<Map<String, Object>> {
     private final LlmSession llmSession;
-    private final LlmContext context;
-    private final LlmContext.LlmMessage prompt;
 
-    public LlmClient(LlmSession llmSession, LlmContext context, String message) {
+    public LlmClient(LlmSession llmSession) {
         this.llmSession = llmSession;
-        this.context = context;
-        this.prompt = new LlmContext.LlmMessage("user", message);
     }
 
     @Override
@@ -42,13 +38,13 @@ public Map<String, Object> call() throws Exception {
         request.addHeader("Content-Type", "application/json");
         request.addHeader("Accept", "application/json");
 
-        var msg = new ArrayList<>(context.getMessages());
-        msg.add(prompt);
-
         var data = Map.of(
-            "model", llmSession.getModel(),
-            "messages", msg);
-
+                "model", "azure.gpt-4.1-mini",
+                "messages", List.of(
+                        createMessage("system", "Du bist ein hilfreicher Assistent am KIT."),
+                        createMessage("user", "Erkläre das Prinzip der Rayleigh-Streuung indrei Sätzen.")
+                )
+        );
         var gson = new GsonBuilder().create();
         var stringBody = gson.toJson(data);
         request.setEntity(new StringEntity(stringBody));
@@ -58,9 +54,12 @@ public Map<String, Object> call() throws Exception {
         }
     }
 
+    private Map<String, Object> createMessage(String role, String content) {
+        return Map.of("role", role, "content", content);
+    }
+
 
-    private static class GsonHttpClientResponseHandler
-            extends AbstractHttpClientResponseHandler<Map<String, Object>> {
+    private static class GsonHttpClientResponseHandler extends AbstractHttpClientResponseHandler<Map<String, Object>> {
         @Override
         public Map<String, Object> handleEntity(HttpEntity entity) throws IOException {
             String content = null;
@@ -69,8 +68,7 @@ public Map<String, Object> handleEntity(HttpEntity entity) throws IOException {
             } catch (ParseException e) {
                 throw new RuntimeException(e);
             }
-            // LoggerFactory.getLogger(LlmClient.class).error("Could not parse json response
-            // {}",content);
+            //LoggerFactory.getLogger(LlmClient.class).error("Could not parse json response {}",content);
             try {
                 return new GsonBuilder().create().fromJson(content, Map.class);
             } catch (Exception e) {

keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java

@@ -1,13 +1,5 @@
-/* This file is part of KeY - https://key-project.org
- * KeY is licensed under the GNU General Public License Version 2
- * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.key.llm;
 
-import java.awt.event.ActionEvent;
-import java.util.Collection;
-import java.util.List;
-import javax.swing.*;
-
 import de.uka.ilkd.key.core.KeYMediator;
 import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.gui.actions.KeyAction;
@@ -19,26 +11,28 @@
 import de.uka.ilkd.key.gui.settings.InvalidSettingsInputException;
 import de.uka.ilkd.key.gui.settings.SettingsProvider;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
-
 import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
 
+import javax.swing.*;
+import java.awt.event.ActionEvent;
+import java.util.Collection;
+import java.util.List;
+
 /**
  *
  * @author Alexander Weigl
  * @version 1 (11/18/25)
  */
 @KeYGuiExtension.Info(experimental = false, description = "LLM support for KeY")
 public class LlmExtension implements KeYGuiExtension, KeYGuiExtension.ContextMenu,
-        KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel,
-        KeYGuiExtension.MainMenu {
+        KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel, KeYGuiExtension.MainMenu {
     private KeyAction actionStartLlmPromptForCurrentProof;
-    private TabPanel uiPrompt;
+    private TabPanel uiPrompt = new LlmPrompt();
 
     @Override
     public @NonNull List<Action> getContextActions(
-            @NonNull KeYMediator mediator, @NonNull ContextMenuKind kind,
-            @NonNull Object underlyingObject) {
+            @NonNull KeYMediator mediator, @NonNull ContextMenuKind kind, @NonNull Object underlyingObject) {
         return List.of();
     }
 
@@ -59,9 +53,7 @@ public void preInit(MainWindow window, KeYMediator mediator) {
     }
 
     @Override
-    public @NonNull Collection<TabPanel> getPanels(@NonNull MainWindow window,
-            @NonNull KeYMediator mediator) {
-        uiPrompt = new LlmPrompt(window, mediator);
+    public @NonNull Collection<TabPanel> getPanels(@NonNull MainWindow window, @NonNull KeYMediator mediator) {
         return List.of(uiPrompt);
     }