runtimeverification / runtimeverification/haskell-backend

kore simplification logs not using rule labels

Open
#4,122 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
Haskell
Stars
224
Forks
43
PR merge metrics
No merged PRs in 30d

Description

The simplification logs contain rule labels if they exist, or otherwise rule locations, to relate rule IDs to K source code (labels or locations) .
The log lines have shape {context: [..., simplification: <rule hash>, detail], message: <rule label or location>}.

While booster uses rule labels if they exist, simplification logs from kore do not report labels and always use locations. Kore should log the rule label if a rule has a label.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start by locating Kore's simplification logging code and compare its rule-identifier handling with the booster behavior described in the issue. Verify the log context and message use a rule label when one exists and a rule location otherwise; the issue does not name a specific file or test.

Written by the indexing model from the issue text.

Assessment

Tech stack
haskell
Domain
backend, observability
Issue type
Bug
Difficulty
3/5
Estimated time
1-2 days
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
48/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.