Add JSON logging to Kore

[geo2a]

Fixes #3817
Fixes #3815

• the Entry type class gets a new oneLineJson method. Log entries will now need to implement this method if they are to be logged as JSON. The default implementation if just the type constructor name.
• The DebugAttemptEquation log entry gets an a oneLineJson implementation that serialised the successful/failed equation applications in the same form as the Booster, i.e. following the RPC log format. The terms are not included to keep the log size manageable.
• The LogSomeAction constructor of the LogType (a filed of KoreLogOptions) is repurposed. Instead of holding one log action, it now holds two, plus a predicate that specifies which log entries to log using which action. Then, the makeKoreLogger1 function uses the selector function to filter the logs, render them with the appropriate rendered (json or standard) and log them using the appropriate log action.
• booster/Server.hs is modified to initialize LogSomeAction with the appropriate log actions. If -l SimplifyJson log level is activated, we enable DebugAttemptEquation and DebugApplyEquation (as before). If --simplification-log-file is passed too, then Kore's simplification will be redirected there, otherwise they will end-up on stderr. Booster's simplilfications behave in the same way.
• Finally, booster/Proxy.hs does not modify the request parameters when falling back to Kore or making internal simplify requests. We do not output logs received form Kore at -l SimplifJson anymore: Kore will now do it itself.

Example

Put simplification logs into a file

kore-rpc-booster def.kore --module DEF --server-port 12341 -l SimplifyJson --simplification-log-file logs.json

Or simply to stderr:

kore-rpc-booster def.kore --module DEF --server-port 12341 -l SimplifyJson

where there will be prepended with [SimplifyJson]

[goodlyrottenapple]

i guess we will want to tweak this in a separate PR to resemble the booster contexts?

[geo2a]

Yes, certainly.

[goodlyrottenapple]

should we have this here? I notice that we still emit stuff like /* T Fn D Spa */ in kore terms. Perhaps once those are removed, we can remove this truncation without things blowing up too much?

[geo2a]

I added the truncation because the golden file got to 140mb... though that was a bit too much to put into git.

[geo2a]

#3823 did not improve matters much unfortunately. I've settled on a slightly longer cutoff of 500 characters.

[goodlyrottenapple]

left a couple of comments, looks good otherwise

[geo2a]

Thanks @goodlyrottenapple! I'll be merging this then.

As we've discussed, we should come up with a minimal test for the JSON logging. I've created an issue #3830.