Clarity on tutorial lessons

[ehildenb]

Issues found by the folks going through the tutorial. I short check-list is provided here, more details for each issues are provided in comments.

@dwightguth I've gone through and put (in bold following each bullet point) the things to check for that bullet point.

[geo2a]

Notes

• [x] Lesson 11: I was having a hard time with the exercise after the LESSON-11-C example. I kept getting parsing ambiguity and? in the end, I decided to skip it. Does it actually have a solution? Check that the solution for this exercise exists/works.
• [x] Lesson 13: The first excersise introduces the --search option, but does not mention that the llvm backend does not support it. I suggest mentioning that the definition should be compiled with kompile --backend haskell for the --search option to be usable. By default kompile uses the llvm backend. Specify that you must do kompile --enable-search for search on the LLVM backend.

[ehildenb]

You need to kompile --enable-search --backend llvm to have the binary generated that will do a search on LLVM backend. This should be made clearer.

[rybla]

Some minor notes:

• [x] Lesson 9: Some formatting errors in the table, because of how "paragraphs" within table cells are handled. Check that tables are formatted correctly on github.com and on kframework.org.

• [x] Lesson 9: It would be nice to see example of how the color attribute is used, since its a little unclear if/what the color attribute takes as an arguments (and what are valid colors? I see that certain named colors work). Provide an example the user can run on the command-line with the color attribute.

• [x] Lesson 10: Formatting errors in tables; some of the escaped need double-backslashes. Check formatting of tables on github.com and kframework.org.

• [x] Link to lesson 11 is broken. Check end-of-document links.

• [x] Lesson 11: typo: “provies” => “provides”. Fix.

• [ ] Lesson 12: what a "freezer" is is not clearly explained. Make the link between the user-defined freezers (with manual strictness) and generated ones more explicit, maybe explaining the naming scheme for freezers.

[JKTKops]

• [x] Lesson 10: typo: end => start => end >= start. Fix

• [x] Lesson 11: It's sort of mentioned off-hand, but it might help to state clearly that casts/strict casts are a compile-time feature, while projection casts are a runtime feature that can cause runtime errors. Make explicit that casts/strict casts are for parsing, and projection casts will cause a runtime halt (but nothing at kompile time). Maybe make sure there is an example of such a runtime halt in the exercises.

• [x] Lesson 12: unbalanced paren before the last code block, I'm not sure what was intended there. Fix typo.

• [x] Lesson 13: "be aware" => "remember"? Change wording.

• [x] Lesson 14: isKResult is referred to as builtin, but this can't be the case if we have to define it ourselves. Shouldn't it be that the name isKResult is treated specially? Specify how the KResult sort is the default sort used for heating/cooling when using strict or seqstrict, and that we're overriding the definition of the automatically generated predicate isKResult. Also double-check that we do introduce somewhere the notion of sort predicates isSORT(_) for each sort.

• [x] Lesson 14: "if I wrote" => "if we wrote" [editorial]. Change wording.

• [ ] Although honestly, I'm not sure I see why a basic tutorial needs to explain how seq and seqstrict work under the hood. The old tutorial showed why they are needed and how to use them and then moved on, and I was able to use K for some toy examples easily with just that knowledge. Showing how they work under the hood later would be great, but starting off with the fully desugared rules in a basic tutorial feels like a huge leap. Consider moving the explanation of strict and seqstrict later, after explaining rewrite rules/semantic rule and other simple things?

[RaoulSchaffranek]

Here are some more typos and minor issues I spotted. These are rather low-hanging fruits. I will prepare a PR.

