Context
The probe merge command currently enforces that all inputs belong to the same schema category (atoms, specs, or proofs). Mixing categories produces an error.
Question
Would it be useful to allow merging atoms with specs and/or proofs into a single file? Potential use cases:
- A single "enriched" merged file containing the full call graph (atoms) alongside specification metadata (specs) and verification results (proofs) for the same code-names.
- Simplifying downstream consumption by having one file instead of three separate merged files.
Considerations
- The
data dictionary values have different schemas per category (atoms have display-name, dependencies, etc.; specs have specified, has_requires, etc.; proofs have verified, status, etc.). Merging them into one dictionary would require either separate top-level keys ("atoms", "specs", "proofs") or a union schema per entry.
probe-lean/enriched-atoms already combines atoms with spec/proof data at the per-entry level. Cross-category merge might overlap with or duplicate that pattern.
- The current same-category enforcement is a simple safety check that prevents accidental misconfiguration.
Decision needed
Decide whether cross-category merge should be supported and, if so, what the output schema should look like.
Context
The
probe mergecommand currently enforces that all inputs belong to the same schema category (atoms, specs, or proofs). Mixing categories produces an error.Question
Would it be useful to allow merging atoms with specs and/or proofs into a single file? Potential use cases:
Considerations
datadictionary values have different schemas per category (atoms havedisplay-name,dependencies, etc.; specs havespecified,has_requires, etc.; proofs haveverified,status, etc.). Merging them into one dictionary would require either separate top-level keys ("atoms","specs","proofs") or a union schema per entry.probe-lean/enriched-atomsalready combines atoms with spec/proof data at the per-entry level. Cross-category merge might overlap with or duplicate that pattern.Decision needed
Decide whether cross-category merge should be supported and, if so, what the output schema should look like.