Simplify option parsing code in pyk

[dwightguth]

I had the recent experience of adding a new command line option to pyk kompile recently and noticed that it's a good bit more complicated than the process of adding a command line option to the Java codebase.

Here is a side by side comparison:

Java:

• Declaratively add option and its description and default
• Use option

Python:

• update exec_kompile in __main__.py
• add field to KompileOptions class
• add default value to KompileOptions class
• Declaratively add option and its description
• add field to LLVMKompile class
• add parameter to LLVMKompile constructor
• add initializer to body of LLVMKompile constructor
• propagate flag from LLVMKompile to JVM

In general I've noticed a lot of code in pyk that simply propagates options back and forth between different layers of abstraction. This adds a good bit of flexibility, because you can always easily control which flags are set to which values at each level. But it makes there be a large amount of boilerplate code like this, which is potentially prone to bugs if a site where an option needs to be propagated is missed. I'm not entirely sure what a scriptable but less-full-of-boilerplate solution might look like, but you might want to consider thinking about it. As the code base grows, you may find that this is a source of fragility in the overall stability of the tool.

[ehildenb]

Related: https://github.com/runtimeverification/k/issues/4188 Related: https://github.com/runtimeverification/pyk/issues/885 Related: https://github.com/runtimeverification/pyk/issues/906

We have prioritized re-usability of the options downstream, which indeed causes a decent amount of boilerplate. We've also prioritized supporting both CLI and TOML file configuration of options in Kontrol, but having one source of truth on the "defaults". Unfortunately, it hasn't quite all stitched together yet.

I think we can definitely do better here, the question is whether it's worth investing in now.