• [x] Lesson 3: Typo, mechinism -> mechanism
• ~~Lesson 3: In the sentence "This is the reason for the requirement that a bracket production have a single non-terminal of the same sort as the production itself." have -> has~~ @JKTKops pointed out to me that have is actually correct here because the phrase is subjunctive.
• [x] Lesson 4: In the sentence "Sometimes priority and associativity proves insufficient to disambiguate a grammar." proves -> prove
• [x] Lesson 5: In the sentence "in which case these directories are prepended on the beginning of the list" on -> to or on -> at
• [x] Lesson 9: comma separated -> comma-separated
• [x] Lesson 10: startin -> starting
• [x] Lesson 12: funtion -> function
• [x] Lesson 12: The Id-production is not marked as a regular-expression: syntax Id ::= "[a-zA-Z_][a-zA-Z0-9_]*" [token] -> syntax Id ::= r"[a-zA-Z_][a-zA-Z0-9_]*" [token]
• [x] Lesson 13: disamiguation -> disambiguation
• [x] Lesson 14: These attribute -> These attributes
• [x] Lesson 14: determinstic -> deterministic
• [x] General: Choose consistently between nonterminal or non-terminal, same for nondeterministic and non-deterministic
• [x] General: left-hand-side and left hand side -> left-hand side, same for right-hand side

What I really like about the tutorial is that it often introduces a topic from the bottom up and then shows how to simplify things. This is, for example, how evaluation orders are introduced. It is much more rewarding for the reader than first presenting the "simple" bits and then claiming, "but wait, there are more complicated cases, and you also need to know about these things under the hood."

[SchmErik]

I submitted https://github.com/kframework/k/pull/2087

I took some notes but I see that a lot of them have been mentioned previously. The only one I have is this:

• [x] Lesson 11: the exercise using strict cast contains an ambiguous grammar so the exercise cannot be run using krun. Either 1) rewrite the examples so they could be run using krun or 2) write in the tutorial indicating that this one is not meant to be run and only kompiled.

[spencerhaoxiao]

• [x] Lesson 1: The link to Instructions on how to build K framework from source should point to the k's Github repo's README instead of the the README on the tutorial pages on kframework.org
• [x] Lesson 6: The lesson-06-b.k file should add requires lesson-06-a.k as the first line.
• [x] Lesson 9: Typo at Line 130 change 'objecte' to 'object'.
• [x] Lesson 12: Line 162 'replaced Ids with NeList{},...' should be changed to 'replaced List with NeList,...'
• [x] Lesson 13: Line 9 and 10, add commas to before and after 'which are not the definition of a function' to make the whole sentence easier to understand.

[calin1304]

• [x] Lesson 11: In the final paragraph of Strict casts shouldn't (I1:Int + I2:Int)::Exp2 choose the second derivation and (I1:Int + I2:int)::Exp choose the first one?
• [x] Lesson 16: Typo in LESSON-16-B-SYNTAX - import ID-SYNTAX instead of imports ID-SYNTAX
• [x] Lesson 16: in LESSON-16-B-SYNTAX function declarations start with fun but in the example program foo.func we are given int foo and int main
• [x] Lesson 16: typo in first paragraph Sert instead of Set
• [x] Lesson 17: languiage instead of language

[mcalancea]

