Skip to content

Update README in Lesson 1.3 - #4805

Merged
automergerpr-permission-manager[bot] merged 4 commits into
runtimeverification:developfrom
ibastys:k-tutorial-dev
May 26, 2025
Merged

Update README in Lesson 1.3#4805
automergerpr-permission-manager[bot] merged 4 commits into
runtimeverification:developfrom
ibastys:k-tutorial-dev

Conversation

@ibastys

@ibastys ibastys commented May 4, 2025

Copy link
Copy Markdown
Contributor

No description provided.

@ibastys

ibastys commented May 4, 2025

Copy link
Copy Markdown
Contributor Author

Line 188: Why are there so many AST representations?

Lines 188-189: Should we mention kore if we cannot give the reader any reference for it? Maybe another flag value is more relevant?

Lines 209-211: I could not find any other reference to inj attribute in the tutorial. Do you know where this is mentioned?

Lines 213-214: I added this sentence, but i am not 100% certain it is true.

Lines 451-452: Compiling with flag --gen-bison-parser or --gen-glr-bison-parser gives an additional warning. Could you say something about it?

Lines 478-502: I didn't get an error when parsing after compilation with bison flags on. When compiling with flag --gen-glr... i get two ASTs, correct?

Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
@mariaKt

mariaKt commented May 21, 2025

Copy link
Copy Markdown
Collaborator

Line 188: Why are there so many AST representations?

There are representations at different levels, that are suited best for different purposes/optimizations. E.g., type/sort inference is easier at a higher level (closer to the definition's original structure). Matching is easier at a lower level, after name mangling. The outputs shown are merely different ways to print an AST (easier to read, easier to debug, convert to a different format as expected by another tool). I don't think there is a need to add any information about this at the tutorial though.

Lines 188-189: Should we mention kore if we cannot give the reader any reference for it? Maybe another flag value is more relevant?

There is an exercise in this tutorial, asking about the KORE representation as well, so it seems to me that when the tutorial was created they thought that KORE was important enough to add at this time. For that reason, I myself would not make the decision to change this, I would like some more input.

Lines 213-214: I added this sentence, but i am not 100% certain it is true.

That is true.

@mariaKt mariaKt left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have suggested some changes in the text, but overall this looks good. Thank you @ibastys .

Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated

@mariaKt mariaKt left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have added a couple of comments (one was already there, but was probably missed due to the conversation being hidden). They are minor and easy to address, so I will approve this now, and feel free to merge after you do so. If there is anything unclear, please let me know.

Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
Comment thread k-distribution/k-tutorial/1_basic/03_parsing/README.md Outdated
@automergerpr-permission-manager
automergerpr-permission-manager Bot merged commit 8be1385 into runtimeverification:develop May 26, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants