[K-Bug] Cannot generate bison parser or glr-bison parser

Open
#4,678 1 comment 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
3/5
Estimated time
1-2 days
Newbie friendliness
35/100
Issue type
Bug
Clarity
Needs clarification
Activity status
Stale
Domain
compilers

Research direction

Start by running the reported kast parser --gen-glr-parser --sort List --definition $(kdist which circt-semantics.llvm) command after kdist build on macOS. The definition and actual failure details are not included, so capture the parser-generation error and determine whether the command generates a parser or reports a useful semantics problem.

Written by the indexing model from the issue text.

Description

What component is the issue in?

Front-End

Which command
  • kompile
  • kast
  • krun
  • kprove
  • kprovex
  • ksearch
What K Version?

v7.1.163

Operating System

MacOS (Apple Silicon/AMD)

K Definitions (If Possible)

TODO

Steps to Reproduce
kdist build
kast parser --gen-glr-parser --sort List --definition $(kdist which circt-semantics.llvm)
Expected Results

generate parser correctly or tell me what's wrong in my semantics

Dominant language
Python
Stars
591
Forks
163
PR merge metrics
No merged PRs in 30d

Contributor guide

Open the contributing guide

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.

More from runtimeverification/k

All issues in runtimeverification/k

Similar issues

More Python issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.