• [x] Lesson 3: This issue.
• [x] Lesson 9: "or you can use the colors attribute to specify a comma-separated list of colors for each non-terminal in the production." => terminal instead of non-terminal here, right?
• [x] Lesson 9: Specifying fewer colors than terminals for the colors attribute crashes with something like /usr/local/bin/kore-print: line 25: 4832 Abort trap: 6 "$@". I guess this can be a bit cryptic so maybe the error can be handled better.
• [x] Lesson 9: What does %c do when it reaches the end of the list? How does %c interact with %r? If %r resets to the default foreground color, that means the current color may no longer be in the list at all, so it's unclear what %c would do.
• [x] Lesson 10: Regarding the paragraph-processing exercise: it's not clear what type of whitespace can be expected. As a general recommendation, I think some exercises would benefit from an example (input/output) pair.
• [ ] Lesson 13: Due to the example grammar in lesson-13-b.k being very simple (addition with concrete values only), some of the heating/cooling rules can be commented out and evaluation would still be correct. Maybe there's an opportunity for an exercise like "extend the grammar such that all given types of rules are necessary for evaluation".
• [x] Lesson 16: lesson-16-b.k instead of lesson-16-a.k.
• [x] General: One of the exercises in Lesson 20 requires the user to test the calculator they've been building along the way with the Haskell Backend. In my case it crashed although it worked as expected for several examples with the LLVM backend. The issue was that, to my surprise, my interpreter wasn't actually deterministic, it often branched and some branches crashed. I wonder what makes the LLVM backend show me the "correct" branch. Also, maybe it makes sense to explicitly recommend to beginners to run programs with --search to ascertain they run deterministically, as to avoid such "silent" branching. Lesson 20 did this indirectly for me but I had to scratch my head for a while.
• [ ] General: I think some exercises warrant example input / example output. I understand some of them are meant to be vague w.r.t how to deal with certain details, which is cool, but if others are unintentional, clarification might help. I mentioned the paragraph exercise in Lesson 10, but there are also the interpreter exercises in Lesson 16.
• [ ] General: Exercises can vary quite a bit in difficulty. Assigning them a rough difficulty estimate (between 1 and 4 stars let's say) might make the process friendlier.

I enjoyed working through the tutorial and look forward to keeping up with the lessons. Big thanks to everyone developing it!

[anvacaru]

• [x] Lesson 4: Small typo in the naming convention of the file which we will name lesson-04-D.k => lesson-04-d.k
• [x] Lesson 5: Exercise 1 has a reference to problem 1 from lesson 1.4, but it should actually reference problem 2 from lesson 1.4
• [x] Lesson 14: " It ought to return true whenever a term should not be heated (because it is a value) and false" => " It ought to return true whenever a term should not be heated (because it is a value) and false"
• [x] Lesson 14: The first final exercise currently refers to LESSON-14-C. Shouldn't it point to LESSON-14-D instead?
• [x] Lesson 19: Typo "there are thre types of breakpoints" => there are three types of breakpoints

[andreiburdusa]

• [x] General: I suggest replacing "Take the solution to problem X" with "Take the solution to Exercise X" because initially I wandered if "problem 2" means the 2nd exercise of the lesson or the 2nd exercise from the Exercises section.
• [ ] General: I agree with Mihai, some exercises were too vague.
• [ ] Lesson 2: The examples work even without the [function] label. Maybe the lesson could explain a bit why it's used or point to another lesson (like Lesson 1.6) where the label is needed.
• [x] Lesson 5: "Modify lesson-02-d.k from lesson 1.2" - Lesson 2 doesn't tell the user to save module LESSON-02-D in a file called lesson-02-d.k (but yes, it's obvious what lesson-02-d.k means)
• [x] Lesson 9: "algorithm that /approximates/ a sound" - Should that be md formatting?
• [x] Lesson 11: "rather, it a runtime check is inserted"
• [x] Lesson 11: "For example, here is an example" sound redundant
• [ ] Lesson 12: lesson-12-c.k should require "lesson-12-a.k"
• [ ] Lesson 12: Is the first "concat" exercise supposed to be about concatenating nonempty lists? If not, Exercise 2 seems to be just a simplified version of it
• [x] Lesson 17: Mention that it's necessary for the <thread> cells to be wrapped inside a <threads> cell

[IljaZakharov]

I appreciate the developers of the tutorial and all contributors to it. It is a straightforward and perfect introduction to K. The first part is pretty simple, and the second one is a bit more difficult. I have the following notes and proposals for the tutorial:

• [ ] There is issue #2365 related to an old Java version. If the K is built with the Java 1.8, which is suggested by the README file, then "kompile" generates a broken parser_PGM link. I propose to add a note that it is safer to use Java 11.
• [ ] Lesson 9 does not contain examples of using "%c" and "%r" expressions. Juan Conjero proposed an excellent example to illustrate their application to non-terminals which helped me understand them better:

syntax Stmt ::= "{" Stmt "}" [color(red), format(%1%i%n%2%d%n%3)] 
                | "{" "}" [color(red), format(%1%2)]
                > right:
                  Stmt Stmt [format(%1%n%2)]
                | "if" "(" Bool ")" Stmt [colors(blue,red,yellow,red), format(%1 %2%c%3%4 %5)]
                | "if" "(" Bool Bool ")" Stmt "else" Stmt [avoid, colors(blue,red,yellow,red,blue), format(%1 %2%c%3 %r%4%5 %6 %7 %8)]
endmodule

