leanprover-community / leanprover-community/lean
Running `leanpkg <command> --help` runs <command>
Open
Nobody has claimed this yet.
- Dominant language
- C++
- Stars
- 434
- Forks
- 79
- PR merge metrics
- No merged PRs in 30d
Description
Prerequisites
- Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Specifically, check out the wishlist, open RFCs,
or feature requests.
- Specifically, check out the wishlist, open RFCs,
- Reduced the issue to a self-contained, reproducible test case.
- Checked that your issue isn't already filed.
Description
Running leanpkg <command> --help runs <command> rather than showing help for it.
Steps to Reproduce
E.g.:
leanpkg test --help executes test.
Expected behavior: For the above, showing e.g. download dependencies, build *.olean files, and run test files as shown from running leanpkg --help.
Actual behavior: leanpkg test is run.
Reproduces how often: 7 days a week.
Versions
⊙ lean --version julian@Air
Lean (version 3.20.0, commit 4c40c41ccc08, Release)
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Reproduce the behavior with leanpkg test --help and compare it with leanpkg --help. Start by tracing how leanpkg dispatches subcommands and handles --help; done means the command help text is shown without running test or another subcommand.
Written by the indexing model from the issue text.
Assessment
- Domain
- cli
- Issue type
- Bug
- Difficulty
- 2/5
- Estimated time
- 1-3 hours
- Activity status
- Stale
- Clarity
- Clearly specified
- Newbie friendliness
- 52/100