Repository navigation
Conversation
wadoon
force-pushed
the
weigl/llm
branch
2 times, most recently
from
February 1, 2026 21:19
178fa01 to
97a994e
Compare
wadoon
force-pushed
the
weigl/llm
branch
2 times, most recently
from
March 9, 2026 22:35
db12eb5 to
ee22098
Compare
…ontext and tests Rework the keyext.llm chat into a full KeY-Agent: - ExtendedPrompt assembles the request (system prompt, proof context, attachments, capped history, resolved user message) instead of the panel. - AgentLoop drives one turn as a bounded tool-calling loop with ask_user and run_command approval pauses, cancel, and per-turn activity. - PromptResolver resolves $, @, /skill:, /prompt:, /skills and /prompts. - Built-in tools: get_proof_context, list_files, read_file, file_info (read-only, jail-checked, bounded), run_command (blocklist + approval), ask_user (interactive), and use_skill (gated by agentCanUseSkills). - BuiltInMCPClient reads the approval/disabled sets live from settings and no longer mutates them in getTools. - File-backed prompt/skill libraries, autocomplete, rewritten settings UI and thin chat panel; demo scaffolding removed (LlmClient*, DemoMcpTool) and token-leaking loggers stripped from logback.xml. - Fix LlmSettings static-initializer order, the Question wire mapping (SerializedName), McpClientStdio schema conversion, make McpToolProvider public for service loading. - Add keyext.llm to the CI test matrix and a 42-test unit suite (AgentLoop, ShellSafetyPolicy, PromptResolver, LlmContext, tool schema serialization, BuiltInMCPClient, ExtendedPrompt).
The completion providers receive the word behind the trigger character, so the suggestions of the '/' provider (skills, prompts) were filtered with text.startsWith(prefix) against their full label including the leading slash. typing the first letter after '/' therefore emptied the suggestion list and the popup went blank - /skills, /skill: and /prompt: could not be completed or entered. Match commands against the slash-less key and add tests locking in the filtering behavior.
The '/' completion popup consumed the Ctrl+Enter send shortcut whenever it was visible, so messages like '/skills' were 'accepted' and never sent. Modified-Enter now passes the popup through, and pure /skills and /prompts messages are answered locally in the chat (no LLM round-trip required). The skills combobox and the dedicated send button are removed from the KeY-Agent panel: skills are selected per turn via /skill:name and listed via /skills, and Ctrl+Enter is the only way to fire a query.
…nsion Prompt and skill management moves out of the modal dialogs into a new 'Prompts & Skills' section of the LLM settings panel: a generic LibraryEditorPanel provides a table of entries plus an embedded form with New/Save/Delete and immediate persistence. The chat panel's autocomplete 'new prompt…'/'new skill…' actions and the Prompts menu entry now open the settings dialog at the LLM node, and LlmLibraryDialogs is removed. Completion popup fixes: clicking an entry now inserts it (previously only a double click worked), and the popup no longer steals the keyboard focus. New: Ctrl+Space in the chat input expands the / @file / /directive before the caret in place (e.g. $seq becomes the current sequent text); unknown tokens and bare activation directives are left untouched.
The settings dialog tree underneath 'LLM Settings' now contains three leaf
providers: 'Tools' (approval/disablement table, moved out of LlmSettingsUI
into the new LlmToolsPanel), 'Prompts' and 'Skills' (the library editors).
The 'Prompts & Skills' section in LlmSettingsUI is gone.
The tool sets are now applied by the Tools node only; the parent LLM
Settings panel owns the remaining fields. The chat panel routes the
autocomplete and Prompts-menu library entries to the specific node
('new skill...' opens Skills, 'new prompt...' opens Prompts).
Adds smoke tests for the new panels and tree children. Section 9 of
key-agent-doc.md documents the new settings-tree structure.
Adds a drag handle in the bottom-right corner of the completion window (undecorated JWindows cannot be resized by the window manager). Dragging the handle resizes the popup; the chosen size persists while the popup is re-shown for the current input. The handle draws a small corner grip and shows the SE-resize cursor.
The system prompt field in LLM Settings now sizes its height to the line-wrapped content instead of using a fixed five rows, so longer prompts stay visible while editing. Growth is clamped between 4 and 24 rows (the JScrollPane scrolls beyond that) and tracks dialog resizes.
The 'Agent may use skills' checkbox now directly follows 'Allow the agent to ask questions'. The 'Send temperature' checkbox and its value spinner share one row, and the spinner is disabled unless the checkbox is on.
Two new built-in tools that operate on the current proof, executing the
existing proof-script commands through ProofScriptEngine (same machinery
as the 'Apply Script' action):
- tryclose: applies the TryClose macro to the first open goal ('branch'),
all open goals, or a single goal by index; optional step cap and
assertClosed mode. Runs in the current branch by default.
- auto: applies KeY's automatic proof strategy with an arbitrary step
limit (mirrors 'auto N'), optionally on all open goals.
Both tools report how many goals were closed and remain open. Approved by
default; users can move them to 'with approval' or disable them in the
settings Tools panel. Documented in key-agent-doc.md. The argument mapping
is covered by a new headless unit test.
Aligns the module with the KeY relicense (GPL-2.0-or-later) applied by spotless after the branch was rebased; mechanical change only.
The 'Tools', 'Prompts' and 'Skills' panels (and the main 'LLM Settings' panel) now render the regular KeY settings header (bold title + subtitle + separator) like the built-in panels (e.g. 'Appearance & Behaviour'): the library editors extend SimpleSettingsPanel and set their header text. The Skills and Prompts forms use the standard three-column settings layout (label / input / help icon) with explanations behind every field. The skill's 'Allowed tools' whitelist was a multi-select JList and is now a scrollable list of checkboxes. The Tools table keeps only its header and the table is titled 'Tool approval' (no duplicated 'Tools' row).
…x list The 'Allowed tools' whitelist is no longer wrapped in a JScrollPane and its label, checkbox list and help icon are now aligned to the top of the row instead of vertically centered next to the tall list. The 'Enabled' checkbox moves to the top of the form, above Name.
…ing, export/import The inline table + form of the Prompts/Skills settings panels is replaced by a simple vertical list showing name (bold) and description per entry. Entries are selectable; 'New' opens an empty modal dialog with the full edit form, 'Edit' (or a double click) opens it pre-filled, and the library persists on OK. 'Delete' removes the selected entry. 'Export...' writes the whole library to a JSON file, 'Import...' merges one back (existing names are updated, new ones added), which also fixes the earlier 'New does nothing' confusion (there was no visible reaction).
When importing a library file that contains entries whose names already exist, a JOptionPane now asks whether they may be overridden: 'Yes' updates them, 'No' keeps the existing entries and only adds the new ones, 'Cancel' aborts the import entirely. The result dialog reports which entries were skipped and why.
The 'Tools' settings panel no longer uses the checkbox table. Each tool gets its own row: the tool name, a short explanation (from the tool definition), a help icon, and a radio group selecting the permission: Default (auto/ask, depending on the tool), With approval, Without approval (always), or Disabled. The choices map to the mutually exclusive approval/disabled sets in LlmSettings, so a selection normalizes the other sets (matching the previous per-column behavior). BuiltInMCPClient gains getAllTools() returning all tool definitions (including disabled ones, so the UI can re-enable them) with their descriptions and default approval requirements.
- Embed panel, LLM settings and tool-permission screenshots in key-agent-doc.md - Reformat SettingsPanel.java and AbstractPropertiesSettings.java with spotless (fixes the CI formatting check)
docs/LLM-Client-Extended.md documented the removed prototype classes LlmClient/LlmClientExtended (Callable-based, raw JSON maps); rewrite it for the current AgentLoop architecture: session/context state, agent loop and AgentResult variants, HTTP transport, prompt assembly, tool registry and MCP extension points, threading model, persistence, tests. Also fix the storage path in key-agent-doc.md: prompts and skills live in the versioned config directory (~/.key/<version>/llm/...).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Synopsis
PR brings LLM support into KeY: a "KeY-Agent" chat panel, integrated as a dockable tab in the Swing UI and backed by an OpenAI-compatible chat-completions endpoint (default: the KIT service
https://ki-toolbox.scc.kit.edu/v1). The agent can answer questions about the current proof, run proof-script commands and inspect source files via a built-in tool set (MCP), and is configurable through a dedicated settings subtree.Screenshots
The KeY-Agent panel (dockable tab "KeY-Agent", also Proof → LLM → Open LLM prompt / Ctrl+K)
Settings: Options → Settings → "LLM Settings"
Settings: per-tool permissions ("LLM Settings" → "Tools")
Intended Change & Plan
LlmPrompt), chat-completions client, message historylist_files/read_filetools and via@pathinput markup$seqtoken, andget_proof_contexttool<endpoint>/openai/models; available models can be edited and selected per proof/prompt:namemarkup and autocomplete/skill:namemarkup, editable system prompt; a dedicated background-knowledge store is still missingImplemented beyond the original plan
AgentLoop)$,@,/) with Ctrl+Space expansion~/.key/llm/Documentation
key-agent-doc.md— getting started, chat panel, input markup ($/@//), skills & prompts, tools, settings reference; includes the screenshots shown abovedocs/LLM-Client-Extended.md— architecture and API of thekeyext.llmmodule (agent loop andAgentResult, tool/MCP registry, threading model, persistence, extension points)weigl/hugo; the in-app help button links to this page). Note: the site deploys frommaster, so the mkdocs changes there still need to be merged/cherry-picked tomaster.Type of pull request
Ensuring quality
keyext.llm(agent loop, prompt resolution, autocomplete, MCP tool registry, schema serialization, shell safety policy, library editor smoke tests).keyext.llmadded to the unit-test matrix in.github/workflows/tests.yml..github/workflows/tests.yml(keyext.llm).The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.