Skip to content

Conversation

@goodlyrottenapple
Copy link
Contributor

Fixes #3894

@goodlyrottenapple goodlyrottenapple marked this pull request as ready for review June 7, 2024 13:57
Comment on lines +66 to +68
isEmpty DebugAppliedRewriteRules{appliedRewriteRules}
| null appliedRewriteRules = True
| otherwise = False
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is now no way (I think) to filter the message once we already start converting it to LogStr, so we would either have to render it twice, once in the filter (where we could then check if it is empty/null) and second time when we actually want to log it. As this would be inefficient, I've added a type-class function which can be used to control if some kore Entry is just used for context and should thus not be emitted as a message. See occurrences of isEmpty in this PR to see what I mean.

Copy link
Contributor

@geo2a geo2a left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice! I've played around with both booster-dev and kore-rpc-booster and the logging options. The JSON timestamp work as I'd expect.

Copy link
Member

@jberthold jberthold left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM (haven't tested it, though) tested now

@jberthold
Copy link
Member

jberthold commented Jun 11, 2024

While at it, could you please remove the dot from https://github.com/runtimeverification/haskell-backend/pull/3925/files#diff-fdf134fb9c13c1143cd1c9d16f037c810a3f29d61d40c9944b898af886bb61e9R188 so that we can parse the timestamps later?

    let formatString = "%Y-%m-%dT%H:%M:%S%6Q"

The %Q includes its own decimal point if the value is not zero , see https://hackage.haskell.org/package/time-1.14/docs/Data-Time-Format.html

@rv-jenkins rv-jenkins merged commit 73fbce6 into master Jun 11, 2024
@rv-jenkins rv-jenkins deleted the sam/json-logs-timestamp branch June 11, 2024 13:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Consolidate --log-format json and --log-timestamps options

5 participants