docs: streamline README and improve CLI --help descriptions#979
docs: streamline README and improve CLI --help descriptions#979
Conversation
Stevengre
changed the title
Stevengre
force-pushed
the
docs/streamline-readme
branch
from
b04922b to
e71120b
Compare
|
|
||
| # Convenience script (also supports png/pdf/dot visualization) | ||
| ./scripts/generate-smir-json.sh your_file.rs . png | ||
| ``` |
There was a problem hiding this comment.
The usage of the script is not entirely clear here, e.g., ./scripts/generate-smir-json.sh your_file.rs . for json generation. IT is not clear now that the convenience script can be used only to generate json, and additionally for visualization. I think Maybe [png/pdf/dot] ?
There was a problem hiding this comment.
Good point, thanks. I clarified the usage and added the optional [png|pdf|dot] argument to indicate visualization formats.
kmir/src/kmir/__main__.py
Outdated
| link_parser.add_argument('smir_files', nargs='+', metavar='SMIR_JSON', help='SMIR JSON files to link') | ||
| link_parser.add_argument( | ||
| '--output-file', '-o', metavar='FILE', help='Output file', default='linker_output.smir.json' | ||
| '--output-file', '-o', metavar='FILE', help='Output file (default: linker_output.smir.json)', default='linker_output.smir.json' |
There was a problem hiding this comment.
What is the meaning of this? The output file name has a default value which is linker_output.smir.json?
There was a problem hiding this comment.
Yes. You can see default='linker_output.smir.json' in the config.
|
This adds a lot of clarity in many places. I asked something that wasn't clear to me, and proposed a minor change where I thought that one command's usage was not covered in as much detail as in the original description. |
…flow Consolidate repeated setup instructions (rustup, git clone, submodule init) into a single Quick Start section. Replace verbose per-command CLI docs with a command table (details available via --help). Add practical "Typical proof workflow" and "Debugging a stuck or failing proof" sections covering show, prune, section-edge, break-on-* flags, and module export/import.
- info --types: document output format and behavior when omitted - show --node-deltas-pro: clarify it also prints rules for the edges - show --rules: note output is Markdown links to K rule sources - link --output-file: show default value (linker_output.smir.json)
- run: clarify --bin is cargo target, --file is SMIR JSON, note mutual exclusivity; --depth explains "execution steps" - prove-rs: --max-depth explains KCFG edge semantics; --reload warns it discards progress; --break-on-function clarifies substring matching - show: --full-printer notes default is compact; --minimize-proof notes it requires --to-module - prune: NODE explains subtree removal - section-edge: edge help uses clearer wording - proof_args: PROOF_ID uses generic "operate on" instead of "view"
Updated script usage instructions in README.
Stevengre
force-pushed
the
docs/streamline-readme
branch
from
7f8beae to
0c9f5d1
Compare
2 participants
Summary
README.md:
--help--break-on-*flags,section-edge,prune, and module export/importCLI
--helpimprovements (__main__.py):run: clarify--bin(cargo target) vs--file(SMIR JSON) mutual exclusivity;--depth→ "execution steps"prove-rs:--max-depthexplains KCFG edge semantics;--reloadwarns about discarding progress;--break-on-functionclarifies substring matchingshow:--full-printernotes default is compact;--minimize-proofnotes dependency on--to-module;--rulesdescribes Markdown link output;--node-deltas-prodocuments auto-printing rulesprune:NODEexplains subtree removalsection-edge: clearer edge format descriptioninfo --types: documents output format and behavior when omittedlink --output-file: shows default valueTest plan
--helpoutput renders correctly for all subcommands