Conversation
anvacaru
left a comment
anvacaru
left a comment
There was a problem hiding this comment.
I suggest splitting the PR and merging only the timestamp now. We can add the node printing once the custom_step harness is updated in pyk.
| ) | ||
|
|
||
| _LOGGER: Final = logging.getLogger(__name__) | ||
| _CONSOLE_LOG_DATETIME_FORMAT: Final = '%Y-%m-%d %H:%M:%S' |
There was a problem hiding this comment.
Consider moving this to a utils.py file so we can reuse it if needed in the future.
This PR adds a new parameter that is passed to custom steps in pyk. Specifically, the `node_id` is passed so that it can be used in downstream custom steps. This is required for a downstream PR in kontrol (runtimeverification/kontrol#1131) that adds the node id to console log cheatcode logging, which is implemented by means of a custom step. This PR will require adjustments in some downstream dependencies as well such as kevm. However, not all downstream dependencies make use of custom steps such as, e.g., wasm-semantics and komet.
|
This feels somewhat messy. The custom step primitive initially didn't have anything to do with the KCFG structure (such as the node id) for some reason, though I can't recall. Is the log that is produced on stderr not enough for teh AI to be able to trace the execution? It prints node ids and timestamps and branching information and everything, so you could just add I won't block merging this, but can you check if the already produced logs are enough? |
3 participants
This PR adds the current datetime & node id to console log cheatcode prints to stdout.
Having the datetime in the output can help figure out how long kontrol took to execute a given piece of code. This is especially useful in print-f style debugging with autonomously inserted console logs by AI. Having the node id helps differentiate between different branches and was a suggestion by @anvacaru .
The console log cheatcode is implemented in kontrol via a custom step. However, custom steps currently do not have access to the current node id. Therefore, this PR requires small upstream changes in pyk and kevm before merging.