Fix changing Taclet Options via the GUI (and more) + TimSort source files added as examples#3889
Merged
Conversation
When a stub under JavaRedux (or a \bootclasspath/\classpath entry) fails to parse, the whole Java model build aborts. This was reported with a misleading message that blamed an unrelated built-in taclet: the first rule needing a JDK type (e.g. doubleSin, whose \find embeds java.lang.Math.sin) would report "java.lang.Math cannot be found" and point at floatRulesAssumeStrictfp.key, hiding the real parse error in the offending stub. Two causes: * JavaService.parseSpecialClasses set the parsedSpecial flag to true *before* parsing. On failure the flag stayed true, so the half-built Java model was silently marked "done" and reused; every later type lookup then failed with a misleading "cannot be found". Reset the flag on failure and let the real exception (which carries the offending stub's file:line) propagate. * ExpressionBuilder.getJavaBlock wrapped every failure as "Could not parse Java block ...". When the underlying failure is really a boot/library-class parse failure, the modality's Java block is an innocent bystander. Detect that case (a BuildingExceptions whose issues point at real .java/.jml stub files) and surface it directly, so the error names the stub and its position. Creted with support of AI tooling
When an overloaded JML operator has no handler for its operand types,
JmlTermFactory.binary/unary reported the failure by dumping KeY's internal
term representation, e.g.
Cannot resolve JML operation add(right,left) >>> Z(1(#))
(types (type, sort): (\bigint,int) >>> (type, sort): (int,int)).
The raw terms (add(...), Z(1(#))) and the "(type, sort)" dump are meaningless
to users. Pretty-print the operands via LogicPrinter and state the operator and
operand types plainly:
Operator '>>>' is not defined for operands of type '\bigint' and 'int'
(in 'right + left >>> 1').
Creted with support of AI tooling
…d Reload" The error dialog's "Save, Close and Reload" button (EditSourceFileAction) called MainWindow.loadProblem(sourceFile), where sourceFile is the file the error pointed at - typically a .java source reached from a .key problem via \javaSource. Loading that bare source file re-enters KeY without the original problem's \includes, so any user-defined symbol declared there vanishes. A spec that is actually fine then fails on reload with a misleading "Unknown escaped symbol X". Concretely: load a .key problem that \includes a symbols file and \javaSource-es a class whose JML uses those symbols; trigger any spec error; hit "Edit File", change something, "Save, Close and Reload" -> the reload now fails with "Unknown escaped symbol ..." on a symbol that was defined all along. Reload the most-recently-opened problem instead (recorded at load start, so it is still available after a failed load), falling back to the source file only if no recent problem is known. Creted with support of AI tooling
Some JML operators are only defined in certain spec math modes: e.g. `>>>` is
implemented for `int`/`long` (in `spec_java_math`/`spec_safe_math`) but not for
`\bigint`, so in the default `spec_bigint_math` it fails no matter how the
operands are cast - the useful advice is to change the mode, not the operands.
The previous message ("Operator '>>>' is not defined for operands of type
'\bigint' and 'int'") wrongly implied a type fix would help. Now, when the
operator is available in another mode, the message says so:
Operator '>>>' is not defined for operands of type 'int' and 'int' (in 'self.x >>> 1').
The '>>>' operator is not available in the 'spec_bigint_math' spec math mode;
it is available under spec_java_math or spec_safe_math (set as a class or method modifier).
IntegerHandler.supportingModes reports which modes define an operator;
OverloadedOperatorHandler.modeHint turns that into the hint; JmlTermFactory
appends it to the binary/unary error messages.
Creted with support of AI tooling
…et's Java block
A missing \classpath or \bootclasspath directory throws a FileNotFoundException
from JavaService while the Java model is being built lazily during taclet
parsing. getJavaBlock caught it and reported "Could not parse Java block
'{..#lhs=+#e;...}'" against a built-in rule file (e.g. integerRulesCommon.key) -
the concrete, correct reason buried as a nested cause.
Extend the environment-setup detection (previously only unwrapped a library
BuildingExceptions) to also surface an IOException in the cause chain, so the
real message is shown directly:
java.io.FileNotFoundException: The \classpath entry ".../classpath" does not exist.
Creted with support of AI tooling
… the .key file A missing \classpath/\bootclasspath directory was reported without any source location: the GUI dialog showed "Line -1 / Column -1" and "[SOURCE COULD NOT BE LOADED]", so the user could not see which declaration was at fault. Capture the source position of each \classpath/\bootclasspath value while parsing the .key file (FindProblemInformation -> ProblemInformation.pathLocations) and validate the directories' existence eagerly in KeYFile.readClassPath/ readBootClassPath (as readJavaPath already does for \javaSource). The resulting BuildingException now carries an explicit Location, so the error reads e.g. The \classpath entry ".../classpath" does not exist. at .../Sort.key:2:12 and the dialog opens Sort.key at the offending line. Adds a BuildingException(Location, String) constructor for errors that originate at a .key declaration rather than an offending parser token. Creted with support of AI tooling
…aded
Changing a taclet option (e.g. the integer semantics) and reloading kept the old
option. With a proof loaded, SettingsManager.getChoiceSettings hands the Taclet
Options panel a *detached* ChoiceSettings copy initialised from that proof (so
the panel can display the proof's active options). applySettings wrote the edited
choices back into that throwaway copy, so the change never reached
ProofSettings.DEFAULT_SETTINGS - which is exactly what (re)loading a problem reads
to build a new proof (InitConfig.computeDefaults). The edit was silently lost.
Write the applied choices through to the global default settings. Taclet options
are global defaults for new proofs anyway ("Taclet options will take effect only
on new proofs"), so a subsequent reload now builds the proof with the chosen
option. When no proof is loaded the panel already edited the global settings, so
behaviour there is unchanged.
Creted with support of AI tooling
…t rows) After auto mode, the proof tree caught up with many nodes at once (the model is set non-attentive during auto mode) and makeNodeVisible scrolled to the current goal with scrollPathToVisible + validate(). scrollPathToVisible moves the viewport via its blit scroll mode, and validate() only re-lays-out - it does not repaint - so the copied region kept stale pixels: ghost / horizontally shifted rows that only cleared once the user dragged the scrollbar by hand (observed on both the vertical and horizontal scrollbar). Repaint the viewport after the programmatic scroll so the final state is drawn correctly. makeNodeVisible is not on the hot auto-mode path (the model is non-attentive then), so the extra repaint is cheap. Creted with support of AI tooling
unp1
changed the title
unp1
added
🐞 Bug
Error Reporting
When the proof-tree tab is hidden, the view deliberately stops listening, so a proof disposed meanwhile leaves the JTree holding a model of the disposed proof. On the next model swap, JTree.setModel clears the selection, which makes the tree UI measure -- and thereby render -- the old selection paths, crashing in the renderer on Proof.getServices of the disposed proof. Replace the selection model with a fresh one before installing the new tree model: the stale paths are forgotten without ever being rendered, and no selection events are fired.
wadoon
approved these changes
Jul 4, 2026
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.
Related Issue
Not related to a specific issue.
These problems were found while resurrecting the TimSort case study; each is a misleading error message or a load/settings bug encountered along the way.
This PR adds error message improvements, the TimSort case study (loads, but some of the shift rules are not yet ported) and most important a bug fix preventing one to change taclet options in the GUI.
Intended Change
A batch of independent fixes that make KeY's problem-loading errors point at the real cause, plus two GUI correctness fixes. Each is a self-contained commit.
Fix that taclet options cannot be changed via the GUI
ChoiceSettingscopy, so changing e.g. the integer semantics and reloading kept the old option.applySettingsnow writes through to the globalDEFAULT_SETTINGSthat a reload reads.Clearer / correctly-attributed error messages
JavaRedux(or a\bootclasspath/\classpathentry) failed to parse,JavaService.parseSpecialClasseshad already marked the model as parsed, so the half-built model was silently reused and the first taclet needing a JDK type (e.g.doubleSin→java.lang.Math) reported "java.lang.Math cannot be found" against an unrelated rule file. The flag is now reset on failure and the real parse error (with the offending stub's location) is surfaced.JmlTermFactorydumped internal term syntax —Cannot resolve JML operation add(right,left) >>> Z(1(#)) …. It now pretty-prints the operands and states the operator and operand types:Operator '>>>' is not defined for operands of type '\bigint' and 'int' (in 'right + left >>> 1').>>>is defined forint/longbut not\bigint). The message now adds: "…not available in the 'spec_bigint_math' spec math mode; it is available under spec_java_math or spec_safe_math", instead of implying a type fix.\classpath/\bootclasspathno longer blames a taclet. A missing directory threw aFileNotFoundExceptiondeep in lazy model building, reported as "Could not parse Java block '{..#lhs=+#e;...}'" against a built-in rule file. The underlying IO failure is now surfaced directly.\classpath/\bootclasspathtoken position is now captured at parse time and validated eagerly (as\javaSourcealready was), so the message reads "The \classpath entry "…/classpath" does not exist. at …/Sort.key:2:12" and the dialog opens the.keyfile at the offending line.GUI correctness
Type of pull request
Ensuring quality
Additional information and contact(s)
Created with AI tooling support
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.