Isabelle Translation

[BookWood7th]

Intended Change

Adds a plugin, which allows the user to automatically translate a KeY sequent to an Isabelle theory and run parts of the automation of Isabelle on the translation. As presented at the KeY Symposium 2024

This broadens the automated toolset of KeY users, which allows for more automated proofs.

Type of pull request

• Refactoring (behaviour should not change or only minimally change)
• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code

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 (add user documentation for Isabelle Translation extension key-docs#41).
• I have tested the feature as follows: KeY Test Suite
• I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

Thesis containing additional information (https://publikationen.bibliothek.kit.edu/1000176239)

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

[WolframPfeifer]

@BookWood7th What is the state of this PR? It is still marked as Draft, and out of date with main. If I remember correctly, it should be nearly main-ready. What is still missing?

[BookWood7th]

I am currently updating the branch and applying a workaround for the automation features. Isabelle doesn't always manage to close all instances of the "e" prover it opened during sledgehammering, which causes a buildup of eprover instances running in the background. For now removing this prover from the sledgehammer toolkit should still leave the user with ample reasoning power via the other provers, namely cvc4 verit z3 spass vampire zipperposition.
There are also some minor visual bugs, where the countdown reaches negative numbers for proof searches and the current proof search is not shown as interrupted, but just stops counting down its remaining time.
The extension otherwise remains functional.

[BookWood7th]

There is also still the somewhat strange Git behavior in this PR. The history suggests I deleted the KeYProject main branch. Should this be a new PR or should it be ignored?

[WolframPfeifer]

Thank you for this nice addition to KeY!

I have only two minor points:

1. There are some classes (e.g., ProofApplyUserAction) which have a very generic name, but are Isabelle-specific. Can you please adapt the names?
   (For the handlers, I think it is ok since this way it is immediately visible that they follow the same structure as the SMT handlers.)

2. Bug #3601 also exists for Isabelle, it should be easy to fix, I suggested an idea.

[WolframPfeifer]

Thanks for fixing the undo bug! There is an ongoing discussion on how to best implement the undo operation in #3606, but I think this is a separate point. Since everything works here, it should be merged now.