--start-symbol for kmir run
#446
Conversation
| run_parser.add_argument( | ||
| '--start-symbol', type=str, metavar='SYMBOL', default='main', help='Symbol name to begin execution from' | ||
| ) |
There was a problem hiding this comment.
👍 good idea.
I was struggling to find a way to have a default value for a K config variable (there is probably none), this is much easier.
| kcell = None | ||
|
|
||
| def get_k_cell(term: KInner) -> None: | ||
| match term: | ||
| case KApply(label=KLabel('<k>')): | ||
| nonlocal kcell | ||
| kcell = term | ||
|
|
||
| collect(get_k_cell, kast_result) | ||
|
|
||
| with output_kast.open('r') as f: | ||
| expected = f.read().rstrip() | ||
|
|
||
| result_pretty = tools.kprint.kore_to_pretty(result).rstrip() | ||
| assert isinstance(kcell, KApply) | ||
| result_pretty = tools.kprint.pretty_print(kcell).rstrip() |
There was a problem hiding this comment.
Not sure we should give up on comparing all of the configuration.
How about we add a make target to both re-generate the *.smir.json and the expected output?
The expected output in my version is easy to produce just by piping kmir run output into a file, and we could run stable-mir-json before so we also update the json. This would be a standard task to run locally as a preparation when opening a PR.
There was a problem hiding this comment.
A make target to update expected outputs will in certain circumstances be a good tool to have.
But, what's the point of having these tests, if they change with every change we make? I think we should try for something that's at least semi-stable so we don't have as many larger irrelevant diffs in our PRs.
There was a problem hiding this comment.
Well... if the test fails, or it you proactively change the expectation file using that make target, reviewers are encouraged to look at the changed output. We can still all choose to skip those changes in the test expectations but they provide examples of how the configuration is expected to change with the respective code change in the PR.
If you think that's useless we can of course also just scrape the tests, or compare selected cells. But I thought it is acceptable to maintain and useful. Let's see what @dkcumming thinks
There was a problem hiding this comment.
I think it is nice to check the diffs, at least that way we can tell if things are changing as we expect. But this is assuming there isn't much overhead. I think it is preferable to have these extra steps if they are manageable though - preferable to not noticing we changed something spuriously and finding it later and having to retrace steps.
There was a problem hiding this comment.
Ok, I've added make update-exec-smir and reverted the test outputs. I do believe that the K configuration exposes implementation details that we should prefer not to have and should focus on interfacing with it to test only behavior (ie. function return values, successful execution, anything we can model about Rust's semantics), but we can kick that can down the road. I wont push for it here.
deps/stable-mir-json
Outdated
There was a problem hiding this comment.
This was in one of my commits on the other PR by mistake.
Maybe best to rebase -i master your current branch and remove all commits from the other PR. Or else you can of course revert the submodule downgrade manually.
There was a problem hiding this comment.
Thanks for catching this. When I merged master in I had too many conflicts that didn't make sense so I just used the "ours" strategy, this submodule downgrade must have slipped in that way.
This reverts commit 4933b21.
gtrepta
force-pushed
the
guy/cli-start-symbol
branch
from
0c3b00c to
e11f43d
Compare
This adds a
<start-symbol>cell to the configuration with a configuration variable for the symbol to begin execution from.It also changes the expected output in the
exec-smirintegration tests to only check the contents of the K cell. The semantics are going to be very unstable right now, and without this change we will probably be spending time updating the test vectors on nearly every pull request.