• [ ] I needed some hints from colleagues to finish lessons 15 and 16. Many previously introduced concepts are combined in these lessons, and I would suggest adding more examples to illustrate how to use patterns and functions to update maps and lists and fetch compound structures from cells containing them.

[lisandrasilva]

Thanks for this tutorial, it was really helpful to understand the basics of K. Following are some tips that might help on improving it.

• [ ] Lesson 13: add the [bracket] production in order to be able to write more complex expressions and see both heating rules being applied.
• [ ] Lesson 14: "...the rules for heating are expressly written only to apply if the argument of the expression is a value." -> the rules for cooling...
• [ ] Lesson 14: again we should have the [bracket] production. In the nondeterministic evaluation order with the strict attribute, we can only observe 2 possible different behaviors when using the --search if we have expressions like (5 + 3) + (2 + 1), for instance.
• [ ] Lesson 15: It could have another exercise after Exercise 1 asking for testing that the Boolean variable is indeed being reset. The grammar would be extended with a production Stmts for instance and the $PGM configuration variable would have sort Stmts so one can have programs with more than one statement.
• [ ] Lesson 17: typo "simlar" => similar
• [ ] Lesson 17: The $PGM:K doesn't allow to write a program that properly test spawn and join. It should be changed to $PGM:Stmts.
• [ ] Lesson 17: The production "join" Exp ";" should have [strict] and the ";" is not necessary in this production since the sort Stmt already has the semicolon in its productions.
• [ ] Lesson 17: The rule for spawn should have ... before the end of the k cell: <k> spawn { Ss } => NEXTID ...</k>

[yanliu18]

Thanks for the tutorial! It was fun going through them, playing/ experimenting K features with toy examples and incrementally building up bigger codes. Here are some issues or confusions I have run to. Hope they will be helpful for the others.

• [ ] Lesson 1: Building K using maven on MacOS (for me is version 12.2.1), might be encounter a install_name_tool failure (building Haskell Backend module). This could be due to LLVM 13 has an incompatible version of this command. The workaround is to uninstall llvm and reinstall llvm@12 using Homebrew, referred to issue #2988. (One more tip: brew install llvm@12 might suggest you to echo 'export PATH="/usr/local/opt/llvm@12/bin:$PATH"' >> ~/.zshrc. You may not do this, it might causing the problem that you build system cannot find llvm.) After the llvm@12 update, you might also run into an issue where stack fails, refer to this fix.

• [ ] Lesson 4: Associativity. The manual explains well, though there might be too much to remember. The mistake I have made is to define associativity for a group operators with different priorities, e.g., syntax left times div mod plus minus(where times > plus). The expected way should be syntax left times div mod and syntax left plus minus. Refer to this slack thread for more details.

• [ ] Lesson 6: When using builtin INT sort, -2 and +3 are treated as a token. This will result in 1+2 to be parsed as tokens of 1 and +2 instead of an addition expression, thus resulting a parsing error. Referred to issue #2455.

• [ ] Lesson 9: Regarding the color and colors paragraph, since colors gives the color for every terminal, there is no needs to control the curser with %c or %r. And color attribute allows multiple colors to be listed. Thus, suggest edit of this paragraph: “At a more advanced level, ... colors attribute ”, colors => color ; delete "You can essentially...the same color."

• [ ] Lesson 19: The latest version of llvm-backend, has removed interpreter-gdb.py. If the tutorial instruction was followed and the first recommended command was executed, it might cause a problem of no such file or directory problem. The solution worked for me was to follow the second recommended command to disable the security protection by adding set auto-load safe-path / to ~/.gdbinit. You might need to delete the ~/.gdbinit file and redefine it if previous step is not working.

[PetarMax]

• [ ] Lesson 16, Sets: "A set with a variable of sort Set also matches any superset of such a set." Should it be: "A set pattern..." instead?

• [ ] Lesson 16, Sets: "As with map, the elements left over will be bound to the Set variable (or .Set if no elements are left over)." => "As with map, the elements left over (or .Set if no elements are left over) will be bound to the variable of sort Set."

[charala1]

