Repository navigation
A JavaFX UI for KeY - #3993
Draft
wadoon wants to merge 309 commits into
Draft
A JavaFX UI for KeY#3993wadoon wants to merge 309 commits into
wadoon wants to merge 309 commits into
Conversation
…oofManagerF multi-proof state and main window wiring
… the proof status icons + Loaded Proofs view
…P (Swing KeyStroke parity) A file override like 'ctrl pressed F11' previously matched Ctrl+Shift+F11 as well (ModifierValue.ANY fallback), so a slot save stroke also triggered the slot load. JavaFX's own KeyCombination parser uses UP defaults; Swing KeyStrokes require exact modifier match. Compile gate re-run clean after a transient incremental-compile failure.
…to the FX window and hosts the rule-completion registry
…Dialog, LogView) + per-run logback file appender
… View menu log view, uicontrol self test (key.fx.verify.uicontrol)
…tus-line extension button; no FX extension SPI yet)
…F) + hide-package-prefix and origin-tracking toggles
Port of Swing de.uka.ilkd.key.gui.actions.TermLabelMenu (View▸Term Labels:
'Display Term Labels in Formulas' master switch plus one check item per term
label name of the loaded proof, backed by a shared TermLabelVisibilityManager),
of HidePackagePrefixToggleAction (View▸Hide Package Prefix) and of the
OriginTermLabelsExt main-menu items (View▸Origin Tracking▸Toggle Term Origin
Tracking with the Swing reload dialog, executed as quick save + quick load via
QuickSaveF).
SequentViewF receives a minimal marked hook ('// lemmaorigin:'): the printer
is now built with the installed VisibleTermLabels (Swing
SequentView.getVisibleTermLabels), the last clicked position is exposed for
the origin visualizer trigger, and the printed text is readable for the
key.fx.verify.lemmaorigin self test (OriginLabelsF.verify).
Deviations: no tooltips on menu items (JavaFX MenuItem has no tooltip API,
general FX deviation); the Swing bold/italic occurrence styling of the label
items is not ported; 'Highlight Origins' is omitted (gates the not-yet-ported
sequent→source origin highlight); Toggle Term Origin Tracking flips the
setting before the reload so the re-created proof carries the new labels
(in Swing the flip happens after the reload and cannot affect it).
… palette, responsive split, assumes-input logic)
…ew panels with match highlighting
…ply semantics and theme styles
…roofs dockable, multi-proof state) * weigl/ocfx-proofmgmt: key.ui.fx: proofmgmt: forward the proofmgmt self-test flags and theme the proof status icons + Loaded Proofs view key.ui.fx: proofmgmt: Loaded Proofs dockable (TaskTreeF port) with ProofManagerF multi-proof state and main window wiring key.ui.fx: proofmgmt: ProofManagementDialogF (port of the Swing ProofManagementDialog) with ClassTreeF and ContractSelectionPanelF # Conflicts: # key.ui.fx/build.gradle # key.ui.fx/src/main/resources/de/uka/ilkd/key/gui/fx/theme/key-dark.css # key.ui.fx/src/main/resources/de/uka/ilkd/key/gui/fx/theme/key-light.css
…edicate abstraction dialogs Port of the Swing gui/mergerule dialogs to JavaFX: MergeRuleCompletionF (implements the InteractiveRuleApplicationCompletionF seam copied verbatim from the seam branch), MergePartnerSelectionDialogF, MergeProcedureCompletionF, MergeRuleMenuItemF, PredicateAbstractionCompletionF, AbstractDomainElemChoiceF and AbstractionPredicatesChoiceDialogF (+ the help resource of the Swing info panel). The nested predicate-abstraction dialog degrades the JTextPane HTML info panel to plain text (no javafx.web in key.ui.fx).
Port of the Swing gui/join dialogs to JavaFX: JoinDialogF (with DecisionPredicateInputF + InspectorForDecisionPredicatesF and SequentViewerF), JoinActionF as the future context-menu trigger, and JoinMergeVerifyF, the interactive self test for the join AND merge dialog ports (key.fx.verify.joinmerge, forwarded by build.gradle). MainWindowF gets a minimal, marked verify hook plus the TODO-merge registration seam comment. Theme styles for the new dialogs are appended to both key-light.css and key-dark.css.
…ons (deeper candidates via getTacletAppAtAndBelow)
…self test reports after OK)
…ender, cancel) and shows it; hold-classic screenshot mode
…arrangement on the FX thread and persist the cached snapshot if the scene graph is already dying; hook now catches Throwable and traces to stderr
…estructive apply step
…VisualizerF) + node info visualizer registry (NodeInfoVisualizerF) Port of Swing de.uka.ilkd.key.gui.NodeInfoVisualizer (+ NodeInfoVisualizerListener) as the abstract Stage subclass NodeInfoVisualizerF in the new package de.uka.ilkd.key.gui.fx.nodeinfo: the same static instance registry (per proof name and node serial number, SortedSet ordered by long name), register/unregister, hasInstances/getInstances and the registered/unregistered listeners; dispose() unregisters and closes. Deviation: the Swing visualizers are hosted inside the source view frame; the FX port uses free windows owned by the main window (same presentation as ProofDiffFrameF). Port of Swing de.uka.ilkd.key.gui.originlabels.OriginTermLabelVisualizer as OriginTermLabelVisualizerF: head pane with the live node link (selects the node, with the Swing confirmation dialog when another proof is selected; DELETED NODE + unregister when the node vanishes) and proof name; origin tree (term short text left, origin specification type right, tooltip with the origin and the origins of the (former) sub-terms) and the term view printing only the selected formula (TermViewLogicPrinter port: no sequent arrow when a formula is selected) or the whole sequent, with all term labels except the origin labels. Tree selection highlights the term in the view (CSS class origin-visualizer-highlight, Swing orange; appended to both theme stylesheets with existing variables), a click in the view selects the tree row. 'Show Origin' (View▸Origin Tracking; in Swing a sequent context-menu contribution of OriginTermLabelsExt) opens the visualizer for the last clicked sequent view term, walked up to a formula. The key.fx.verify.lemmaorigin self test now also opens/disposes a visualizer and checks the registry semantics. Deviations: HTML tooltips become plain multi-line text; the Swing JSplitPane initial divider location (1.0, tree collapsed) is not reproduced; the rule-app listener of the Swing node link is replaced by the proof-tree listener (same information for the DELETED NODE check).
…proof tree for a node whose sequent prints term labels (the root sequent of a freshly loaded problem has none)
…th the ProblemLoader branch of Swing taskFinishedInternal, WindowUserInterfaceControl.java:236-244)
…tive theme (dark theme fix)
…e whose sequent carries origin labels
… jobs — verify-sweep.sh takes shard arguments (shard1..shard7, ~30-45 min each instead of ~4h sequential; themepersist save+restore share a shard, long/special runs share a shard), workflow matrix fail-fast:false, per-shard log artifacts
…ization) — trigger on push to main/weigl branches scoped to the UI modules + workflow file, 44 parallel jobs (~20 min each, GitHub queues beyond the free concurrency limit), per-flag log artifacts; script reworked to a name->recipe catalog (run single flags locally too)
…chover (README/settings.gradle/build.gradle), Swing retirement checklist (SWING-RETIREMENT.md, plan only), PARITY-SIGNOFF closed, KNOWN-SIMPLIFIED status note, nightly/on-push per-flag UI verify sweep as a GitHub matrix workflow (key.ui.fx/ci/verify-sweep.sh) * weigl/ocfx-wp11-endgame: WP-11: UI verify sweep on push, one matrix job per flag (max parallelization) — trigger on push to main/weigl branches scoped to the UI modules + workflow file, 44 parallel jobs (~20 min each, GitHub queues beyond the free concurrency limit), per-flag log artifacts; script reworked to a name->recipe catalog (run single flags locally too) WP-11: shard the nightly UI verify sweep across seven parallel matrix jobs — verify-sweep.sh takes shard arguments (shard1..shard7, ~30-45 min each instead of ~4h sequential; themepersist save+restore share a shard, long/special runs share a shard), workflow matrix fail-fast:false, per-shard log artifacts WP-11: institutionalize the full per-flag UI verify sweep as a nightly GitHub workflow — key.ui.fx/ci/verify-sweep.sh (Xvfb + software rendering, sequential one-app-at-a-time runs of all 41 verify hooks, real z3 + graphviz + xdotool, FAIL detection per flag, logs as artifacts) + .github/workflows/ui-verify.yml (cron 02:00 UTC + workflow_dispatch) + README pointer WP-11: close PARITY-SIGNOFF — no OPEN/unverified row remains: the last OPENs get explicit final statuses (KeyStroke default wiring RESOLVED via P1 key.fx.verify.shortcuts; symbex source highlights + sequent-hover cross-highlight, info-view stats staleness and the global toolbar dropdown marked deliberate KNOWN-DEFERRED with their source sites; SMT select-menu deferral clearly marked as the WP-7 per-feature deferral); close-out paragraph after the carried-forward list (items resolved vs. deliberate deferrals) + a WP-11 close-out section that references the per-WP evidence logs without claiming the concurrently-running sweep results; KNOWN-SIMPLIFIED gains the ledger-status note (no row OPEN, marker-count table explains the consolidated markers) and links SWING-RETIREMENT.md WP-11: Swing retirement checklist (documented, NOT executed) — factual inventory of what key.ui.fx/keyext.*.fx still compile against from the Swing side (key.ui.fx: 0 Swing imports; keyext.caching.fx: 6 import sites of ProofCachingSettings/CachingException hosted in keyext.caching; keyext.slicing.fx: explicit :key.ui classpath-only dep; all six keyext counterparts ported), the transitive Swing runtime classpath, the shared key.ui/examples asset, and the staged phase 1/2/3 plan with explicit maintainer decision points (2a-2e, 3a-3c); the Swing UI keeps shipping until the phase-3 gate WP-11: FX default switchover in the docs — :key.ui.fx:run (MainEx) is the documented default entry point, key.ui:run demoted to legacy (still available until the retirement decision, key.ui.fx/SWING-RETIREMENT.md); root README/settings.gradle/start-task updated, -DmainClass ergonomics documented; key.ui.fx/README: run-task whitelist documented (53 key.fx.* properties), per-flag headless verify recipe added, the WP-era verify flags added to the main table and autosave/minimizeinteraction moved out of the harness-injected table (whitelisted since dd4afc5)
…panded panels share the area with draggable dividers (was a fixed equal-growth VBox, the TornadoFX original's 'ExpandedDrawerContentArea'); a freshly expanded item starts with an equal share; drawer API moved from raw getChildren() to SplitPane-backed accessors (addItem/removeItem/containsItem/itemCount/itemAt/resync/hostedItems) + expandedCountProperty for the frame host
… — the west drawer, the workspace (sequent) and the east drawer share draggable dividers, so the drawer width is resizable (was a fixed BorderPane left/right placement); dividers adapt when a drawer expands or collapses its last panel (collapsed = button-bar width only)
…tored — DockLayoutStore saves west/east divider fractions in layout.properties (shutdown hook), startup loads them with factory defaults 0.18/0.86; expanded drawers reopen at the last saved position (reviewer request: store the separator position to restore the layout accurately)
…n order (was third, after Proof Tree and Goal List — reviewer request); the drawerlayout self-test expansion assertion follows the new order
…spotlessCheck over all modules) fails on keyext.ui.testgen.fx and the other FX extension ports, which were merged without a spotless pass (the local gate only covered :key.ui.fx)
… were icon-only with a tooltip before (reviewer request; Swing shows the action names when created with longName=true), texts: Open, Reload, Save, Proof Mgmt, Start Auto, Stop Auto, Goal Back, Prune Proof; tooltips keep the static Swing descriptions
…ons (Swing DropdownSelectionButton parity) — the automation dropdown lists the four AUTOMATION_MACROS, main click stops a running automation or runs the selected macro; the SMT dropdown lists the usable solver unions (selecting one also makes it the active solver union), main click launches it on all open goals via SolverListenerF.launchOnProof; the separate Start/Stop toolbar buttons are gone (Swing has none either)
…were anchored top right; reviewer request) — the overlay box is bottom-right aligned and inset above the status bar
…ed "The KeY Project" like the Swing AboutAction message dialog) instead of a notification toast — shows the copyright, the project homepage link and the version (reviewer request)
…ti-row entry labels to the top — the title column keeps its preferred (widest label) width while only the input column shrinks/grows, and labels of taller rows (e.g. "Heatmap Mode") align to the top of the row (reviewer requests)
…highlight ...") becomes the left-aligned subtitle of the panel (was a right-aligned form row under the title); the settings panel subtitle wraps its text now (reviewer request)
… — the panel area ScrollPane uses fitToHeight, so short panels (e.g. Javac Options) stretch to the full viewport height and are no longer cut off (components were unnecessarily hidden by the fixed-height viewport; reviewer request)
…r button — it was shown with PopupWindow.show(Node, x, y) at screen coordinates (0, buttonHeight), i.e. the left top corner of the desktop (reviewer bug report); the side-based show(Node, Side.BOTTOM, 0, 0) is used instead (the plain show(Node) anchor overload no longer exists in JavaFX 25)
…um rule applications (the Swing MaxRuleAppSlider, reviewer request) — position p maps to (p%9+1)*10^(p/9) like the Swing original, tick labels 1..1M, kept in sync with the max-steps spinner; a section separator separates the "JavaDL Options" property group from the max-steps row (visual aids)
…ent" entry at the top of the View menu reselects the sequent dockable in the workspace (the sequent was closable but there was no way to reopen it; reviewer request)
…rame border (was flush against the bottom edge) and the "Ignore other Java files" checkbox aligns with the profile combo in the input column (was in the far-left label column; reviewer request). The profile list itself already contains all resolvers on the classpath (JavaDL, JavaDL+Permissions, Well-Definedness, Information Flow via DefaultProfileResolver services)
…rows vertically with the dialog (the scroll pane stretches its content now; reviewer request)
… — the scroll pane takes all remaining height (was a fixed preferred viewport height; reviewer request)
…w ProofTreeFilterF interface (name/isActive/setActive/exclusivity) with the ViewSettingsFilterF record for boolean ViewSettings-backed filters; the four built-in filters are registered with one add(...) line each in the createBuiltinFilters() registration list and the context-menu toggles (+ the Swing one-node-filter exclusivity) are derived from the list — adding a new filter is now a new class plus one registration line (reviewer request)
…reeVerifyF, DialogsVerifyF, JoinMergeVerifyF, TacletMatchVerifyF (key.ui.fx) and CachingVerifyF, IsabelleVerifyF, SlicingVerifyF, TestgenVerifyF (keyext.*.fx) move from src/main to src/test via git mv (reviewer request: test code must not ship in the normal source directory); MainWindowF invokes them reflectively (runVerifyHarness) and the key.ui.fx run task carries the module's test output plus the four extension modules' new testArtifacts jars, so the key.fx.verify.* flags keep working unchanged
Member
Author
No monitoring is added. To make it safe, I would just say to the agent that it should make it safe. I will copy your commands to opencode. |
…ep's "=1" default — the sweep recipes pass the property as =1 to request the default demo (heap/model_methods/CellTest_callSet.key), the value-as-path form still works (CI sweep: dialogs red since WP-11 with "example not found .../examples/1")
…blank values — the sweep recipe passes -Dkey.fx.verify.joinmerge.maxsteps= (empty) which crashed Integer.parseInt in the field initializer (NumberFormatException, ExceptionInInitializerError; CI sweep joinmerge-gcd red since WP-11)
… selected proof's row appears — a proof load activates the proof before it is registered, so the selection sync at that moment found no row and never retried (the proofmgmt verify then failed "highlighted row is not the selected proof"; red since WP-11)
… item — item 0 is now "Loaded Proofs" which is collapsed by default and the content area hosts only expanded items, so the reorder assertion regressed with the Loaded-Proofs-first order
…efore the legs and opens the taclet dialog off the FX thread safely — the harness's flag change raced the worker's selectedTaclet (the core reads the flag on the calling thread, so the unarmed leg still ran armed) and the leg booleans were crossed (armed passed expectDialog=true, results assigned to the wrong variables); setMinimizeInteraction latch-joins the FX-thread change and the legs read armed=no-dialog&&applied / unarmed=dialog&&!applied. The armed leg then exposed the product bug: WindowUserInterfaceControlF.completeAndApplyTacletMatch constructed the taclet dialog Stage on the calling thread (IllegalStateException off the FX thread) — the construction hops via FxUtil.runAndWait (on-FX callers unchanged, off-FX callers block until the dialog is up); the harness dialog watcher polls Window.getWindows() through callAndWait (FX-restricted in JavaFX 25, an uncaught exception silently killed the daemon watcher)
… verify hook runs in the demo-load callback like the other proof-dependent hooks, so without a demo the app never reaches the exit flow and the recipe's wait runs into the job timeout (45 min hang; exit-code=0 now)
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
2 participants
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.
JavaFX UI for KeY — feature-complete port + reviewer polish
This PR completes the JavaFX migration of the KeY UI (
key.ui.fx+keyext.*.fx) and incorporates the reviewer-visual-test feedback. All 11 work packages are merged; the latest 20 commits fix the CI gate and address the reviewer's issue list, one commit per item.Work packages (WP-1 … WP-11)
SWING-RETIREMENT.md), CI verify sweep (key.ui.fx/ci/verify-sweep.sh+ 44-job push matrix in.github/workflows/ui-verify.yml)Reviewer round (Oct 12–13)
spotlessCheckover all modules green again (the keyext.*.fx ports had missed the format gate).SplitPanes with draggable dividers; multi-panel proportions resizable; divider positions persisted inlayout.propertiesand restored at startup.SplitMenuButtons (SwingDropdownSelectionButtonparity: automation dropdown = the four proof macros, SMT dropdown = the usable solver unions; separate Start/Stop buttons removed, like Swing).DefaultProfileResolverservices).MaxRuleAppSliderparity), section separators, gear menu opens at the button (was: top-left corner of the desktop).ProofTreeFilterFinterface +ViewSettingsFilterF; new filter = new class + oneaddFilter(...)line in the constructor (context menu + exclusivity derived from the list).src/test:ProofTreeVerifyF,DialogsVerifyF,JoinMergeVerifyF,TacletMatchVerifyFand the four extension harnesses no longer ship insrc/main; the app dispatches them reflectively and theruntask carries the test outputs — allkey.fx.verify.*flags unchanged.Quality gates
:key.ui.fx:spotlessApply :key.ui.fx:compileJava :key.ui.fx:test(+ full-repospotlessCheck).CodeQuality(spotless),Tests(module tests), and the UI verify sweep (44 per-flag jobs on push,ubuntu-latest, artifacts per flag).CI sweep greenness (second round,
6469fa9e01)The push sweep surfaced six red flags. Compared against the previous run, five were already red before this round (red since WP-11); only
drawerlayoutwas a regression of the Loaded-Proofs-first order. Fixed one commit each, each verified locally through the real sweep runner first:dialogs— the contract e2e read the property as an example path while the recipes pass=1as a request for the default demo (→examples/1not found);=1/blank now selects the default demo, real paths still override.joinmerge-gcd— the recipe passesmaxsteps=empty, which crashedInteger.parseIntin the harness field initializer; blank/malformed values fall back to the default.proofmgmt-all— a proof load activates the proof before the Loaded Proofs view registers it, so the selection sync found no row and never retried ("highlighted row is not the selected proof");TaskTreeF.addProofre-syncs when the selected proof's row appears.drawerlayout— the reorder assertion used item 0 ("Loaded Proofs", collapsed by default — the content area only hosts expanded items); it now reorders the first expanded item.minimizeinteraction— the harness's flag change raced the worker'sselectedTaclet(the unarmed leg still ran armed) and the leg booleans were crossed; the legs now latch-join the FX-thread flag change and readarmed = no dialog && applied,unarmed = dialog && !applied. This exposed a product bug:WindowUserInterfaceControlF.completeAndApplyTacletMatchconstructed the taclet dialog Stage on the calling thread (a Stage cannot be built off the FX thread) — the construction now hops viaFxUtil.runAndWait(on-FX callers unchanged), and the harness dialog watcher pollsWindow.getWindows()throughcallAndWait(FX-restricted in JavaFX 25).loadingexit— the recipe never passed a demo sequent although the hook runs in the demo-load callback, so the app never reached the exit flow and the job ran into its 45-min timeout; the recipe passes the demo now (locally:exit-code=0, PASS).The windows
key.utilWeakValueInternerTestfailure is a pre-existing flaky concurrency test outside this port's scope (FX sources only); re-run on occurrence.