Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"Betterhelp" - self-care is non-negotiable. - LOW SEVERITY #5731

Open
kjx opened this issue Aug 29, 2024 · 0 comments
Open

"Betterhelp" - self-care is non-negotiable. - LOW SEVERITY #5731

kjx opened this issue Aug 29, 2024 · 0 comments
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

Comments

@kjx
Copy link

kjx commented Aug 29, 2024

Summary

(sorry couldn't resist the issue title)

the dafny command needs better help

Background and Motivation

running the dafny command gets an informative message:

.dafny 
Required command was not provided.

Description:
  The Dafny CLI enables working with Dafny, a verification-aware programming language. Use 'dafny -?' to see help for the previous CLI format.

Usage:
  Dafny [command] [options] [[--] <additional arguments>...]]

and on for another couple of pages. But unfortunately then doing:

.dafny help
*** Error: 'help': The first input must be a command or a legacy option or file with supported extension

gets a particularly unhelpful message.

.dafny --help resolve dfyconfig.toml 

gets pages of help on :resolve" but forgetting the -- gets the same nonhekpful result

.dafny help resolve dfyconfig.toml 
*** Error: 'help': The first input must be a command or a legacy option or file with supported extension

Proposed Feature

I notice doing 'dafny --help X' never runs the command X but rather prints out help.
consider making "help" a command as well as or instead of an option.

at least, if dafny can't intepret the command it could give a hint to try -h or --help.

Alternatives

see above

@kjx kjx added the kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny label Aug 29, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
Projects
None yet
Development

No branches or pull requests

1 participant