• [ ] The section on colors is not clear about the %c and %r placeholders. Let's add an example
• [ ] The section on code selectors should make it clear that it is meant to be read from source. Critical info is hidden if read from kframework.org on a browser.
• [ ] When reading about isKResult, we suddenly encounter the symbol attribute with no explanation.
• [ ] https://kframework.org/k-distribution/k-tutorial/1_basic/15_configurations/ -- the SUM example uses ellipses which is correct, but would work without them too. Perhaps add a reminder pointing back to https://kframework.org/k-distribution/k-tutorial/1_basic/13_rewrite_rules/ to help the reader "get it".
• [ ] https://kframework.org/k-distribution/k-tutorial/1_basic/15_configurations/ mention somewhere that a cell a implicitly introduces a variable (symbol?) A
• [ ] "If we had declared a cell as <first-number>, then the cell sort name would be FirstNumberCell." --> is that what we'd get if we used <firstNumber> as well?
• [ ] --search doesn't work if the module name includes underscores. See https://runtimeverification.slack.com/archives/C022YGTV4JK/p1656498523114479?thread_ts=1656442281.531069&cid=C022YGTV4JK

[ovatman]

• [ ] Lesson 15: I found it hard to understand what is being requested in Lesson 15's exercise 1 (in terms of syntax). I had a couple of guesses and I tried each of my guesses but it would be really helpful if a syntactical example like "false; 3 / 5 reset; -7 / -2" is provided for the exercise.
• [ ] Lesson 19: In Lesson 19 example lesson-19-b.k putting a breakpoint at line 9 didn't work for me. All the other examples were okay but when I tried to put a breakpoint at line 9, I didn't get the expected input; instead the run just finished without breaking. It might be my mistake though I tried to follow the provided example as much as possible.
• [ ] General: It might be very useful to warn trainees that there needs to be white-space between operators and operands (i.e. instead of '2+5' you need to write '2 + 5'). It makes more sense as you go along the tutorial; but in the beginning, when you quickly write krun -cPGM='2+5', it wastes too much time to understand why it doesn't work.

[fiedlr]

Thanks for the tutorial, it's a great piece of writing for the fact that K is not the easiest thing to learn. A couple of thoughts:

• [x] Lesson 2: I missed seeing mention of the --definition flag because the tutorials often worked with multiple definitions. The tutorial said we would come to this later but it was quite handy to know before. I guess the tutorial meant the Modules Lesson, but --definition is often much faster than to have a central module and import everything every time.
• [x] Lesson 4: lesson-04-d.k has && and | instead of ||, which is used in the rest of tutorial (inconsistency)
• [x] Lesson 4: I would drop "Write these priority and associativity declarations both inline and explicitly." and let the reader guess if the inline definition suffices and check for themselves.
• [x] Lesson 4: It might be useful to mention the difference between “ABB” and “A” “B” B”. The following grammar is formally ambiguous but looks totally OK to the parser because of how it understands tokens:

  syntax Expr ::= "a" Expr "b"
            | "abb"
            | "b"

  "abb" can be parsed in two different ways, with the token "abb" or with a sequence of tokens "a" "b" "b". It can lead to problems when one is not aware of it in some more complicated example.

• [x] Lesson 5. LESSON-05-D-2 => LESSON-05-D?
• [ ] Lesson 6. I would flip Ex 2 and Ex 3 because Ex 1 deals with division, so it'd be nice to have them together.
• [x] Lesson 6. Very fun exercises if one tries to avoid using Boolean functions from domains.md. I suggest putting Ex2 without built-in Boolean functions into Exercises in Lesson 7, when one learns about the side conditions and order of evaluation so that it can be correct. For example,

  A == A => true
  _A == _B => false [owise]

  Now assuming you can only use built-in Integer functions, A < B is fun to implement.

