key

key copied to clipboard

KeY proofs cannot be replayed if certain labels are present

5

## Description If certain labels are present on a term and a find-and-add taclet is applied, stored proofs cannot be replayed/loaded. The problem is that the recomputation of the labels...

mattulbrich

Fix for #3501: Decrease log level of duplicate sort warnings

1

## Description This pull request addresses #3501. Since this a warning (or better, lots of them) that potentially confuses the users, this very minor PR decreases the log level from...

WolframPfeifer

Bump the gradle-deps group with 6 updates

2

Bumps the gradle-deps group with 6 updates: | Package | From | To | | --- | --- | --- | | [org.jspecify:jspecify](https://github.com/jspecify/jspecify) | `0.3.0` | `1.0.0` | | [io.github.eisop:checker-qual](https://github.com/eisop/checker-framework)...

dependabot[bot]

Replaces #3491 ## Related Issue This pull request addresses #. ## Intended Change This adds functionality to check a single control-flow trace in KeY, so only one path in the...

lks9

Restoration of the formatter for KEY files

2

Archeology: In the back old days, we reformatted all our KeY files. If you need to restore a branch before that time to bring it on the master, you should...

wadoon

## Description When KeY is started, there are multiple warnings about duplicate sort declarations in the taclet base. While we should get rid of those in the future, they are...

WolframPfeifer

KeY GUI slows down already at proofs of size 10000

1

## Description The proof tree rendering slows down for medium sized proof trees. ## Reproducible always ### Steps to reproduce > What is your expected behavior and what was the...

unp1

Improved treatment of final fields

2

## Intended Change Final fields cannot change their value after a single assignment in the constructor. In the current KeY logic, final fields are treated like normal fields stored on...

mattulbrich

Remove the version lock for JDT in the spotless configurations, b/c the new version can handle all classes w/o error. Also, apply spotless to the code basis. It seems, that...

wadoon

Package structured reworked for sealed packages

1

This brings some clean-ups of the #3451 branch to main, without adding `module-info.java` files. Features * distinct packages for each (gradle) module * fixing service loader files

wadoon