Allow compilation of a <file>:<module> via --add-module.

[mariaKt]

This PR extends the --add-module option to accept K source files (.k/.md) in addition to JSON, using the format file.k:MODULE_NAME or file.md:MODULE_NAME.

• Parses K source modules via kprove --dry-run (pyk's parse_modules), matching how kontrol's --lemmas flag works
• JSON format (file.json from --to-module) remains supported for backward compatibility
• Type of add_module changed from Path | None to str | None across the pipeline

The intend of this was to be used for conditional compilation of the lemmas added for the validate owner function. However, while working on it, I found that currently there are limitations to what rules can be loaded dynamically, making static compilation of the lemmas for validate owner a better short term option. We could comment out the imports, so that by default the lemmas are not used, or try adding a new build target.

Identified limitations

• syntax declarations (generally, other than tokens for existing sorts)
• KAs
• subsort injections

[Stevengre]

This looks like it currently lacks sufficient test coverage, especially for the newly introduced file.k/md/json:MODULE paths.

I’m also not fully convinced about the necessity of this feature. From my understanding, the “one file → one module” workflow already covers most use cases, so the added value here isn’t entirely clear to me yet.

That said, extending functionality is generally a good direction. However, before merging, I think we should at least have:

• Proper tests covering the new code paths (not just the existing JSON case)
• Documentation updates clarifying the intended use cases and expected behavior

Otherwise, this risks introducing an under-specified and under-tested feature into the codebase.

[mariaKt]

This looks like it currently lacks sufficient test coverage, especially for the newly introduced file.k/md/json:MODULE paths.

I’m also not fully convinced about the necessity of this feature. From my understanding, the “one file → one module” workflow already covers most use cases, so the added value here isn’t entirely clear to me yet.

That said, extending functionality is generally a good direction. However, before merging, I think we should at least have:

* Proper tests covering the new code paths (not just the existing JSON case)

* Documentation updates clarifying the intended use cases and expected behavior

Otherwise, this risks introducing an under-specified and under-tested feature into the codebase.

You are correct. Here is the context. When I first started this, there were multiple modules in a file and I meant to import only some, so the extension Path -> str made sense. Then, as I worked around the limitations, I ended up with only one module to be imported in the new file, so this extension alone (without the necessary pyk functionality extensions) would not help much. The feature I believe can be useful that is added here is the ability to read from .k/.md in addition to .json would be useful. However, there are restrictions in how the rules can be written when loading a .k/.md module, that are not present when using the .json path.

In any case, this cannot be used for the current lemmas, so as you point out I will need to add a couple of small unit tests for these.

[Stevengre]

Thanks. Since I don’t think this PR is ready for review yet, I switched it back to draft, so for now we only need to review the PRs that are still open. Does that sound right to you? Sorry if you would have preferred to keep this one open, and of course it can be reopened anytime.