dafny icon indicating copy to clipboard operation
dafny copied to clipboard

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

Open kjx opened this issue 6 months ago • 0 comments

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 avatar Aug 29 '24 08:08 kjx