add toml support for pyk options #4254
Conversation
ovatman
requested review from
dwightguth,
ehildenb,
rv-jenkins and
F-WRunTime
as code owners
ovatman
requested review from
nwatson22
and removed request for
dwightguth,
rv-jenkins,
ehildenb and
F-WRunTime
|
@ovatman you'll need to rebase on |
There was a problem hiding this comment.
This looks good to me, once it has been rebased properly and the KEVM and kontrol branches are working. I like the solution of having the mapping from command-line string format to python variable format.
There may be a way to avoid having to mention all the superclasses in from_option_string, by adding a new function in Options here similar to the constructor that collects and merges the from_option_strings for any type of Options.
There is a lot of boilerplate that has to be duplicated across all 3 repos, but this was also the case with version of Options that was merged. Hopefully eventually we will be wrapping the argparse and toml parsing logic and consolidating most of the boilerplate into pyk only (Similar to what is mentioned in #4188)
ovatman
force-pushed
the
tolga/toml-options-rebased
branch
from
28bcfb0
to
68705e1
Compare
Fixes #4197 This PR allows calling `pyk prove` with a custom server executable via `pyk prove --kore-rpc-command COMMAND`, which is especially useful when giving logging options to the server, i.e.: ``` pyk prove test-spec.k --verbose --kore-rpc-command 'kore-rpc-booster -l Simplify' ```
fixes #4187 The pyk outer lexer now has location information for attribute tokens. The unit tests for the lexer now check that the token text actually appears at its location in the source text. --------- Co-authored-by: rv-jenkins <[email protected]>
Co-authored-by: devops <[email protected]>
Transfer of: runtimeverification/pyk#1008