Skip to content

Conversation

@PiIsRational
Copy link

Intended Change

Changes the saving behaviour of the proof independent settings, to keep settings that are not used by the loading KeY instance.

This also happens to fix a bug that was causing certain settings to not get saved properly when they were not opened
in KeY.

Type of pull request

  • New feature (non-breaking change which adds functionality)
  • Breaking change (fix or feature that would cause existing functionality to change)
  • There are changes to the (Java) code

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I have tested the feature as follows:
    created special settings and compared them to the same settings after saving them back from KeY

Additional information and contact(s)

@WolframPfeifer is involved in this pull request.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@codecov
Copy link

codecov bot commented Dec 15, 2025

Codecov Report

❌ Patch coverage is 28.57143% with 10 lines in your changes missing coverage. Please review.
✅ Project coverage is 47.99%. Comparing base (e5853a5) to head (ba0945c).
⚠️ Report is 12 commits behind head on main.

Files with missing lines Patch % Lines
...ka/ilkd/key/settings/ProofIndependentSettings.java 16.66% 6 Missing and 4 partials ⚠️
Additional details and impacted files
@@            Coverage Diff            @@
##               main    #3700   +/-   ##
=========================================
  Coverage     47.98%   47.99%           
  Complexity    16045    16045           
=========================================
  Files          1683     1683           
  Lines         96046    96053    +7     
  Branches      15388    15390    +2     
=========================================
+ Hits          46091    46097    +6     
  Misses        44683    44683           
- Partials       5272     5273    +1     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:
  • ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.

@WolframPfeifer WolframPfeifer marked this pull request as ready for review January 12, 2026 14:45
@WolframPfeifer WolframPfeifer self-requested a review January 12, 2026 14:46
@WolframPfeifer WolframPfeifer added Feature New feature or request Java Pull requests that update Java code labels Jan 12, 2026
@WolframPfeifer WolframPfeifer added this to the v3.0.0 milestone Jan 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Feature New feature or request Java Pull requests that update Java code

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants