Create a JSON-RPC for KeY #3303
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Drodt
reviewed
Oct 31, 2023
| ``` | ||
|
|
||
|
|
||
| ### client/sm (`server ~~> client`) |
There was a problem hiding this comment.
I would prefer verbose names. Avoid abbreviations like "sm".
There was a problem hiding this comment.
Yes, something from the beginning.
I am still very unhappy with the client API. It is mainly the progress listener, which is not very good, especially with parallel processes.
...test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java
Outdated
Show resolved
Hide resolved
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. |
wadoon
force-pushed
the
weigl/jsonrpc
branch
from
8e62a0f to
d2dcd70
Compare
wadoon
force-pushed
the
weigl/jsonrpc
branch
from
6887838 to
ae5f215
Compare
* origin/weigl/jsonrpc: (71 commits) Bump com.diffplug.spotless from 6.22.0 to 6.23.0 Bump ch.qos.logback:logback-classic from 1.4.11 to 1.4.12 prepare config using dedicated labels Add a configuration for automatic generation of changelogs by Github Prevent second reading of declarations in KeYUserProblemFile Re-enable check for non-unique taclet names and remove two taclet duplicates Bump org.junit.vintage:junit-vintage-engine from 5.10.0 to 5.10.1 Improve selection consistency in task tree view Undo unrelated change that got checked in. Use selection in task tree view to change chosen problem not mouse events Slight alternative in who selects the first node after loading (should be safer) Remove further unnecessary proof change events Fix (for issue #3347) that node selection gets forgotten when switching between proofs Merge errors spotless and merge errors add throwable adapter running for primitive data types, somethings wrong in de-/serialization more doc and py generation working on a working minimal version Creating an JSON-RPC API ...
* refs/heads/main: (197 commits) reformat files remove unused imports Fixed crash with invalid SMT solver path on start. IsInstalled check for SMT solvers is is now dependet on OS. fix reviewer comments Add key features for the FM tutorial Bump ch.qos.logback:logback-classic in the gradle-deps group Bump ch.qos.logback:logback-classic from 1.5.3 to 1.5.5 Bump org.slf4j:slf4j-api from 2.0.12 to 2.0.13 applying spotless Boyer Moore Majority Vote Added test case for the bugfix Fixes a StackOverflow when pretty printing a taclet updating test case descriptions for error reporting Update dependabot.yml Update dependabot configuration unified naming of operator to "seq_upd". Bump org.ow2.asm:asm from 9.6 to 9.7 reformat after merge fix hashing of set statements and assert statements ... # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java # key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java
…onrpc * refs/remotes/origin/main: (26 commits) Fix comment Fix checkstyle workflow Fix checkstyle workflow Fix merge conflicts & spotless Remove todo Spotless Fix? resolving error Move ParsableVariable to ncore Spotless Spotless Rename AbstractSV to OperatorSV Beautified code Fix settings test for SE Spotless fixes Fix taclet prefix check when parsing Fix taclet equality test Fix parsing of variable conditions Fix errors resulting from changing ParseableVar Delete Legacy Matcher and adapt VM matcher for new Modality operator Fix errors after changing ParsableVars ...
* also fix some encoding in recorder/src files
* weigl/codequality: reenable sonarqube, disable the crappy things adding comments to jml spec factory default contracts EQ version of seqSwapPreservesSeqPerm + proof added rule for sequences: swap preserves perm Fix test case that failed with new default-contract behavior Fix code format Add test Add documentation Add proof setting for sound or unsound default contracts Don't add default contracts for Object or <init> methods Default contract for contractless methods Fix compiler check when using classpath Add printf to JavaRedux
* refs/heads/main: Fix and test goToNext() Fix goToNextSibling() (thx Tobias) Format Add comments and next() method Remove SVSubstitute Clean up inheritance Implement missing methods Start implementation of traversal Implement cursor Increase Java version API design
|
|
# By Mattias Ulbrich (15) and others # Via GitHub (21) and others * origin/main: (36 commits) Bump the github-actions-deps group with 2 updates Bump the gradle-deps group with 5 updates formatting Bump the github-actions-deps group with 2 updates Bump the gradle-deps group with 8 updates spotless generating ProofTree tooltips lazily, options to disable them completely fix for visual bug with overlapping/unreadable text in color settings Fox copyright year Bump the gradle-deps group with 6 updates improving code for heatmap activation applied spotless Missed nonnullness of map keys. type annotations for test cases repairing a nullness type error some more NonNull annotations Adding a test case for immutable maps. extending the nonnull type system to the immutable maps repairing type annotations in key.util ... it compiles again. repairing heatmap updates for inner nodes ... # Conflicts: # .github/workflows/code_quality.yml # build.gradle
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
A remote KeY api as promised in KeY++
Design Descisions
We use handles to refer to large entities like,
KeYEnvironment,Proof, orNode.These handles are called
*Idand are aligned hierarchical:If you have a
NodeId, you can get aProofIdby callingnodeId.proofId().We do not use expose any
key.coreclasses. For example, Key'sExamples are converted intoExampleDescfor the serialization. Every information holding class ends withDesc.Given complex arguments (especially optional/nullable parameters) are packed into a class which ends with
Params.TODO