Skip to content

Weigl/jsonrpc cleaned #3723

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Draft
wadoon wants to merge 64 commits into
base: weigl/jsonrpc
Choose a base branch
from
Draft

Weigl/jsonrpc cleaned #3723

wadoon wants to merge 64 commits into from

Conversation

@wadoon
Copy link
Member

@wadoon wadoon commented Jan 24, 2026

Related Issue

This pull request resolves #.

Intended Change

Plan

  • Implement feature 1
  • Implement feature 2
  • Code cleanup
  • Document the changes

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • Refactoring (behaviour should not change or only minimally change)
  • New feature (non-breaking change which adds functionality)
  • Breaking change (fix or feature that would cause existing functionality to change)
  • There are changes to the (Java) code
  • There are changes to the taclet rule base
  • There are changes to the deployment/CI infrastructure (gradle, github, ...)
  • Other:

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

Additional information and contact(s)

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

Drodt and others added 30 commits February 22, 2024 10:31
@Drodt
Start fix
f683fb5
@Drodt
Generate easier to prove contracts for non-trivial diverges
7472e4a
@Drodt
Merge branch 'main' into fix-29
9b0c1a8
@Drodt
Merge branch 'main' into fix-29
058b2a0
@Drodt
Merge branch 'main' into fix-29
2fdd99f
@Drodt
Merge branch 'main' into fix-29
c66b6e3
@Drodt
Fix merge error
0fcfca3
@Drodt
Check for applicability of Antec-/SuccTaclets in Proof Replay
38058e3
@Drodt
Add test
649b2b1
@dependabot
Bump the gradle-deps group with 4 updates
2ea1714 
Bumps the gradle-deps group with 4 updates: [ch.qos.logback:logback-classic](https://github.com/qos-ch/logback), org.sonarqube, org.javacc.javacc and org.ow2.asm:asm.


Updates `ch.qos.logback:logback-classic` from 1.5.21 to 1.5.23
- [Release notes](https://github.com/qos-ch/logback/releases)
- [Commits](qos-ch/logback@v_1.5.21...v_1.5.23)

Updates `org.sonarqube` from 7.2.0.6526 to 7.2.2.6593

Updates `org.javacc.javacc` from 4.0.1 to 4.0.3

Updates `org.ow2.asm:asm` from 9.9 to 9.9.1

---
updated-dependencies:
- dependency-name: ch.qos.logback:logback-classic
  dependency-version: 1.5.23
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: gradle-deps
- dependency-name: org.sonarqube
  dependency-version: 7.2.2.6593
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: gradle-deps
- dependency-name: org.javacc.javacc
  dependency-version: 4.0.3
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: gradle-deps
- dependency-name: org.ow2.asm:asm
  dependency-version: 9.9.1
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: gradle-deps
...

Signed-off-by: dependabot[bot] <support@github.com>
@dependabot
Bump the github-actions-deps group with 2 updates
94b62fd 
Bumps the github-actions-deps group with 2 updates: [actions/upload-artifact](https://github.com/actions/upload-artifact) and [actions/cache](https://github.com/actions/cache).


Updates `actions/upload-artifact` from 5 to 6
- [Release notes](https://github.com/actions/upload-artifact/releases)
- [Commits](actions/upload-artifact@v5...v6)

Updates `actions/cache` from 4 to 5
- [Release notes](https://github.com/actions/cache/releases)
- [Changelog](https://github.com/actions/cache/blob/main/RELEASES.md)
- [Commits](actions/cache@v4...v5)

---
updated-dependencies:
- dependency-name: actions/upload-artifact
  dependency-version: '6'
  dependency-type: direct:production
  update-type: version-update:semver-major
  dependency-group: github-actions-deps
- dependency-name: actions/cache
  dependency-version: '5'
  dependency-type: direct:production
  update-type: version-update:semver-major
  dependency-group: github-actions-deps
...

Signed-off-by: dependabot[bot] <support@github.com>
@wadoon
Bump the gradle-deps group with 4 updates (KeYProject#3704)
e4bfd43
@wadoon
Bump the github-actions-deps group with 2 updates (KeYProject#3705)
9d922a3
@wadoon
Check for applicability of Antec-/SuccTaclets in Proof Replay (KeYPro…
23bdc37 
…ject#3702)
@mattulbrich
activating an ancient rule for the treatment of exactInstance of null
7e54530
@mattulbrich
remove trailing whitespace
e5853a5
@mattulbrich
Generate easier POs for non-trivial diverges clauses (KeYProject#3430)
37890dd
@wadoon
(Re-)activating an ancient rule for the treatment of exactInstance of…
af4fc7e 
… null (KeYProject#3706)
@wadoon @flo2702
Single file version of smt-solvers.json
31637e8 
* loading of additional config files
* fix migration of config from string to path
* adapt solver configuration to main version
@wadoon @flo2702
adding system property to specify further smt-solvers.json
c58f59e
@wadoon @flo2702
add a proper loading of preambles
2c559e9 
* some handlerOption fixes
@WolframPfeifer @flo2702
make Metal the default LaF, create checkbox for defaultLaFDecorated
4928583
@flo2702
Make Metal default when creating new config
eb3cbbc
@flo2702
Fix formatting
5a359b5
@flo2702 @wadoon
Fix typos in SolverPropertiesLoader
9910926
@wadoon
KeY/JSON config for SMT solvers (KeYProject#3597)
ad77331
@dependabot
Bump the gradle-deps group with 4 updates
d0516d3 
Bumps the gradle-deps group with 4 updates: [ch.qos.logback:logback-classic](https://github.com/qos-ch/logback), [org.junit:junit-bom](https://github.com/junit-team/junit-framework), [org.junit.jupiter:junit-jupiter-engine](https://github.com/junit-team/junit-framework) and [com.gradleup.shadow](https://github.com/GradleUp/shadow).


Updates `ch.qos.logback:logback-classic` from 1.5.23 to 1.5.24
- [Release notes](https://github.com/qos-ch/logback/releases)
- [Commits](qos-ch/logback@v_1.5.23...v_1.5.24)

Updates `org.junit:junit-bom` from 5.14.1 to 5.14.2
- [Release notes](https://github.com/junit-team/junit-framework/releases)
- [Commits](junit-team/junit-framework@r5.14.1...r5.14.2)

Updates `org.junit.jupiter:junit-jupiter-engine` from 5.14.1 to 5.14.2
- [Release notes](https://github.com/junit-team/junit-framework/releases)
- [Commits](junit-team/junit-framework@r5.14.1...r5.14.2)

Updates `com.gradleup.shadow` from 9.3.0 to 9.3.1
- [Release notes](https://github.com/GradleUp/shadow/releases)
- [Commits](GradleUp/shadow@9.3.0...9.3.1)

---
updated-dependencies:
- dependency-name: ch.qos.logback:logback-classic
  dependency-version: 1.5.24
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: gradle-deps
- dependency-name: org.junit:junit-bom
  dependency-version: 5.14.2
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: gradle-deps
- dependency-name: org.junit.jupiter:junit-jupiter-engine
  dependency-version: 5.14.2
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: gradle-deps
- dependency-name: com.gradleup.shadow
  dependency-version: 9.3.1
  dependency-type: direct:production
  update-type: version-update:semver-patch
  dependency-group: gradle-deps
...

Signed-off-by: dependabot[bot] <support@github.com>
@flo2702
Return to Metal as default Look and Feel (KeYProject#3658)
3294576
@wadoon
Bump the gradle-deps group with 4 updates (KeYProject#3712)
9d0379c
@wadoon
some functions for tff
22b3ea5 
# Conflicts:
#	settings.gradle
wadoon and others added 30 commits January 24, 2026 15:47
@wadoon
more doc and py generation
7a2cd37
@wadoon
running for primitive data types, somethings wrong in de-/serialization
e76737d
@wadoon
add throwable adapter
0c07fe4
@wadoon
spotless and merge errors
8ea50ca
@wadoon
fix after refactoring + spotless
5da8944
@wadoon
wip
ef85dbf
@wadoon
start of a simple Java client
d4a6d13
@samysweb @wadoon
- Shutdown Callbacks
a1cdd8c 
- TreeNodeDesc
- Some stabilization of features

# Conflicts:
#	keyext.api/src/main/java/org/keyproject/key/api/StartServer.java
@samysweb @wadoon
Error message for python generation
ac52095
@samysweb @wadoon
Updated library and example
adabd6a
@samysweb @wadoon
Added proof api endpoint
5d25210
@samysweb @wadoon
Attempt at reseting proof control
7212855
@samysweb @wadoon
First (incomplete) working proof management endpoint
7891d2f
@samysweb @wadoon
Updated python client for proof endpoint
ade9b76
@samysweb @wadoon
Improved interface, environment disposal
a8bafa9
@samysweb @wadoon
Fixed JSON type annotation&retrieval
d5e1997
@samysweb @wadoon
Updated json type annotation on codegen/python side
2edb690
@samysweb @wadoon
Merge branch 'steuber/jsonrpc' into weigl/jsonrpc
2ee77a1
@samysweb @wadoon
Configurable Strategy (not Streategy) options for proof auto mode
eeab48e
@samysweb @wadoon
Extracted node description function
bc052de
@samysweb @wadoon
Null serialization (necessary due to python class initialization), no…
0414f48 
…de labels
@wadoon
reformat / remove weakrefs from the data model
2c854a9
@wadoon
fix compile error
cad9502
@wadoon
spotless
c3d287b
@wadoon
fixing the missing javadoc in the api generator
7b42bfa
@wadoon
better documentation
696c5b0
@wadoon
working on documentation, now with json examples
0ac56bd
@wadoon
try to make the documentation better
f74be3c
@wadoon
better documentation
048c811
@wadoon
add a script for reformatting a stack of commits
785f46b
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

6 participants

@wadoon @Drodt @mattulbrich @WolframPfeifer @flo2702 @samysweb