Skip to content

Inconsistent command-line error messages #4072

@davidcok

Description

@davidcok

Dafny version

4.1.0+dev

Code to produce this issue

No response

Command to run and resulting output

No response

What happened?

The command-line error messages take many forms:

  • some start with *** Error:, some with dafny: Error, some with no prefix
  • some go to stdout, some to stderr
  • some include the full legacy help document, some do not
  • some use exceptions for handling errors, some do not
  • they generally do not use the same ErrorReporter mechanism that other errors do

Regularizing this is complicated by the design in which the dafny tool uses the boogie command-line parser for part of its logic. It is also complicated by needing to support both verb-form (which uses the .NET Command Line handling library) and legacy CLI.

What type of operating system are you experiencing the problem on?

Mac

Metadata

Metadata

Assignees

No one assigned

    Labels

    area: error-reportingClarity of the error reportingkind: enhancementEnhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions