Fixes for minor regressions on main#3844
Merged
Merged
Conversation
A stored settings value may deserialize as Integer or Long depending on its magnitude and the format, but the numeric property converters assumed a fixed boxed type and threw a ClassCastException on the other -- which could crash KeY on startup while loading the settings. Accept any Number instead.
A recent-file entry whose profile name was never set serialized the null value as the string "null"; reloading it then tried to resolve a profile named "null", failed, and showed an error dialog instead of opening the file. Treat a missing profile name (null or the legacy "null" string) as "use the default profile" on load, and stop writing the "null" placeholder when saving.
After a compound macro finished, the status line kept the partial count from the macro's last internal strategy pass (e.g. "Applied 2 rules, 1 goal" even though the macro had closed thousands) instead of the macro's own aggregate. Display the ProofMacroFinishedInfo's aggregate result when a macro completes.
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.
Intended Change
Three small, independent fixes for minor regressions on
main.Startup crash if SMT solver timeout is increased (Integer cannot be cast to class Long) #3833
entry whose profile name was never set had the null value as the string
"null"; reloading it then tried to resolve a profile named"null", failed.A missing profile name is now treated as "use the default profile" on
load, and the
"null"placeholder is no longer written on save.compound macro finished, the status line kept the partial count from the macro's
last internal strategy pass instead of the macro's own aggregate. The
ProofMacroFinishedInfoaggregate is now displayed when a macro completes.Type of pull request
Ensuring quality
(
AbstractPropertiesSettingsTest).Additional information and contact(s)
These fixes were separated out of the multithreading work
(#3842) as standalone,
cherry-pickable commits so they can land on
mainindependently.This PR has been done with AI tooling support.
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.