A remote KeY api as promised in KeY++

Design Descisions

We use handles to refer to large entities like, KeYEnvironment, Proof, or Node. These handles are called *Id and are aligned hierarchical:
```
EnvironemntId < ProofId < NodeId 
```
If you have a NodeId, you can get a ProofId by calling nodeId.proofId().
We do not use expose any key.core classes. For example, Key's Examples are converted into ExampleDesc for the serialization. Every information holding class ends with Desc.
Given complex arguments (especially optional/nullable parameters) are packed into a class which ends with Params.

TODO

[x] Implement a client in non-java, non-jvm (Python)

Oct 17 '23 14:10 wadoon

For what languages do you want to write a client? What's on your TODO list?

I make a simple one in Python. The Python stubs are mostly generated by using Java Reflection. I am creating a JSON with meta information, markdown and Python classes.

I don't know whether you want a rust client. In general, you need a background thread for reading messages, and a shared map from request ids to wait conditions/locks for block synchronous requests until return value is received.

The Python API is more for testing, I am not planning a production-worthy state.

Do we have a use case? For JVM programs I would still recommend to use KeY directly.

Nov 02 '23 11:11 wadoon