Update dependency: deps/haskell-backend_release#4929
Merged
automergerpr-permission-manager[bot] merged 3 commits intoJun 4, 2026
Merged
Conversation
ehildenb
approved these changes
Jun 4, 2026
automergerpr-permission-manager
Bot
merged commit fb2fde2
into
develop
36 of 38 checks passed
automergerpr-permission-manager
Bot
deleted the
_update-deps/runtimeverification/haskell-backend
branch
ehildenb
added a commit
that referenced
this pull request
Jun 5, 2026
~Blocked on: runtimeverification/haskell-backend#4151 ~Blocked on: #4929 Lets pyk request the haskell-backend's per-request log bundle and write it to disk, so downstream can diagnose fallback behaviour per RPC. The request carries the list of log entries to capture and the response returns them in-band; pyk owns the default set and writes each request's bundle to its own file. This pairs with the haskell-backend per-request-rpc branch, which adds the haskell-logging request field ([String]) and the haskell-log-entries response field to the five JSON-RPC endpoints and captures the named entries independently of the server's -l/--log-file configuration. Changes: - BoosterServer now emits the booster-form haskell-log CLI (--log-file FILE, repeated -l ENTRY) via a new overridable _haskell_log_cli_args hook; it previously sent the kore-rpc form (--log, --log-entries A,B), which made kore-rpc-booster exit on a usage error before opening its RPC port. - KoreClient.{execute,implies,simplify,get_model,add_module} take haskell_logging: Iterable[str] | None — the entries to capture for that request — and send it as the haskell-logging wire field (omitted when None); the optional haskell-log-entries bundle is parsed onto every result type, and simplify returns a SimplifyResult (state, logs, haskell_log_entries). - KoreClient.last_request_id exposes the JSON-RPC id of the most recent request issued by the client, used to name each per-request log file. - CTermSymbolic owns the canonical default entry set (HASKELL_LOGGING_ENTRIES), overridable per instance (and through the cterm_symbolic factory) so downstream can tailor it; the on/off flag is threaded through execute/simplify/kast_simplify/implies and KCFGExplore.extend_cterm. - CTermSymbolic takes a haskell_log_dir: when set, every RPC requests the bundle and the entries returned on the response are written to <haskell_log_dir>/<request_id>.jsonl (one JSON value per line, named by request id so concurrent proof workers never collide). - pyk prove --haskell-logging points that sink at <save-directory>/haskell-logs/ (requires --save-directory). Validation: - make -C pyk check clean. - Confirmed against the per-request-rpc backend implementation: it accepts haskell-logging: [String], routes the flat list to both engines (skipping names each does not recognise), tag-matches id-carrying contexts like Rewrite, and returns the captured entries in-band — pyk's default set is fully recognised, no skips. - Integration and regression-new not run locally (the machine's K install is pinned for a benchmark) — relying on CI. --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.