This PR enables the -l SimplifyJson log option in kore-rpc-booster and booster-dev. This option enables structured (as JSON) logging of equation application/failures to apply an equation.
These feature is a reincarnation of the log-*-simplifications request parameter. It has become evident that bundling the logs into the response is a bad idea, as they tend to be very heavy-weight. In this iteration, we change two things:
logs do not contains the states anymore, but only the rule unique IDs and the failure reason (if failed)
logs are written to a file, rather then collected in-memory and returned in the response
Log format
the logs follow the format of the Simplification constructor of the LogEntry datatype from kore-rpc-types. This allows us to shovel both Booster's and Kore's equation application data into the same format that. Here are three examples of a log entries:
Failure in Booster: {"tag":"simplification","result":{"tag":"failure","reason":"RuleNotPreservingDefinedness","rule-id":"d0c635862a74b433473f8d45be9da2608b68fbdcf820aff3a421795196e6070b"},"origin":"booster"}
Success in Booster: [SimplifyJson] {"tag":"simplification","result":{"tag":"success","rule-id":"f310443b160236f56d095576a7500c11d1e98ee7af349b0bbf7a34b5e444d300"},"origin":"booster"}
Success in Kore: {"tag":"simplification","result":{"tag":"success","rule-id":"24f1c49206508c64e029253c37c243d97ca8b3aaea2e4d938380c89870b81955"},"origin":"kore-rpc"}
Note: we do not have a way to get the failures from Kore at that point.
Output to file or stderr
Both kore-rpc-booster and booster-dev now support a new CLI option, --log-file FILENAME. This option only has effect of -l SimplifyJson is supplied too. If both are present, the simplification logs will be written to FILENAME, otherwise they will end-up in stderr.
Note: when written to stderr, the logs are prefixed with [SimplifyJson] to distinguish them from log entries of other types. When writing to a file, this prefix is skipped.
Analysis of logs
These logs are intended for machine, rather direct human consumption. I'm working on a Python tool on top of pyk that would allow transforming these logs into a table. Something along the lines of:
the above entries as are an exert from a table produced from logs of a Kontrol proof. For proof-wide tables to be more useful, we may want to add request IDs.
Summary of changes
This PR enables the
-l SimplifyJsonlog option inkore-rpc-boosterandbooster-dev. This option enables structured (as JSON) logging of equation application/failures to apply an equation.These feature is a reincarnation of the
log-*-simplificationsrequest parameter. It has become evident that bundling the logs into the response is a bad idea, as they tend to be very heavy-weight. In this iteration, we change two things:Log format
the logs follow the format of the Simplification constructor of the
LogEntrydatatype fromkore-rpc-types. This allows us to shovel both Booster's and Kore's equation application data into the same format that. Here are three examples of a log entries:Note: we do not have a way to get the failures from Kore at that point.
Output to file or
stderrBoth
kore-rpc-boosterandbooster-devnow support a new CLI option,--log-file FILENAME. This option only has effect of-l SimplifyJsonis supplied too. If both are present, the simplification logs will be written toFILENAME, otherwise they will end-up instderr.Note: when written to
stderr, the logs are prefixed with[SimplifyJson]to distinguish them from log entries of other types. When writing to a file, this prefix is skipped.Analysis of logs
These logs are intended for machine, rather direct human consumption. I'm working on a Python tool on top of
pykthat would allow transforming these logs into a table. Something along the lines of:the above entries as are an exert from a table produced from logs of a Kontrol proof. For proof-wide tables to be more useful, we may want to add request IDs.