Basic linter types and attributes
This file defines the basic types and attributes used by the linting
framework. A linter essentially consists of a function
declaration → tactic (option string), this function together with some
metadata is stored in the linter structure. We define two attributes:
Defines the user attribute nolint for skipping #lint
should_be_linted linter decl returns true if decl should be checked
using linter, i.e., if there is no nolint attribute.
- test : declaration → tactic (option string)
- no_errors_found : string
- errors_found : string
- is_fast : bool
- auto_decls : bool
A linting test for the #lint command.
test defines a test to perform on every declaration. It should never fail. Returning none
signifies a passing test. Returning some msg reports a failing test with error msg.
no_errors_found is the message printed when all tests are negative, and errors_found is printed
when at least one test is positive.
If is_fast is false, this test will be omitted from #lint-.
If auto_decls is true, this test will also be executed on automatically generated declarations.