Implement logging of applied equations as JSON in Kore #3818
Conversation
This file contains hidden or 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
geo2a
force-pushed
the
georgy/simplify-json-kore
branch
from
fdb2a3a to
b1a3c39
Compare
geo2a
force-pushed
the
georgy/simplify-json-kore
branch
from
b1a3c39 to
f05f39d
Compare
geo2a
force-pushed
the
georgy/simplify-json-kore
branch
from
9fcf9cb to
25fd8bd
Compare
|
Subsumed by #3824 |
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.
Fixes #3817
Fixes #3815
Changes to Kore:
Kore.JsonRpc.ServerStatetype to contain an optional handle to write the simplification logs intoKore.Simplify.SimplifyEnvtype to hold an optional handle as well, instead of a boolean flag.Kore.Equation.Application.applyEquation, if the simplified contains the handle, output the trace as JSON into it. Include only the unique ID, not the termsChanges to
Proxy.hsanddev-tools/kore-rpc-dev/Server.hs:-l SimplifyJsonis set, thread the handle tostderr/log file through to Kore'sServerStateProxy.hs, do not modify the request parameters when falling back to Kore or making internal simplify requests. Do not output logs received form Kore at-l SimplifJsonanymore: Kore will now do it itselfNote that the behavior of
kore-rpc-booster -l SimplifyJsonis tested by thebooster/test/rpc-intergration/test-log-simplify-jsonintegration test, which compares the log to a golden file. The changes in this PR do not break this test.