ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
37 stars 10 forks source link

Add warning flags to command-line #151

Open n-osborne opened 11 months ago

n-osborne commented 11 months ago

The warning system for the qcheck-stm plugin can be a bit verbose, informing the user about each skipped clause even if there is another one that contains the information it were looking for.

I propose to have three verbosity modes:

  1. error only (when ortac have not been able to generate anything)
  2. warnings that impacts the generated artefact or test coverage (when a function has been skipped because next-state is impossible to generate, or because there is no sut type in the parameters).
  3. extra verbosity, displaying every warnings possible even about skipped clauses.

2 could be the default, 1 a --quiet option and 3 a --verbose option.