KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

saving proofs for sequent problems #3496

Closed mattulbrich closed 2 months ago

mattulbrich commented 2 months ago

Parsing sequents in \problem{...} has been supported for a while now. This commit adapts the saving routine accordingly.

Related Issue

This is unintentionally reported in #3483. There the actual problem here is shadowed by this problem here.

Intended Change

Currently sequents can be formulated in the \problem section, but cannot be stored.

This fix changes that.

Type of pull request

Ensuring quality

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

codecov[bot] commented 2 months ago

Codecov Report

Attention: Patch coverage is 66.66667% with 1 line in your changes missing coverage. Please review.

Project coverage is 38.10%. Comparing base (dd8d2ef) to head (ea0879b). Report is 5 commits behind head on main.

Files Patch % Lines
.../uka/ilkd/key/proof/io/OutputStreamProofSaver.java 66.66% 0 Missing and 1 partial :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3496 +/- ## ============================================ + Coverage 38.09% 38.10% +0.01% - Complexity 17175 17181 +6 ============================================ Files 2107 2107 Lines 127517 127519 +2 Branches 21436 21437 +1 ============================================ + Hits 48581 48596 +15 + Misses 72950 72940 -10 + Partials 5986 5983 -3 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.