[Bug] [kprove] - Unable to find klabels in syntax priorities statement
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 35/100
- Issue type
- Bug
- Clarity
- Mostly clear
- Activity status
- Stale
- Domain
- compilers
Research direction
Start with the reproducer files test.k and spec-2.k, then run the listed kompile and kprove commands to confirm the delayed missing-production error. Trace how the custom timeUnit tag and +Int priority are handled between compilation and proof parsing; done means the error is reported at kompile time or the proof completes as expected.
Written by the indexing model from the issue text.
Description
K Version
Tell us what version of K you are using.
Example:
% kompile --version
K version: 5.0.0
Build date: Tue Mar 30 23:29:40 UTC 2021
Description
A definition that includes a custom tag for some productions, and then uses them in a syntax priorities statement, is able to kompile fine, but at kprove time it fails to find the labels mentioned in the syntax priorities statement.
Input Files
File test.k:
module TEST
imports INT
configuration <k> .K </k>
syntax Int ::= Int "seconds" [timeUnit]
// ---------------------------------------
rule N seconds => N [macro]
syntax priorities timeUnit > _+Int_
endmodule
File spec-2.k:
requires "test.k"
module VERIFICATION
imports TEST
syntax KItem ::= runLemma ( Int ) | doneLemma ( Int )
rule <k> runLemma(I) => doneLemma(I) ... </k>
endmodule
module SPEC-2
imports VERIFICATION
claim <k> runLemma(3 +Int 7) => doneLemma(10) ... </k>
endmodule
Reproduction Steps
First kompile the definition with the haskell backend, then run the proof:
% kompile test.k --backend haskell
[Warning] Compiler: Could not find main syntax module with name TEST-SYNTAX in
definition. Use --syntax-module to specify one. Using TEST as default.
% kprove spec-2.k
[Error] Outer Parser: Could not find any productions for tag: _+Int_
Source(/home/dev/src/mkr-mcd-spec-pr/test.k)
Location(8,5,8,39)
Expected Behavior
If this should be an error, then it should happen at kompile time. If not, then the proof should go through.
- Dominant language
- Python
- Stars
- 591
- Forks
- 163
- PR merge metrics
- No merged PRs in 30d
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from runtimeverification/k
-
runtimeverification/k#4939 · 1 assignee ·
-
Concolic Explorer Open
Difficulty 5/5 Over a week Newbie friendliness 32/100
runtimeverification/k#4937 ·
-
Difficulty 5/5 Over a week Newbie friendliness 30/100
runtimeverification/k#4936 ·
-
type:epic
runtimeverification/k#4934 · 4 comments · 1 assignee ·
-
runtimeverification/k#4924 · 1 assignee ·
All issues in runtimeverification/k
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
bancolombia/sentinel#23 ·
-
test md OpenCI
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
-
integration:quickjs org:external priority:backlog topic:code-interpreter topic:middleware type:feature
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
langchain-ai/deepagents#6450 ·
-
bug client
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100