Proof Slicing is automatical active during loading proofs and macros

[wadoon]

Description

During proof loading/replay and macro application, the Proof Slicing UI is constantly updated.

This might be a potential drawback for performance.

Reproducible

Always

Steps to reproduce

Loading a KeY file with a proof is enough:

Screencast.From.2026-02-10.12-27-57.mp4

What is your expected behavior, and what was the actual behavior?

Slicing, as well as nearly all UI updates, should be paused during proof loading or macro runs for the sake of performance.

[WolframPfeifer]

After looking at the video, I think the reason is that Proof Caching is active, which uses Proof Slicing to find better caching candidates. Caching uses a subsequent relation: sequent S is a subsequent of sequent T iff S has a subset of T's formulas on either/both sides. A cache hit occurs if a subsequent S of the current goal's sequent T is in the cache (i.e., already closed in this or a different proof). However, this can be optimized: S is also a hit if it contains additional formulas not present in T, as long as these have not been used for closing the goal corresponding to S. This is what the proof slicing can check, and therefore it is run during caching.

That is the theory, however, I am not sure about the implementation. I hope that slicing does not run anymore as soon as you disable caching. Also, maybe it would be possible to get rid of a few listeners, at least not update the GUI that often ...

[FliegendeWurst]

I don't think it is related to proof caching, the same would happen with just the slicing extension enabled.

I can certainly reduce the frequency of UI updates, so that the counters will only be updated once the proof finished loading.

[FliegendeWurst]

I have opened #3735 which reduces the UI updates to twice a second (was easier to implement).

For reference, the slicing extension only constructs the dependency graph when loading the proof, it doesn't do any analysis or slicing at that point.