Skip to content

Interactive Proof Replayer - #3897

Draft
wadoon wants to merge 4 commits into
mainfrom
weigl/p2ps
Draft

Interactive Proof Replayer#3897
wadoon wants to merge 4 commits into
mainfrom
weigl/p2ps

Conversation

@wadoon

@wadoon wadoon commented Jul 6, 2026 •
edited by WolframPfeifer
Loading

Copy link
Copy Markdown
Member

Intended Change

A user interface that allows you to replay stored proofs interactively.

The idea is to (a) allow restoring stored proofs partially, (b) on error try to message your current state into a replayable state (e.g. hide formulas etc.), and (c) restart the proof replay.

image

Feature

  • Load Proofs from file and store them into a data structure
  • Nice beautiful proof tree, similar to the "Proof Tree".
  • Clicking on a tree node allows you to
    • Apply selected rules on the current proof node
    • Apply a sub-tree to a proof node
    • If applied, jump to the (last) corresponding proof node.
  • Applied with success => "green" marked tree node
  • Applied with error => "red" marked tree node
  • Shows stored information of rule application
  • Shows why rule application was not applicable

Type of pull request

  • New feature (non-breaking change which adds functionality)

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
  • I added new test case(s) for new functionality.
  • I have tested the feature as follows: ...
  • I have checked that runtime performance has not deteriorated.
  • For new Gradle modules: I added the Gradle module to the test matrix in
    .github/workflows/tests.yml

@wadoon wadoon added this to the v3.1.0 milestone Jul 6, 2026
@wadoon wadoon added the Feature New feature or request label Jul 6, 2026
@mattulbrich
mattulbrich marked this pull request as draft August 16, 2026 12:09
@mattulbrich

mattulbrich commented Aug 16, 2026

Copy link
Copy Markdown
Member

I converted to draft due to the number of open check boxes.

wadoon and others added 3 commits October 11, 2026 17:16
@wadoon
first attempt
637cfe5 
# Conflicts:
#	key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension
@WolframPfeifer @wadoon
implement 'apply single rule'
f65f7ed
@wadoon
format
29342c2
@wadoon wadoon self-assigned this Oct 11, 2026
@wadoon
Review fixes 2-8 for PR #3897 (interactive proof replayer)
16792a1 
- Mark replayed/failed stored-tree nodes green/red and repaint via the
  tree model; restore the taclet error path (mark red + report instead of
  silently swallowing) (fix 2)
- Guard the AUTOMODE_TIME parser case against a null proof, completing
  the null-proof handling started in the PR (fix 3)
- Guard replaySingleRule against a missing goal/node selection and show
  a dialog instead of NPEing (fix 4)
- Only open the context menu on an actual tree row; ignore right-clicks
  in empty space (fix 5)
- Only copy stored notes onto the replayed node on success, never
  clearing existing notes (fix 6)
- Remove dead code (countNodes, collectRuleApps, tryReplayRuleAtGoal,
  onNodeSelected, write-only proof field, debug System.out) (fix 7)
- Run the replay off the EDT via SwingWorker (SMT solver launches can
  block) and give the two SMT failure modes meaningful messages (fix 8)

Also keeps the (spotless-fixed) project license header in the extension.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@wadoon wadoon

Labels

Feature New feature or request

Projects

None yet

Milestone

v3.1.0

Development

Successfully merging this pull request may close these issues.

3 participants

@wadoon @mattulbrich @WolframPfeifer