runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
444 stars 145 forks source link

More flexible logging options in RPC requests #4209

Open geo2a opened 1 year ago

geo2a commented 1 year ago

In the Haskell team, we're working on providing fine-grained information on when kore-rpc-booster aborts in Booster and reverts to Kore. We will output this information on a per-request basis, as part of the "logs" field.

While for this use-case the current RPC log options are enough, we anticipate the need for additional RPC log options. To reduce friction with other backends (i.e. Maude) in future, we propose a schema change that would make the RPC log options extensible. Since RPC logs are not a part of the core backend functionality, every backend may choose whether or not to implement a particular log option.

Proposed change to request logging params:

Currently:

"log-successful-rewrites": bool, 
"log-failing-rewrites": bool, 
"log-successfule-simplifications": bool, 
"log-failing-simplifications": bool, 
...

After change:

"log-tags": [ "log-xxx-rewrites", "log-yyy-simplifications", ...]

The sister issue in haskell-backend: https://github.com/runtimeverification/haskell-backend/issues/3655

geo2a commented 4 months ago

We have made the decision to remove the logging feature form the KORE RPC protocol. See haskell-backend/docs/logging.md for the new approach.