Dynamic targets in `kbuild`

Start by tracing how kbuild reads target specifications from kbuild.toml and handles the kbuild kompile command. Review the proposed kbuild.py hook and BuildInput examples to define the integration boundaries. Done means build hooks can receive arguments, perform target processing, and coexist with or replace kbuild.toml target metadata.

kbuild currently only admits static build targets specified in kbuild.toml. In order to support more complex build scripts (in particular https://github.com/runtimeverification/evm-semantics/issues/1744), kbuild needs to handle input parameters, do pre- or postprocessing on targets, and support nontrivial logic.

The solution for this problem is to expose an interface that enables the developer to provide hooks into the build pipeline. The following example outlines such an approach.

Suppose we have a simple target

[targets.haskell]
backend = "haskell"
main-file = "imp.md"
md-selector = "k"

However, for some use cases we'd like to kompile some additional rules for the same target:

md-selector = "k | k_extra"

So we create a file kbuild.py, and define

def build_haskell(build_input: BuildInput) -> Target:
    md_selector = 'k | k_extra' if if build_input.args.get('extra_rules') == 'true' else 'k'
    return HaskellTarget(main_file='imp.k', md_selector)

Here, build_input is provided by the framework, and can contain things like:

class BuildInput:
    platform: str
    k_version: KVersion
    build_dir: Path
    args: Mapping[str, str]
    ...

When kbuild is called, the build argument can be passed:

kbuild kompile haskell --arg extra-rules=true

We can provide decorators for a better programming interface:

@kbuild_param('extra_rules', __my_str_to_bool)
def build_haskell(build_input: BuildInput, extra_rules: bool) -> Target:
    ...

As the hook is provided, the target specification in kbuild,toml becomes superfluous, and can be removed. With support for such hooks, kbuild can be reimplemented so that target specifications in kbuild.toml just become metadata for either a custom or a simple default hook implementation.