• [x] Lesson 8. As @charala1 pointed out, this exercise should have a link "Download this tutorial and read it as markdown" pointing to the file. E.g., after reading Compile this file I had to go looking for it on GitHub.
• [x] Lesson 9 typo: In practice, _un_parsing is not always precisely reversible => In practice, parsing is not always precisely reversible (we want to reverse parsing ~ unparse, not reverse unparsing ~ parse, right?)
• [ ] Lesson 9: I must agree with others that %c is not very well explained, I needed to experiment with it to see how it works. An example would be useful.
• [x] Lesson 12: I would put Parsing Syntactic Lists in Programs before the exercise with concat, because how would we test concat without this?
• [x] Lesson 13: ... , but when a definition is compiled,... => ... . When a definition is compiled, ...
• [ ] Lesson 13: When I first saw this, I felt like why do it this way? Might add some additional motivation, at least on an intuitive level. When we start working with the "IMP" language, advantages become much more evident.
• [ ] Lesson 13: The integer subtraction exercise is kind of dull because one can just copy&paste addition and replace the operator.. How about something else, like implementing a ternary operator ? :? It would be more informative.
• [x] Lesson 14: Ex. 2: Says remove eval from lesson 1.11 problem 2. But this evaluator actually works without eval. So it might be better actually to just say rework the evaluator to use seqstrict or something like that.
• [ ] Lesson 14: I agree with others that it's quite advanced to cover how seqstrict works under the hood. I'm not sure if all the talk about contexts is that necessary. Wouldn't it be better just to say arguments are evaluated strict in ltr manner by heating and cooling back to their original places? This is how a human remembers it intuitively anyway.
• [x] Lesson 15: Consider the following definition which is equivalent to the one in LESSON-15-B (lesson-15-c.k) => Consider the following definition (lesson-15-c.k) which is equivalent to the one in LESSON-15-B.
• [x] Lesson 15: Ex1: As @lisandrasilva pointed out, the syntax is not very well accustomed to testing that reset ; works. It'd be good to add an exercise to do this along with instructions to modify the syntax.
• [ ] Lesson 16: A List pattern in K consists of zero or more list elements (as represented by the ListItem symbol), followed by zero or one variables of sort List, followed by zero or more list elements. => just add an example.
• [ ] Lesson 16 last Exercise with function scopes (labeled Ex 1): I felt like this might be a significant increase in difficulty compared to previous exercises. I would split it into several exercises so that the reader is less overwhelmed.
• [x] Lesson 19: First, make sure you have not passed -O1, -O2, or -O3 to kompile. Second, simply add the command line flags -ccopt -g -ccopt -O1 to kompile. Is the first sentence necessary? I would just say run kompile with these flags...
• [x] Lesson 19: codes should have line numbers since we’re referring to them.
• [x] Lesson 20: My Mac is Intel, compilation with the Haskell backend does not fail but krun does without --no-haskell-binary, see https://runtimeverification.slack.com/archives/C7E701MFG/p1660319199525119
• [x] Lesson 21: a SMT solver ~> an SMT solver
• [x] Why Lesson 22 isn’t in the side panel?
• [x] I agree with others that referring to Problems while they are titled Exercises is a little confusing.

[jinxinglim]

Lesson 1:

• [ ] Under the instructions for building with Nix flakes, after the instruction of temporarily adding the K binaries, it would be good to include how to add them permanently (i.e., update your $PATH with <checkout-dir>/result/bin).
• [ ] Building with Maven: If you have different Java versions installed, make sure you switch to a version that is compatible with Maven (e.g., run sudo update-alternatives --config java then select the openjdk-11-jdk version) before running mvn package. I initially had openjdk-17-jdk as my Java version, but it was incompatible with Maven.
• [ ] It will be good to include a short note on how to uninstall if one installed from binary package previously ,i.e., sudo apt remove kframework.

Lesson 13:

• [ ] I think it will be good if the instruction "Write an addition expression with integers" in one of the exercises can change to "Write an addition expression with at least 3 integers" to see how the different depth works.
• [ ] It might be good to put a remark that if the reader has trouble understanding the rules within the code in the future, they can try running program with --depth 1, then gradually increase the value of --depth to see successive states which may in turn help them understand the code. This method works for me quite well.

Lesson 16:

• [ ] The instruction of Exercise 1 is not exactly clear. It would be good if there is a test file included in this lesson for us to test our resulting interpreter.

Lesson 19:

• [ ] It would be good to add after the instruction on "...add the corresponding add-auto-load-safe-path command to your ~/.gdbinit file as prompted." that if there is no .gdbinit file in my ~/ directory, create one yourself. And that it is required to run commands k start, k step and k match in the lesson.

