Add Fallback to LogEntry
#3657
Merged
Add Fallback to LogEntry
#3657
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
geo2a
force-pushed
the
georgy/log-term-on-successful-rewrite
branch
from
2e02a73
to
048b328
Compare
jberthold
reviewed
Sep 13, 2023
geo2a
force-pushed
the
georgy/log-term-on-successful-rewrite
branch
from
048b328
to
db8439b
Compare
geo2a
changed the title
Rewrite logs
geo2a
force-pushed
the
georgy/log-term-on-successful-rewrite
branch
from
033fad6
to
fc5aa93
Compare
|
|
geo2a
force-pushed
the
georgy/log-term-on-successful-rewrite
branch
from
fc5aa93
to
209a03f
Compare
Pull-out `Depth` into its own `Kore.JsonRpc.Types.Depth` module
geo2a
changed the title
Rewrite logsFallback to LogEntry
| @@ -46,7 +48,8 @@ data LogRewriteResult | |||
|
|
|||
| data LogEntry | |||
| = Rewrite | |||
| { result :: LogRewriteResult | |||
| { originalTerm :: Maybe KoreJson | |||
There was a problem hiding this comment.
do we need the original term? the intention for the rewrite trace was to be used when debugging proofs with single step turned on in pyk, so we already have the originalTerm anyway.
There was a problem hiding this comment.
Agreed, let's drop it after all.
Comment on lines
61
to
75
| | -- | Indicates a fallback of an RPC-server to a more powerful, but slower backup server, i.e. Booster to Kore | ||
| Fallback | ||
| { originalTerm :: Maybe KoreJson | ||
| -- ^ state before fallback | ||
| , rewrittenTerm :: Maybe KoreJson | ||
| -- ^ state after fallback | ||
| , reason :: Text | ||
| -- ^ fallback reason | ||
| , ruleIds :: NonEmpty Text | ||
| -- ^ rules applied during fallback, the first rule is the one that caused the fallback | ||
| , recoveryDepth :: Depth | ||
| -- ^ depth reached in fallback, must be the same as (length ruleIds) | ||
| , origin :: LogOrigin | ||
| -- ^ proxy server the log was emitted from | ||
| } |
There was a problem hiding this comment.
this looks good. should have all the info we need :)
rv-jenkins
pushed a commit
to runtimeverification/hs-backend-booster
that referenced
this pull request
Sep 27, 2023
…alls back to Kore (#313) Closes #295 Needs runtimeverification/haskell-backend#3657 Note that the `Fallback` entry changes its level of detail in presence of `logSuccessfulRewrites`/logFailedRewrites`: * If only `logFallbacks` is supplied, then the log entry will only contain the pre- and post-state * If `logFailingRewtires` is given too, the log entry will additionally contain the rule id that caused the fallback and the fallback reason * If `logSuccessfulRewrites` is given too, the log entry will additionally contain the the rule log in Kore
jberthold
pushed a commit
that referenced
this pull request
Apr 10, 2024
…alls back to Kore (#313) Closes runtimeverification/hs-backend-booster#295 Needs #3657 Note that the `Fallback` entry changes its level of detail in presence of `logSuccessfulRewrites`/logFailedRewrites`: * If only `logFallbacks` is supplied, then the log entry will only contain the pre- and post-state * If `logFailingRewtires` is given too, the log entry will additionally contain the rule id that caused the fallback and the fallback reason * If `logSuccessfulRewrites` is given too, the log entry will additionally contain the the rule log in Kore
jberthold
pushed a commit
that referenced
this pull request
Apr 10, 2024
…alls back to Kore (#313) Closes runtimeverification/hs-backend-booster#295 Needs #3657 Note that the `Fallback` entry changes its level of detail in presence of `logSuccessfulRewrites`/logFailedRewrites`: * If only `logFallbacks` is supplied, then the log entry will only contain the pre- and post-state * If `logFailingRewtires` is given too, the log entry will additionally contain the rule id that caused the fallback and the fallback reason * If `logSuccessfulRewrites` is given too, the log entry will additionally contain the the rule log in Kore
jberthold
pushed a commit
that referenced
this pull request
Apr 10, 2024
…alls back to Kore (#313) Closes runtimeverification/hs-backend-booster#295 Needs #3657 Note that the `Fallback` entry changes its level of detail in presence of `logSuccessfulRewrites`/logFailedRewrites`: * If only `logFallbacks` is supplied, then the log entry will only contain the pre- and post-state * If `logFailingRewtires` is given too, the log entry will additionally contain the rule id that caused the fallback and the fallback reason * If `logSuccessfulRewrites` is given too, the log entry will additionally contain the the rule log in Kore
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.
This PR modifies the
LogEntrytype inkore-rpc-typesin two ways:origianlTermintoRewritelog entry constructor (and emit Nothing for now in Kore to retain the current behavior. This change is not necessary at the moment, but we may need to log these terms in future.Fallbackconstructor toLogEntryto enablekore-rpc-boosterto emit a trace when it falls back from Booster to Kore.