Cleanup any mention of --transition flag #3897
Conversation
|
I textually searched the codebase for |
There was a problem hiding this comment.
Mostly LGTM, but see my comments.
One thing that's still unclear to me - the outdated lessons state that --search will not explore all heating / cooling interleavings unless specifically instructed to do so with --transition. Is that still the case, and is there some modern alternative to --transition? Or does --search explore all interleavings by default nowadays?
| @@ -31,99 +31,6 @@ the `krun` tool with the option `--search`. For example: | |||
|
|
|||
There was a problem hiding this comment.
We've removed almost everything from this lesson - the title is "Tagging; Transition Kompilation Option", and we no longer explain tagging nor --transition. We should consider just deleting it entirely.
The only remaining content is pretty short and could be easily moved into other lessons:
- defining the variable increment rule
- describing
--search
| with the command: | ||
|
|
||
| ```shell script | ||
| kompile imp.k --transition="addition division lookup assignment increment read print" |
There was a problem hiding this comment.
Most of these addition, division, lookup, etc. tags are unneeded now, so we should remove the corresponding group(_) attributes on the rules. Similarly in the other lessons too.
| Oops, we see only one solution, the same as when we ran it without search. | ||
|
|
||
| Here is what happens. `krun` can only explore as much of the transition | ||
| system associated to a program as `kompile` allowed the generated language | ||
| model to yield. Since most of the K users are interested in language models | ||
| that execute efficiently, that is, in faster interpreters for the defined | ||
| languages, by default `kompile` optimizes the generated language model for | ||
| execution. In particular, it inserts no backtracking markers, which `krun` | ||
| uses when called with the `--search` option in order to systematically generate | ||
| the entire transition system associated to a program. This is why `krun` | ||
| showed us only one solution when run with the `--search` option on `div.imp`. |
There was a problem hiding this comment.
Does --search still only return one solution here, or does it actually show all the different interleavings nowadays?
If it only returns one solution, I think we still need to include a good chunk of the prose here to explain why the other solutions are missing.
There was a problem hiding this comment.
I tested it and indeed --search returns all solutions now. I believe this was written before the search feature in the llvm backend was a thing.
|
Closing as it's overridden by #3901 . Will open this in the pl-tutorial repo. |
fixes: #1936