search

KeYProject / key

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

Feature: If possible save the last selected node in the proof, to reselect it upon loading. #3324

Closed unp1 closed 8 months ago

unp1 commented 1 year ago

This commit addresses issue #3297.

codecov[bot] commented 1 year ago

Codecov Report

Attention: 40 lines in your changes are missing coverage. Please review.

Comparison is base (ac66700) 37.86% compared to head (638e108) 37.85%.

Files Patch % Lines
...of/io/IntermediatePresentationProofFileParser.java 31.25% 11 Missing :warning:
.../uka/ilkd/key/proof/io/OutputStreamProofSaver.java 25.00% 8 Missing and 1 partial :warning:
...a/ilkd/key/proof/io/IntermediateProofReplayer.java 33.33% 5 Missing and 1 partial :warning:
...e/uka/ilkd/key/proof/io/AbstractProblemLoader.java 37.50% 2 Missing and 3 partials :warning:
...key/proof/io/intermediate/AppNodeIntermediate.java 33.33% 4 Missing :warning:
...ore/src/main/java/de/uka/ilkd/key/proof/Proof.java 0.00% 2 Missing :warning:
...main/java/de/uka/ilkd/key/proof/io/ProofSaver.java 60.00% 2 Missing :warning:
.../main/java/de/uka/ilkd/key/proof/io/AutoSaver.java 0.00% 1 Missing :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3324 +/- ## ============================================ - Coverage 37.86% 37.85% -0.01% - Complexity 16905 16908 +3 ============================================ Files 2055 2055 Lines 125528 125553 +25 Branches 21226 21237 +11 ============================================ + Hits 47525 47528 +3 - Misses 72152 72171 +19 - Partials 5851 5854 +3 ```

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

wadoon commented 11 months ago

Why does this have so many changed files. This should rather be a local feature.

Is it not possible to use the local settings, instead of the proof replayer?

unp1 commented 11 months ago

Why does this have so many changed files. This should rather be a local feature.

The amount of files is just because we need to pass the selected node to the proof saver.

Is it not possible to use the local settings, instead of the proof replayer?

Sadly not as we do no save unique node identifiers in our proofs and the node numbers upon reload may differ (e.g. when the proof was pruned at some point).

wadoon commented 11 months ago

Sadly not as we do no save unique node identifiers in our proofs and the node numbers upon reload may differ (e.g. when the proof was pruned at some point).

Sarah and I have used a slightly different system to identify nodes uniquely. We used the path from root to the node in the same manner as PiO and PiS. See here. Of course, if you apply run-length encoding you can save a lot of entries in the list (mostly zero, and some ones).

unp1 commented 8 months ago

I close this PR as we will fix the issue using #3380