Lesson 22:

• [ ] For exercise 2, although the exercise asks us to extend the VERIFICATION module with two simplifications that capture the meaning of maxInt(A:Int, B:Int), it is actually not required as there are maxInt rules in domains.md.

[ehildenb]

From sonzu on Discord:

• [ ] In Lesson 1.3: BNF Syntax and Parser Generation, being a newbie, i thought it is telling me that i compiling the example was not possible, however, after a few days, i found out otherwise.

[sonzu-prog]

• [ ] In Lession 1.3, i do not understand what ".k .exclude" means.

  .k .exclude
     syntax Int ::= r"[\\+-]?[0-9]+" [token]

[Robertorosmaninho]

• [ ] Broken Link at From 0 to K Tutorial. The "install or update to the latest K release" points to a page that doesn't exist anymore.
• [x] The README misses the fmt as dependence to build K. It should be included in the list of dependencies to be installed with brew.
• [ ] Lesson 6: the last Fruits in the "Booleans in K - Exercise" sentence is miss highlighted.
• [ ] Lesson 19: Typo in "Generally speaking, there are three types of breakpoints we are interested in in a K semantics:", replace with "Generally speaking, there are three types of breakpoints we are interested in a K semantics:"

[Sta1400]

• [ ] In Lesson 1.3, maybe you should add a link to the regular expressions page on Wikipedia (https://en.wikipedia.org/wiki/Regular_expression)

[radumereuta]

• [ ] add more clarifications about why krun input and krun -cPGM behaves differently: https://github.com/runtimeverification/k/issues/3166

[Scott-Guest]

• [ ] General: Personal preference, but I think the in-text exercises should be numbered as well. It just makes it easier to organize my solutions.
• [ ] Lesson 2,3,4: kompiling as instructed results in

    [Warning] Compiler: Could not find main syntax module with name FOO-SYNTAX in definition. 
                        Use --syntax-module to specify one. Using FOO as default.

  We should either introduce syntax modules from the beginning (currently not done until Lesson 5), add instructions to pass the --syntax-module flag, or at least indicate that this warning can be ignored for now.

• [ ] Lesson 4: Small typo / inconsistency: lesson-04-E.k => lesson-04-e.k
• [ ] Lesson 4: It seems more useful to explain the issue in Exercise 4 as part of the text rather than leaving it as an exercise. The text never mentions that K/Flex tokenize greedily, so the exercise really just tests if you have this external knowledge.
• [ ] Lesson 9: "here is a variant of LESSON-09-A" => "here is a variant of LESSON-09-A"
• [ ] Lesson 12: "In this case, K will automatically transform the grammar in LESSON-12-B-SYNTAX..." => LESSON-12-A-SYNTAX.
• [ ] Lesson 15: For the exercise, it seems worth mentioning that you cannot use ... on the RHS of a rule if there is a configuration variable preventing the cell from being concretized.
• [ ] Lesson 16: It's mentioned that you can have multiple variables of Map sort on the RHS of a rule for map patterns, but the semantics is never well-explained (what happens if the keys overlap, or do they need to be disjoint, etc.?)
• [ ] Lesson 16: It would be useful to include a discussion of unparsing/specifying formats for these data structures (if that is even a feature K has?)
• [ ] Lesson 17: It's unclear why we have to provide default values to cells that won't actually be created at program start (e.g. \<optional> specifies the value 0 in the configuration of LESSON-17-A even though it has multiplicity "?") Is there a reason this is required, or is there a way to specify what the cells should contain without providing a concrete value like this?
• [ ] Lesson 20: "Note that on arm64 macOS (Apple Silicon), there is a known issue with the Compact library that causes crashes in the Haskell backend. Pass the additional flag --no-haskell-binary to kompile to resolve this. This flag is also needed when using krun." This issue also seems to occur on my Intel MacOS machine. Additionally, "--no-haskell-binary" does not appear to be a valid flag for krun.
• [ ] Lesson 22: KLabels are used here but never explained. It would also be good to include further explanation of why the "Bot" sort is required.
• [ ] Lesson 22: The claim in Exercise 2 now seems to go through without having to add additional simplification rules